:: SCMRING1 semantic presentation

REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal V29() cardinal limit_cardinal countable denumerable Element of bool REAL
bool REAL is set
omega is non empty epsilon-transitive epsilon-connected ordinal V29() cardinal limit_cardinal countable denumerable set
bool omega is V29() set
bool NAT is V29() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
[:2,2:] is set
[:[:2,2:],2:] is set
bool [:[:2,2:],2:] is set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
[:1,1:] is set
bool [:1,1:] is set
[:[:1,1:],1:] is set
bool [:[:1,1:],1:] is set
9 is non empty epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
Segm 9 is countable Element of bool omega
K233() is non empty set
SCM-Memory is non empty set
bool SCM-Memory is set
[:SCM-Memory,2:] is set
bool [:SCM-Memory,2:] is set
SCM-OK is Relation-like SCM-Memory -defined 2 -valued Function-like non empty V14( SCM-Memory ) V18( SCM-Memory ,2) Element of bool [:SCM-Memory,2:]
SCM-VAL is Relation-like 2 -defined Function-like V14(2) set
SCM-OK * SCM-VAL is Relation-like non-empty Function-like set
product (SCM-OK * SCM-VAL) is functional non empty with_common_domain product-like set
K234() is non empty V137() V138() V139() V141() set
K70((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))) is functional non empty set
[:K234(),K70((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))):] is set
bool [:K234(),K70((product (SCM-OK * SCM-VAL)),(product (SCM-OK * SCM-VAL))):] is set
{} is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() cardinal {} -element FinSequence-membered countable set
3 is non empty epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
0 is Function-like functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V29() cardinal {} -element FinSequence-membered countable Element of NAT
SCM-Data-Loc is non empty Element of bool SCM-Memory
Seg 1 is non empty trivial V29() 1 -element countable Element of bool NAT
{1} is non empty trivial 1 -element set
Seg 2 is non empty V29() 2 -element countable Element of bool NAT
{1,2} is non empty set
8 is non empty epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
Segm 8 is countable Element of bool omega
S is non empty 1-sorted
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like Function-like set
proj1 (SCM-OK * (S)) is set
proj1 SCM-OK is set
len <%NAT, the carrier of S%> is epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
proj1 <%NAT, the carrier of S%> is epsilon-transitive epsilon-connected ordinal natural V29() cardinal 2 -element countable set
proj2 SCM-OK is set
proj1 (S) is set
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like Function-like set
(SCM-OK * (S)) . NAT is set
proj1 SCM-OK is set
SCM-OK . NAT is set
(S) . (SCM-OK . NAT) is set
(S) . 0 is set
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like Function-like set
s is Element of SCM-Memory
(SCM-OK * (S)) . s is set
proj1 SCM-OK is set
SCM-OK . s is epsilon-transitive epsilon-connected ordinal Element of 2
(S) . (SCM-OK . s) is set
(S) . 1 is set
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like Function-like set
g is set
proj1 (SCM-OK * (S)) is set
(SCM-OK * (S)) . g is set
s is non empty 1-sorted
(s) is Relation-like 2 -defined Function-like V14(2) set
the carrier of s is non empty set
<%NAT, the carrier of s%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (s) is Relation-like non-empty Function-like set
S is Element of SCM-Data-Loc
(SCM-OK * (s)) . S is set
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like non-empty Function-like set
product (SCM-OK * (S)) is functional non empty with_common_domain product-like set
pi ((product (SCM-OK * (S))),NAT) is set
proj1 (SCM-OK * (S)) is set
(SCM-OK * (S)) . NAT is set
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like non-empty Function-like set
product (SCM-OK * (S)) is functional non empty with_common_domain product-like set
s is Element of SCM-Data-Loc
pi ((product (SCM-OK * (S))),s) is set
proj1 (SCM-OK * (S)) is set
(SCM-OK * (S)) . s is set
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like non-empty Function-like set
product (SCM-OK * (S)) is functional non empty with_common_domain product-like set
s is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
s . NAT is set
pi ((product (SCM-OK * (S))),NAT) is set
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like non-empty Function-like set
product (SCM-OK * (S)) is functional non empty with_common_domain product-like set
s is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
g is epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable set
NAT .--> g is Relation-like {NAT} -defined Function-like one-to-one Cardinal-yielding set
{NAT} is non empty trivial 1 -element set
{NAT} --> g is Relation-like {NAT} -defined {g} -valued Function-like constant non empty V14({NAT}) V18({NAT},{g}) Cardinal-yielding V132() Element of bool [:{NAT},{g}:]
{g} is non empty trivial 1 -element set
[:{NAT},{g}:] is set
bool [:{NAT},{g}:] is set
s +* (NAT .--> g) is Relation-like Function-like set
x is set
proj1 (SCM-OK * (S)) is set
proj1 (NAT .--> g) is set
(s +* (NAT .--> g)) . NAT is set
(NAT .--> g) . NAT is set
(s +* (NAT .--> g)) . x is set
(SCM-OK * (S)) . x is set
proj1 (NAT .--> g) is set
(s +* (NAT .--> g)) . x is set
s . x is set
(SCM-OK * (S)) . x is set
proj1 s is set
proj1 (s +* (NAT .--> g)) is set
proj1 (NAT .--> g) is set
SCM-Memory \/ (proj1 (NAT .--> g)) is non empty set
SCM-Memory \/ {NAT} is non empty set
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like non-empty Function-like set
product (SCM-OK * (S)) is functional non empty with_common_domain product-like set
s is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
g is epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable set
(S,s,g) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
NAT .--> g is Relation-like {NAT} -defined Function-like one-to-one Cardinal-yielding set
{NAT} --> g is Relation-like {NAT} -defined {g} -valued Function-like constant non empty V14({NAT}) V18({NAT},{g}) Cardinal-yielding V132() Element of bool [:{NAT},{g}:]
{g} is non empty trivial 1 -element set
[:{NAT},{g}:] is set
bool [:{NAT},{g}:] is set
s +* (NAT .--> g) is Relation-like Function-like set
(S,s,g) . NAT is set
proj1 (NAT .--> g) is set
(NAT .--> g) . NAT is set
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like non-empty Function-like set
product (SCM-OK * (S)) is functional non empty with_common_domain product-like set
s is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
g is epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable set
(S,s,g) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
NAT .--> g is Relation-like {NAT} -defined Function-like one-to-one Cardinal-yielding set
{NAT} --> g is Relation-like {NAT} -defined {g} -valued Function-like constant non empty V14({NAT}) V18({NAT},{g}) Cardinal-yielding V132() Element of bool [:{NAT},{g}:]
{g} is non empty trivial 1 -element set
[:{NAT},{g}:] is set
bool [:{NAT},{g}:] is set
s +* (NAT .--> g) is Relation-like Function-like set
x is Element of SCM-Data-Loc
(S,s,g) . x is set
s . x is set
proj1 (NAT .--> g) is set
SCM-OK . NAT is set
SCM-OK . x is epsilon-transitive epsilon-connected ordinal Element of 2
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like non-empty Function-like set
product (SCM-OK * (S)) is functional non empty with_common_domain product-like set
s is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
g is epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable set
(S,s,g) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
NAT .--> g is Relation-like {NAT} -defined Function-like one-to-one Cardinal-yielding set
{NAT} --> g is Relation-like {NAT} -defined {g} -valued Function-like constant non empty V14({NAT}) V18({NAT},{g}) Cardinal-yielding V132() Element of bool [:{NAT},{g}:]
{g} is non empty trivial 1 -element set
[:{NAT},{g}:] is set
bool [:{NAT},{g}:] is set
s +* (NAT .--> g) is Relation-like Function-like set
x is epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable set
(S,s,g) . x is set
s . x is set
proj1 (NAT .--> g) is set
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like non-empty Function-like set
product (SCM-OK * (S)) is functional non empty with_common_domain product-like set
s is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
g is Element of SCM-Data-Loc
x is Element of the carrier of S
g .--> x is Relation-like SCM-Data-Loc -defined {g} -defined the carrier of S -valued Function-like one-to-one set
{g} is non empty trivial 1 -element set
{g} --> x is Relation-like {g} -defined the carrier of S -valued {x} -valued Function-like constant non empty V14({g}) V18({g},{x}) Element of bool [:{g},{x}:]
{x} is non empty trivial 1 -element set
[:{g},{x}:] is set
bool [:{g},{x}:] is set
s +* (g .--> x) is Relation-like Function-like set
gx is set
proj1 (SCM-OK * (S)) is set
proj1 (g .--> x) is set
(s +* (g .--> x)) . g is set
(g .--> x) . g is set
(s +* (g .--> x)) . gx is set
(SCM-OK * (S)) . gx is set
proj1 (g .--> x) is set
(s +* (g .--> x)) . gx is set
s . gx is set
(SCM-OK * (S)) . gx is set
proj1 s is set
proj1 (s +* (g .--> x)) is set
proj1 (g .--> x) is set
SCM-Memory \/ (proj1 (g .--> x)) is non empty set
SCM-Memory \/ {g} is non empty set
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like non-empty Function-like set
product (SCM-OK * (S)) is functional non empty with_common_domain product-like set
s is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
s . NAT is set
g is Element of SCM-Data-Loc
x is Element of the carrier of S
(S,s,g,x) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
g .--> x is Relation-like SCM-Data-Loc -defined {g} -defined the carrier of S -valued Function-like one-to-one set
{g} is non empty trivial 1 -element set
{g} --> x is Relation-like {g} -defined the carrier of S -valued {x} -valued Function-like constant non empty V14({g}) V18({g},{x}) Element of bool [:{g},{x}:]
{x} is non empty trivial 1 -element set
[:{g},{x}:] is set
bool [:{g},{x}:] is set
s +* (g .--> x) is Relation-like Function-like set
(S,s,g,x) . NAT is set
proj1 (g .--> x) is set
SCM-OK . NAT is set
SCM-OK . g is epsilon-transitive epsilon-connected ordinal Element of 2
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like non-empty Function-like set
product (SCM-OK * (S)) is functional non empty with_common_domain product-like set
s is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
g is Element of SCM-Data-Loc
x is Element of the carrier of S
(S,s,g,x) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
g .--> x is Relation-like SCM-Data-Loc -defined {g} -defined the carrier of S -valued Function-like one-to-one set
{g} is non empty trivial 1 -element set
{g} --> x is Relation-like {g} -defined the carrier of S -valued {x} -valued Function-like constant non empty V14({g}) V18({g},{x}) Element of bool [:{g},{x}:]
{x} is non empty trivial 1 -element set
[:{g},{x}:] is set
bool [:{g},{x}:] is set
s +* (g .--> x) is Relation-like Function-like set
(S,s,g,x) . g is set
proj1 (g .--> x) is set
(g .--> x) . g is set
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like non-empty Function-like set
product (SCM-OK * (S)) is functional non empty with_common_domain product-like set
s is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
g is Element of SCM-Data-Loc
x is Element of the carrier of S
(S,s,g,x) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
g .--> x is Relation-like SCM-Data-Loc -defined {g} -defined the carrier of S -valued Function-like one-to-one set
{g} is non empty trivial 1 -element set
{g} --> x is Relation-like {g} -defined the carrier of S -valued {x} -valued Function-like constant non empty V14({g}) V18({g},{x}) Element of bool [:{g},{x}:]
{x} is non empty trivial 1 -element set
[:{g},{x}:] is set
bool [:{g},{x}:] is set
s +* (g .--> x) is Relation-like Function-like set
gx is Element of SCM-Data-Loc
(S,s,g,x) . gx is set
s . gx is set
proj1 (g .--> x) is set
S is non empty 1-sorted
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like non-empty Function-like set
product (SCM-OK * (S)) is functional non empty with_common_domain product-like set
s is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
g is Element of SCM-Data-Loc
s . g is set
pi ((product (SCM-OK * (S))),g) is set
S is non empty 1-sorted
the carrier of S is non empty set
s is Element of SCM-Data-Loc
g is Element of the carrier of S
<*s,g*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*s*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,s] is V15() set
{1,s} is non empty set
{{1,s},{1}} is non empty set
{[1,s]} is Function-like non empty trivial 1 -element set
<*g*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,g] is V15() set
{1,g} is non empty set
{{1,g},{1}} is non empty set
{[1,g]} is Function-like non empty trivial 1 -element set
K109(<*s*>,<*g*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
SCM-Data-Loc \/ the carrier of S is non empty set
x is set
proj2 <*s,g*> is set
<*s,g*> is Relation-like NAT -defined K233() \/ the carrier of S -valued Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable FinSequence of K233() \/ the carrier of S
K233() \/ the carrier of S is non empty set
dom <*s,g*> is 2 -element countable Element of bool NAT
proj2 <*s,g*> is set
gx is set
<*s,g*> . gx is set
S is non empty V67() V92() V93() V94() V103() V110() V111() L11()
SCM-Instr S is non empty set
(S) is Relation-like 2 -defined Function-like V14(2) set
the carrier of S is non empty set
<%NAT, the carrier of S%> is Relation-like NAT -defined Function-like T-Sequence-like V29() 2 -element countable V136() set
SCM-OK * (S) is Relation-like non-empty Function-like set
product (SCM-OK * (S)) is functional non empty with_common_domain product-like set
s is Element of SCM-Instr S
g is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
s address_1 is Element of K233()
s address_2 is Element of K233()
(S,g,(s address_2)) is Element of the carrier of S
(S,g,(s address_1),(S,g,(s address_2))) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
(s address_1) .--> (S,g,(s address_2)) is Relation-like K233() -defined {(s address_1)} -defined the carrier of S -valued Function-like one-to-one set
{(s address_1)} is non empty trivial 1 -element set
{(s address_1)} --> (S,g,(s address_2)) is Relation-like {(s address_1)} -defined the carrier of S -valued {(S,g,(s address_2))} -valued Function-like constant non empty V14({(s address_1)}) V18({(s address_1)},{(S,g,(s address_2))}) Element of bool [:{(s address_1)},{(S,g,(s address_2))}:]
{(S,g,(s address_2))} is non empty trivial 1 -element set
[:{(s address_1)},{(S,g,(s address_2))}:] is set
bool [:{(s address_1)},{(S,g,(s address_2))}:] is set
g +* ((s address_1) .--> (S,g,(s address_2))) is Relation-like Function-like set
(S,g) is epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
g . NAT is set
succ (S,g) is non empty epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable set
(S,(S,g,(s address_1),(S,g,(s address_2))),(succ (S,g))) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
NAT .--> (succ (S,g)) is Relation-like {NAT} -defined Function-like one-to-one Cardinal-yielding set
{NAT} --> (succ (S,g)) is Relation-like non-empty {NAT} -defined {(succ (S,g))} -valued Function-like constant non empty V14({NAT}) V18({NAT},{(succ (S,g))}) Cardinal-yielding V132() Element of bool [:{NAT},{(succ (S,g))}:]
{(succ (S,g))} is non empty trivial 1 -element set
[:{NAT},{(succ (S,g))}:] is set
bool [:{NAT},{(succ (S,g))}:] is set
(S,g,(s address_1),(S,g,(s address_2))) +* (NAT .--> (succ (S,g))) is Relation-like Function-like set
(S,g,(s address_1)) is Element of the carrier of S
(S,g,(s address_1)) + (S,g,(s address_2)) is Element of the carrier of S
(S,g,(s address_1),((S,g,(s address_1)) + (S,g,(s address_2)))) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
(s address_1) .--> ((S,g,(s address_1)) + (S,g,(s address_2))) is Relation-like K233() -defined {(s address_1)} -defined the carrier of S -valued Function-like one-to-one set
{(s address_1)} --> ((S,g,(s address_1)) + (S,g,(s address_2))) is Relation-like {(s address_1)} -defined the carrier of S -valued {((S,g,(s address_1)) + (S,g,(s address_2)))} -valued Function-like constant non empty V14({(s address_1)}) V18({(s address_1)},{((S,g,(s address_1)) + (S,g,(s address_2)))}) Element of bool [:{(s address_1)},{((S,g,(s address_1)) + (S,g,(s address_2)))}:]
{((S,g,(s address_1)) + (S,g,(s address_2)))} is non empty trivial 1 -element set
[:{(s address_1)},{((S,g,(s address_1)) + (S,g,(s address_2)))}:] is set
bool [:{(s address_1)},{((S,g,(s address_1)) + (S,g,(s address_2)))}:] is set
g +* ((s address_1) .--> ((S,g,(s address_1)) + (S,g,(s address_2)))) is Relation-like Function-like set
(S,(S,g,(s address_1),((S,g,(s address_1)) + (S,g,(s address_2)))),(succ (S,g))) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
(S,g,(s address_1),((S,g,(s address_1)) + (S,g,(s address_2)))) +* (NAT .--> (succ (S,g))) is Relation-like Function-like set
(S,g,(s address_1)) - (S,g,(s address_2)) is Element of the carrier of S
(S,g,(s address_1),((S,g,(s address_1)) - (S,g,(s address_2)))) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
(s address_1) .--> ((S,g,(s address_1)) - (S,g,(s address_2))) is Relation-like K233() -defined {(s address_1)} -defined the carrier of S -valued Function-like one-to-one set
{(s address_1)} --> ((S,g,(s address_1)) - (S,g,(s address_2))) is Relation-like {(s address_1)} -defined the carrier of S -valued {((S,g,(s address_1)) - (S,g,(s address_2)))} -valued Function-like constant non empty V14({(s address_1)}) V18({(s address_1)},{((S,g,(s address_1)) - (S,g,(s address_2)))}) Element of bool [:{(s address_1)},{((S,g,(s address_1)) - (S,g,(s address_2)))}:]
{((S,g,(s address_1)) - (S,g,(s address_2)))} is non empty trivial 1 -element set
[:{(s address_1)},{((S,g,(s address_1)) - (S,g,(s address_2)))}:] is set
bool [:{(s address_1)},{((S,g,(s address_1)) - (S,g,(s address_2)))}:] is set
g +* ((s address_1) .--> ((S,g,(s address_1)) - (S,g,(s address_2)))) is Relation-like Function-like set
(S,(S,g,(s address_1),((S,g,(s address_1)) - (S,g,(s address_2)))),(succ (S,g))) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
(S,g,(s address_1),((S,g,(s address_1)) - (S,g,(s address_2)))) +* (NAT .--> (succ (S,g))) is Relation-like Function-like set
4 is non empty epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
(S,g,(s address_1)) * (S,g,(s address_2)) is Element of the carrier of S
(S,g,(s address_1),((S,g,(s address_1)) * (S,g,(s address_2)))) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
(s address_1) .--> ((S,g,(s address_1)) * (S,g,(s address_2))) is Relation-like K233() -defined {(s address_1)} -defined the carrier of S -valued Function-like one-to-one set
{(s address_1)} --> ((S,g,(s address_1)) * (S,g,(s address_2))) is Relation-like {(s address_1)} -defined the carrier of S -valued {((S,g,(s address_1)) * (S,g,(s address_2)))} -valued Function-like constant non empty V14({(s address_1)}) V18({(s address_1)},{((S,g,(s address_1)) * (S,g,(s address_2)))}) Element of bool [:{(s address_1)},{((S,g,(s address_1)) * (S,g,(s address_2)))}:]
{((S,g,(s address_1)) * (S,g,(s address_2)))} is non empty trivial 1 -element set
[:{(s address_1)},{((S,g,(s address_1)) * (S,g,(s address_2)))}:] is set
bool [:{(s address_1)},{((S,g,(s address_1)) * (S,g,(s address_2)))}:] is set
g +* ((s address_1) .--> ((S,g,(s address_1)) * (S,g,(s address_2)))) is Relation-like Function-like set
(S,(S,g,(s address_1),((S,g,(s address_1)) * (S,g,(s address_2)))),(succ (S,g))) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
(S,g,(s address_1),((S,g,(s address_1)) * (S,g,(s address_2)))) +* (NAT .--> (succ (S,g))) is Relation-like Function-like set
6 is non empty epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
s jump_address is epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
(S,g,(s jump_address)) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
NAT .--> (s jump_address) is Relation-like {NAT} -defined NAT -valued Function-like one-to-one Cardinal-yielding set
{NAT} --> (s jump_address) is Relation-like {NAT} -defined NAT -valued {(s jump_address)} -valued Function-like constant non empty V14({NAT}) V18({NAT},{(s jump_address)}) Cardinal-yielding V132() Element of bool [:{NAT},{(s jump_address)}:]
{(s jump_address)} is non empty trivial 1 -element set
[:{NAT},{(s jump_address)}:] is set
bool [:{NAT},{(s jump_address)}:] is set
g +* (NAT .--> (s jump_address)) is Relation-like Function-like set
7 is non empty epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
s cond_address is Element of K233()
(S,g,(s cond_address)) is Element of the carrier of S
0. S is V48(S) Element of the carrier of S
s cjump_address is epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
IFEQ ((S,g,(s cond_address)),(0. S),(s cjump_address),(succ (S,g))) is epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable set
(S,g,(IFEQ ((S,g,(s cond_address)),(0. S),(s cjump_address),(succ (S,g))))) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
NAT .--> (IFEQ ((S,g,(s cond_address)),(0. S),(s cjump_address),(succ (S,g)))) is Relation-like {NAT} -defined Function-like one-to-one Cardinal-yielding set
{NAT} --> (IFEQ ((S,g,(s cond_address)),(0. S),(s cjump_address),(succ (S,g)))) is Relation-like {NAT} -defined {(IFEQ ((S,g,(s cond_address)),(0. S),(s cjump_address),(succ (S,g))))} -valued Function-like constant non empty V14({NAT}) V18({NAT},{(IFEQ ((S,g,(s cond_address)),(0. S),(s cjump_address),(succ (S,g))))}) Cardinal-yielding V132() Element of bool [:{NAT},{(IFEQ ((S,g,(s cond_address)),(0. S),(s cjump_address),(succ (S,g))))}:]
{(IFEQ ((S,g,(s cond_address)),(0. S),(s cjump_address),(succ (S,g))))} is non empty trivial 1 -element set
[:{NAT},{(IFEQ ((S,g,(s cond_address)),(0. S),(s cjump_address),(succ (S,g))))}:] is set
bool [:{NAT},{(IFEQ ((S,g,(s cond_address)),(0. S),(s cjump_address),(succ (S,g))))}:] is set
g +* (NAT .--> (IFEQ ((S,g,(s cond_address)),(0. S),(s cjump_address),(succ (S,g))))) is Relation-like Function-like set
5 is non empty epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
s const_address is Element of K233()
s const_value is Element of the carrier of S
(S,g,(s const_address),(s const_value)) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
(s const_address) .--> (s const_value) is Relation-like K233() -defined {(s const_address)} -defined the carrier of S -valued Function-like one-to-one set
{(s const_address)} is non empty trivial 1 -element set
{(s const_address)} --> (s const_value) is Relation-like {(s const_address)} -defined the carrier of S -valued {(s const_value)} -valued Function-like constant non empty V14({(s const_address)}) V18({(s const_address)},{(s const_value)}) Element of bool [:{(s const_address)},{(s const_value)}:]
{(s const_value)} is non empty trivial 1 -element set
[:{(s const_address)},{(s const_value)}:] is set
bool [:{(s const_address)},{(s const_value)}:] is set
g +* ((s const_address) .--> (s const_value)) is Relation-like Function-like set
(S,(S,g,(s const_address),(s const_value)),(succ (S,g))) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
(S,g,(s const_address),(s const_value)) +* (NAT .--> (succ (S,g))) is Relation-like Function-like set
x is Element of SCM-Data-Loc
gx is Element of SCM-Data-Loc
<*x,gx*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*x*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,x] is V15() set
{1,x} is non empty set
{{1,x},{1}} is non empty set
{[1,x]} is Function-like non empty trivial 1 -element set
<*gx*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,gx] is V15() set
{1,gx} is non empty set
{{1,gx},{1}} is non empty set
{[1,gx]} is Function-like non empty trivial 1 -element set
K109(<*x*>,<*gx*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[1,{},<*x,gx*>] is V15() V16() set
[1,{}] is V15() set
{1,{}} is non empty set
{{1,{}},{1}} is non empty set
[[1,{}],<*x,gx*>] is V15() set
{[1,{}],<*x,gx*>} is non empty set
{[1,{}]} is Function-like non empty trivial 1 -element set
{{[1,{}],<*x,gx*>},{[1,{}]}} is non empty set
fx is Element of SCM-Data-Loc
y is Element of SCM-Data-Loc
<*fx,y*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*fx*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,fx] is V15() set
{1,fx} is non empty set
{{1,fx},{1}} is non empty set
{[1,fx]} is Function-like non empty trivial 1 -element set
<*y*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,y] is V15() set
{1,y} is non empty set
{{1,y},{1}} is non empty set
{[1,y]} is Function-like non empty trivial 1 -element set
K109(<*fx*>,<*y*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[2,{},<*fx,y*>] is V15() V16() set
[2,{}] is V15() set
{2,{}} is non empty set
{2} is non empty trivial 1 -element set
{{2,{}},{2}} is non empty set
[[2,{}],<*fx,y*>] is V15() set
{[2,{}],<*fx,y*>} is non empty set
{[2,{}]} is Function-like non empty trivial 1 -element set
{{[2,{}],<*fx,y*>},{[2,{}]}} is non empty set
c₈ is Element of SCM-Data-Loc
c₉ is Element of SCM-Data-Loc
<*c₈,c₉*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*c₈*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₈] is V15() set
{1,c₈} is non empty set
{{1,c₈},{1}} is non empty set
{[1,c₈]} is Function-like non empty trivial 1 -element set
<*c₉*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₉] is V15() set
{1,c₉} is non empty set
{{1,c₉},{1}} is non empty set
{[1,c₉]} is Function-like non empty trivial 1 -element set
K109(<*c₈*>,<*c₉*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[3,{},<*c₈,c₉*>] is V15() V16() set
[3,{}] is V15() set
{3,{}} is non empty set
{3} is non empty trivial 1 -element set
{{3,{}},{3}} is non empty set
[[3,{}],<*c₈,c₉*>] is V15() set
{[3,{}],<*c₈,c₉*>} is non empty set
{[3,{}]} is Function-like non empty trivial 1 -element set
{{[3,{}],<*c₈,c₉*>},{[3,{}]}} is non empty set
c₁₀ is Element of SCM-Data-Loc
c₁₁ is Element of SCM-Data-Loc
<*c₁₀,c₁₁*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*c₁₀*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₁₀] is V15() set
{1,c₁₀} is non empty set
{{1,c₁₀},{1}} is non empty set
{[1,c₁₀]} is Function-like non empty trivial 1 -element set
<*c₁₁*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₁₁] is V15() set
{1,c₁₁} is non empty set
{{1,c₁₁},{1}} is non empty set
{[1,c₁₁]} is Function-like non empty trivial 1 -element set
K109(<*c₁₀*>,<*c₁₁*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[4,{},<*c₁₀,c₁₁*>] is V15() V16() set
[4,{}] is V15() set
{4,{}} is non empty set
{4} is non empty trivial 1 -element set
{{4,{}},{4}} is non empty set
[[4,{}],<*c₁₀,c₁₁*>] is V15() set
{[4,{}],<*c₁₀,c₁₁*>} is non empty set
{[4,{}]} is Function-like non empty trivial 1 -element set
{{[4,{}],<*c₁₀,c₁₁*>},{[4,{}]}} is non empty set
c₁₂ is epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
<*c₁₂*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
[1,c₁₂] is V15() set
{1,c₁₂} is non empty set
{{1,c₁₂},{1}} is non empty set
{[1,c₁₂]} is Function-like non empty trivial 1 -element set
[6,<*c₁₂*>,{}] is V15() V16() set
[6,<*c₁₂*>] is V15() set
{6,<*c₁₂*>} is non empty set
{6} is non empty trivial 1 -element set
{{6,<*c₁₂*>},{6}} is non empty set
[[6,<*c₁₂*>],{}] is V15() set
{[6,<*c₁₂*>],{}} is non empty set
{[6,<*c₁₂*>]} is Function-like non empty trivial 1 -element set
{{[6,<*c₁₂*>],{}},{[6,<*c₁₂*>]}} is non empty set
c₁₃ is epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
<*c₁₃*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
[1,c₁₃] is V15() set
{1,c₁₃} is non empty set
{{1,c₁₃},{1}} is non empty set
{[1,c₁₃]} is Function-like non empty trivial 1 -element set
c₁₄ is Element of SCM-Data-Loc
<*c₁₄*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of SCM-Data-Loc
[1,c₁₄] is V15() set
{1,c₁₄} is non empty set
{{1,c₁₄},{1}} is non empty set
{[1,c₁₄]} is Function-like non empty trivial 1 -element set
[7,<*c₁₃*>,<*c₁₄*>] is V15() V16() set
[7,<*c₁₃*>] is V15() set
{7,<*c₁₃*>} is non empty set
{7} is non empty trivial 1 -element set
{{7,<*c₁₃*>},{7}} is non empty set
[[7,<*c₁₃*>],<*c₁₄*>] is V15() set
{[7,<*c₁₃*>],<*c₁₄*>} is non empty set
{[7,<*c₁₃*>]} is Function-like non empty trivial 1 -element set
{{[7,<*c₁₃*>],<*c₁₄*>},{[7,<*c₁₃*>]}} is non empty set
c₁₅ is Element of SCM-Data-Loc
c₁₆ is Element of the carrier of S
(S,c₁₅,c₁₆) is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of S -valued Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable FinSequence of SCM-Data-Loc \/ the carrier of S
SCM-Data-Loc \/ the carrier of S is non empty set
<*c₁₅*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₁₅] is V15() set
{1,c₁₅} is non empty set
{{1,c₁₅},{1}} is non empty set
{[1,c₁₅]} is Function-like non empty trivial 1 -element set
<*c₁₆*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₁₆] is V15() set
{1,c₁₆} is non empty set
{{1,c₁₆},{1}} is non empty set
{[1,c₁₆]} is Function-like non empty trivial 1 -element set
K109(<*c₁₅*>,<*c₁₆*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[5,{},(S,c₁₅,c₁₆)] is V15() V16() set
[5,{}] is V15() set
{5,{}} is non empty set
{5} is non empty trivial 1 -element set
{{5,{}},{5}} is non empty set
[[5,{}],(S,c₁₅,c₁₆)] is V15() set
{[5,{}],(S,c₁₅,c₁₆)} is non empty set
{[5,{}]} is Function-like non empty trivial 1 -element set
{{[5,{}],(S,c₁₅,c₁₆)},{[5,{}]}} is non empty set
gx is Element of SCM-Data-Loc
fx is Element of SCM-Data-Loc
<*gx,fx*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*gx*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,gx] is V15() set
{1,gx} is non empty set
{{1,gx},{1}} is non empty set
{[1,gx]} is Function-like non empty trivial 1 -element set
<*fx*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,fx] is V15() set
{1,fx} is non empty set
{{1,fx},{1}} is non empty set
{[1,fx]} is Function-like non empty trivial 1 -element set
K109(<*gx*>,<*fx*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[1,{},<*gx,fx*>] is V15() V16() set
[1,{}] is V15() set
{1,{}} is non empty set
{{1,{}},{1}} is non empty set
[[1,{}],<*gx,fx*>] is V15() set
{[1,{}],<*gx,fx*>} is non empty set
{[1,{}]} is Function-like non empty trivial 1 -element set
{{[1,{}],<*gx,fx*>},{[1,{}]}} is non empty set
y is Element of SCM-Data-Loc
c₈ is Element of SCM-Data-Loc
<*y,c₈*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*y*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,y] is V15() set
{1,y} is non empty set
{{1,y},{1}} is non empty set
{[1,y]} is Function-like non empty trivial 1 -element set
<*c₈*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₈] is V15() set
{1,c₈} is non empty set
{{1,c₈},{1}} is non empty set
{[1,c₈]} is Function-like non empty trivial 1 -element set
K109(<*y*>,<*c₈*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[2,{},<*y,c₈*>] is V15() V16() set
[2,{}] is V15() set
{2,{}} is non empty set
{2} is non empty trivial 1 -element set
{{2,{}},{2}} is non empty set
[[2,{}],<*y,c₈*>] is V15() set
{[2,{}],<*y,c₈*>} is non empty set
{[2,{}]} is Function-like non empty trivial 1 -element set
{{[2,{}],<*y,c₈*>},{[2,{}]}} is non empty set
x is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
c₁₀ is Element of SCM-Data-Loc
c₁₁ is Element of SCM-Data-Loc
<*c₁₀,c₁₁*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*c₁₀*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₁₀] is V15() set
{1,c₁₀} is non empty set
{{1,c₁₀},{1}} is non empty set
{[1,c₁₀]} is Function-like non empty trivial 1 -element set
<*c₁₁*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₁₁] is V15() set
{1,c₁₁} is non empty set
{{1,c₁₁},{1}} is non empty set
{[1,c₁₁]} is Function-like non empty trivial 1 -element set
K109(<*c₁₀*>,<*c₁₁*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[1,{},<*c₁₀,c₁₁*>] is V15() V16() set
[[1,{}],<*c₁₀,c₁₁*>] is V15() set
{[1,{}],<*c₁₀,c₁₁*>} is non empty set
{{[1,{}],<*c₁₀,c₁₁*>},{[1,{}]}} is non empty set
c₁₂ is Element of SCM-Data-Loc
c₁₃ is Element of SCM-Data-Loc
<*c₁₂,c₁₃*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*c₁₂*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₁₂] is V15() set
{1,c₁₂} is non empty set
{{1,c₁₂},{1}} is non empty set
{[1,c₁₂]} is Function-like non empty trivial 1 -element set
<*c₁₃*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₁₃] is V15() set
{1,c₁₃} is non empty set
{{1,c₁₃},{1}} is non empty set
{[1,c₁₃]} is Function-like non empty trivial 1 -element set
K109(<*c₁₂*>,<*c₁₃*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[3,{},<*c₁₂,c₁₃*>] is V15() V16() set
[3,{}] is V15() set
{3,{}} is non empty set
{3} is non empty trivial 1 -element set
{{3,{}},{3}} is non empty set
[[3,{}],<*c₁₂,c₁₃*>] is V15() set
{[3,{}],<*c₁₂,c₁₃*>} is non empty set
{[3,{}]} is Function-like non empty trivial 1 -element set
{{[3,{}],<*c₁₂,c₁₃*>},{[3,{}]}} is non empty set
c₉ is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
c₁₅ is Element of SCM-Data-Loc
c₁₆ is Element of SCM-Data-Loc
<*c₁₅,c₁₆*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*c₁₅*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₁₅] is V15() set
{1,c₁₅} is non empty set
{{1,c₁₅},{1}} is non empty set
{[1,c₁₅]} is Function-like non empty trivial 1 -element set
<*c₁₆*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₁₆] is V15() set
{1,c₁₆} is non empty set
{{1,c₁₆},{1}} is non empty set
{[1,c₁₆]} is Function-like non empty trivial 1 -element set
K109(<*c₁₅*>,<*c₁₆*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[1,{},<*c₁₅,c₁₆*>] is V15() V16() set
[[1,{}],<*c₁₅,c₁₆*>] is V15() set
{[1,{}],<*c₁₅,c₁₆*>} is non empty set
{{[1,{}],<*c₁₅,c₁₆*>},{[1,{}]}} is non empty set
c₁₇ is Element of SCM-Data-Loc
c₁₈ is Element of SCM-Data-Loc
<*c₁₇,c₁₈*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*c₁₇*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₁₇] is V15() set
{1,c₁₇} is non empty set
{{1,c₁₇},{1}} is non empty set
{[1,c₁₇]} is Function-like non empty trivial 1 -element set
<*c₁₈*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₁₈] is V15() set
{1,c₁₈} is non empty set
{{1,c₁₈},{1}} is non empty set
{[1,c₁₈]} is Function-like non empty trivial 1 -element set
K109(<*c₁₇*>,<*c₁₈*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[4,{},<*c₁₇,c₁₈*>] is V15() V16() set
[4,{}] is V15() set
{4,{}} is non empty set
{4} is non empty trivial 1 -element set
{{4,{}},{4}} is non empty set
[[4,{}],<*c₁₇,c₁₈*>] is V15() set
{[4,{}],<*c₁₇,c₁₈*>} is non empty set
{[4,{}]} is Function-like non empty trivial 1 -element set
{{[4,{}],<*c₁₇,c₁₈*>},{[4,{}]}} is non empty set
c₁₄ is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
c₂₀ is Element of SCM-Data-Loc
c₂₁ is Element of SCM-Data-Loc
<*c₂₀,c₂₁*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*c₂₀*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₂₀] is V15() set
{1,c₂₀} is non empty set
{{1,c₂₀},{1}} is non empty set
{[1,c₂₀]} is Function-like non empty trivial 1 -element set
<*c₂₁*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₂₁] is V15() set
{1,c₂₁} is non empty set
{{1,c₂₁},{1}} is non empty set
{[1,c₂₁]} is Function-like non empty trivial 1 -element set
K109(<*c₂₀*>,<*c₂₁*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[1,{},<*c₂₀,c₂₁*>] is V15() V16() set
[[1,{}],<*c₂₀,c₂₁*>] is V15() set
{[1,{}],<*c₂₀,c₂₁*>} is non empty set
{{[1,{}],<*c₂₀,c₂₁*>},{[1,{}]}} is non empty set
c₂₂ is epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
<*c₂₂*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
[1,c₂₂] is V15() set
{1,c₂₂} is non empty set
{{1,c₂₂},{1}} is non empty set
{[1,c₂₂]} is Function-like non empty trivial 1 -element set
[6,<*c₂₂*>,{}] is V15() V16() set
[6,<*c₂₂*>] is V15() set
{6,<*c₂₂*>} is non empty set
{6} is non empty trivial 1 -element set
{{6,<*c₂₂*>},{6}} is non empty set
[[6,<*c₂₂*>],{}] is V15() set
{[6,<*c₂₂*>],{}} is non empty set
{[6,<*c₂₂*>]} is Function-like non empty trivial 1 -element set
{{[6,<*c₂₂*>],{}},{[6,<*c₂₂*>]}} is non empty set
c₁₉ is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
c₂₄ is Element of SCM-Data-Loc
c₂₅ is Element of SCM-Data-Loc
<*c₂₄,c₂₅*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*c₂₄*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₂₄] is V15() set
{1,c₂₄} is non empty set
{{1,c₂₄},{1}} is non empty set
{[1,c₂₄]} is Function-like non empty trivial 1 -element set
<*c₂₅*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₂₅] is V15() set
{1,c₂₅} is non empty set
{{1,c₂₅},{1}} is non empty set
{[1,c₂₅]} is Function-like non empty trivial 1 -element set
K109(<*c₂₄*>,<*c₂₅*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[1,{},<*c₂₄,c₂₅*>] is V15() V16() set
[[1,{}],<*c₂₄,c₂₅*>] is V15() set
{[1,{}],<*c₂₄,c₂₅*>} is non empty set
{{[1,{}],<*c₂₄,c₂₅*>},{[1,{}]}} is non empty set
c₂₆ is epsilon-transitive epsilon-connected ordinal natural V29() cardinal countable Element of NAT
<*c₂₆*> is Relation-like NAT -defined NAT -valued Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of NAT
[1,c₂₆] is V15() set
{1,c₂₆} is non empty set
{{1,c₂₆},{1}} is non empty set
{[1,c₂₆]} is Function-like non empty trivial 1 -element set
c₂₇ is Element of SCM-Data-Loc
<*c₂₇*> is Relation-like NAT -defined SCM-Data-Loc -valued Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable FinSequence of SCM-Data-Loc
[1,c₂₇] is V15() set
{1,c₂₇} is non empty set
{{1,c₂₇},{1}} is non empty set
{[1,c₂₇]} is Function-like non empty trivial 1 -element set
[7,<*c₂₆*>,<*c₂₇*>] is V15() V16() set
[7,<*c₂₆*>] is V15() set
{7,<*c₂₆*>} is non empty set
{7} is non empty trivial 1 -element set
{{7,<*c₂₆*>},{7}} is non empty set
[[7,<*c₂₆*>],<*c₂₇*>] is V15() set
{[7,<*c₂₆*>],<*c₂₇*>} is non empty set
{[7,<*c₂₆*>]} is Function-like non empty trivial 1 -element set
{{[7,<*c₂₆*>],<*c₂₇*>},{[7,<*c₂₆*>]}} is non empty set
c₂₃ is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
c₂₉ is Element of SCM-Data-Loc
c₃₀ is Element of SCM-Data-Loc
<*c₂₉,c₃₀*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*c₂₉*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₂₉] is V15() set
{1,c₂₉} is non empty set
{{1,c₂₉},{1}} is non empty set
{[1,c₂₉]} is Function-like non empty trivial 1 -element set
<*c₃₀*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₃₀] is V15() set
{1,c₃₀} is non empty set
{{1,c₃₀},{1}} is non empty set
{[1,c₃₀]} is Function-like non empty trivial 1 -element set
K109(<*c₂₉*>,<*c₃₀*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[1,{},<*c₂₉,c₃₀*>] is V15() V16() set
[[1,{}],<*c₂₉,c₃₀*>] is V15() set
{[1,{}],<*c₂₉,c₃₀*>} is non empty set
{{[1,{}],<*c₂₉,c₃₀*>},{[1,{}]}} is non empty set
c₃₁ is Element of SCM-Data-Loc
c₃₂ is Element of the carrier of S
(S,c₃₁,c₃₂) is Relation-like NAT -defined SCM-Data-Loc \/ the carrier of S -valued Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable FinSequence of SCM-Data-Loc \/ the carrier of S
SCM-Data-Loc \/ the carrier of S is non empty set
<*c₃₁*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₃₁] is V15() set
{1,c₃₁} is non empty set
{{1,c₃₁},{1}} is non empty set
{[1,c₃₁]} is Function-like non empty trivial 1 -element set
<*c₃₂*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₃₂] is V15() set
{1,c₃₂} is non empty set
{{1,c₃₂},{1}} is non empty set
{[1,c₃₂]} is Function-like non empty trivial 1 -element set
K109(<*c₃₁*>,<*c₃₂*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[5,{},(S,c₃₁,c₃₂)] is V15() V16() set
[5,{}] is V15() set
{5,{}} is non empty set
{5} is non empty trivial 1 -element set
{{5,{}},{5}} is non empty set
[[5,{}],(S,c₃₁,c₃₂)] is V15() set
{[5,{}],(S,c₃₁,c₃₂)} is non empty set
{[5,{}]} is Function-like non empty trivial 1 -element set
{{[5,{}],(S,c₃₁,c₃₂)},{[5,{}]}} is non empty set
c₂₈ is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
c₃₄ is Element of SCM-Data-Loc
c₃₅ is Element of SCM-Data-Loc
<*c₃₄,c₃₅*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*c₃₄*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₃₄] is V15() set
{1,c₃₄} is non empty set
{{1,c₃₄},{1}} is non empty set
{[1,c₃₄]} is Function-like non empty trivial 1 -element set
<*c₃₅*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₃₅] is V15() set
{1,c₃₅} is non empty set
{{1,c₃₅},{1}} is non empty set
{[1,c₃₅]} is Function-like non empty trivial 1 -element set
K109(<*c₃₄*>,<*c₃₅*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[2,{},<*c₃₄,c₃₅*>] is V15() V16() set
[[2,{}],<*c₃₄,c₃₅*>] is V15() set
{[2,{}],<*c₃₄,c₃₅*>} is non empty set
{{[2,{}],<*c₃₄,c₃₅*>},{[2,{}]}} is non empty set
c₃₆ is Element of SCM-Data-Loc
c₃₇ is Element of SCM-Data-Loc
<*c₃₆,c₃₇*> is Relation-like NAT -defined Function-like non empty V29() 2 -element FinSequence-like FinSubsequence-like countable set
<*c₃₆*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₃₆] is V15() set
{1,c₃₆} is non empty set
{{1,c₃₆},{1}} is non empty set
{[1,c₃₆]} is Function-like non empty trivial 1 -element set
<*c₃₇*> is Relation-like NAT -defined Function-like constant non empty trivial V29() 1 -element FinSequence-like FinSubsequence-like countable set
[1,c₃₇] is V15() set
{1,c₃₇} is non empty set
{{1,c₃₇},{1}} is non empty set
{[1,c₃₇]} is Function-like non empty trivial 1 -element set
K109(<*c₃₆*>,<*c₃₇*>) is Relation-like NAT -defined Function-like non empty V29() FinSequence-like FinSubsequence-like countable set
[3,{},<*c₃₆,c₃₇*>] is V15() V16() set
[[3,{}],<*c₃₆,c₃₇*>] is V15() set
{[3,{}],<*c₃₆,c₃₇*>} is non empty set
{{[3,{}],<*c₃₆,c₃₇*>},{[3,{}]}} is non empty set
c₃₃ is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
c₃₉ is Element of SCM-Data-Loc
c₄₀ is Element of SCM-Data-Loc
<*c₃₉,c₄₀*> is Relation-like NAT -defined