:: 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 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
[4,{},<*c₄₁,c₄₂*>] is V15() V16() set
[[4,{}],<*c₄₁,c₄₂*>] is V15() set
{[4,{}],<*c₄₁,c₄₂*>} is non empty 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
[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 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,<*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
[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 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,<*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
[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 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
<*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,{}],(S,c₅₅,c₅₆)] is V15() set
{[5,{}],(S,c₅₅,c₅₆)} is non empty 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
[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 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,{}],<*c₆₀,c₆₁*>] is V15() set
{[4,{}],<*c₆₀,c₆₁*>} is non empty 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
[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 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,<*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
[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 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,<*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
[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 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
<*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,{}],(S,c₇₄,c₇₅)] is V15() set
{[5,{}],(S,c₇₄,c₇₅)} is non empty 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
[4,{},<*c₇₇,c₇₈*>] is V15() V16() set
[[4,{}],<*c₇₇,c₇₈*>] is V15() set
{[4,{}],<*c₇₇,c₇₈*>} is non empty 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,<*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
[4,{},<*c₈₁,c₈₂*>] is V15() V16() set
[[4,{}],<*c₈₁,c₈₂*>] is V15() set
{[4,{}],<*c₈₁,c₈₂*>} is non empty 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
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,<*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
[4,{},<*c₈₆,c₈₇*>] is V15() V16() set
[[4,{}],<*c₈₆,c₈₇*>] is V15() set
{[4,{}],<*c₈₆,c₈₇*>} is non empty set
{{[4,{}],<*c₈₆,c₈₇*>},{[4,{}]}} 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
<*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,{}],(S,c₈₈,c₈₉)] is V15() set
{[5,{}],(S,c₈₈,c₈₉)} is non empty 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 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,<*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,<*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 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,<*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 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
<*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,{}],(S,c₉₆,c₉₇)] is V15() set
{[5,{}],(S,c₉₆,c₉₇)} is non empty 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 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,<*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
<*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,{}],(S,c₁₀₁,c₁₀₂)] is V15() set
{[5,{}],(S,c₁₀₁,c₁₀₂)} is non empty 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))
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
K70((product (SCM-OK * (S))),(product (SCM-OK * (S)))) is functional non empty set
[:(SCM-Instr S),K70((product (SCM-OK * (S))),(product (SCM-OK * (S)))):] is set
bool [:(SCM-Instr S),K70((product (SCM-OK * (S))),(product (SCM-OK * (S)))):] is set
[:(SCM-Instr S),(product (SCM-OK * (S))):] is set
[:[:(SCM-Instr S),(product (SCM-OK * (S))):],(product (SCM-OK * (S))):] is set
bool [:[:(SCM-Instr S),(product (SCM-OK * (S))):],(product (SCM-OK * (S))):] is set
s is Relation-like [:(SCM-Instr S),(product (SCM-OK * (S))):] -defined product (SCM-OK * (S)) -valued Function-like V14([:(SCM-Instr S),(product (SCM-OK * (S))):]) V18([:(SCM-Instr S),(product (SCM-OK * (S))):], product (SCM-OK * (S))) Function-yielding V128() Element of bool [:[:(SCM-Instr S),(product (SCM-OK * (S))):],(product (SCM-OK * (S))):]
curry s is Relation-like SCM-Instr S -defined K78((product (SCM-OK * (S))),(product (SCM-OK * (S)))) -valued Function-like non empty V14( SCM-Instr S) V18( SCM-Instr S,K78((product (SCM-OK * (S))),(product (SCM-OK * (S))))) Function-yielding V128() Element of bool [:(SCM-Instr S),K78((product (SCM-OK * (S))),(product (SCM-OK * (S)))):]
K78((product (SCM-OK * (S))),(product (SCM-OK * (S)))) is functional non empty M4( product (SCM-OK * (S)), product (SCM-OK * (S)))
[:(SCM-Instr S),K78((product (SCM-OK * (S))),(product (SCM-OK * (S)))):] is set
bool [:(SCM-Instr S),K78((product (SCM-OK * (S))),(product (SCM-OK * (S)))):] is set
g is Element of SCM-Instr S
(curry s) . g is Relation-like Function-like Element of K70((product (SCM-OK * (S))),(product (SCM-OK * (S))))
x is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
((curry s) . g) . x is set
(S,g,x) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
(curry s) . g is Relation-like product (SCM-OK * (S)) -defined product (SCM-OK * (S)) -valued Function-like V14( product (SCM-OK * (S))) V18( product (SCM-OK * (S)), product (SCM-OK * (S))) Function-yielding V128() Element of K78((product (SCM-OK * (S))),(product (SCM-OK * (S))))
((curry s) . g) . x is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
s . (g,x) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
s is Relation-like SCM-Instr S -defined K70((product (SCM-OK * (S))),(product (SCM-OK * (S)))) -valued Function-like non empty V14( SCM-Instr S) V18( SCM-Instr S,K70((product (SCM-OK * (S))),(product (SCM-OK * (S))))) Function-yielding V128() Element of bool [:(SCM-Instr S),K70((product (SCM-OK * (S))),(product (SCM-OK * (S)))):]
g is Relation-like SCM-Instr S -defined K70((product (SCM-OK * (S))),(product (SCM-OK * (S)))) -valued Function-like non empty V14( SCM-Instr S) V18( SCM-Instr S,K70((product (SCM-OK * (S))),(product (SCM-OK * (S))))) Function-yielding V128() Element of bool [:(SCM-Instr S),K70((product (SCM-OK * (S))),(product (SCM-OK * (S)))):]
[:(product (SCM-OK * (S))),(product (SCM-OK * (S))):] is set
bool [:(product (SCM-OK * (S))),(product (SCM-OK * (S))):] is set
x is Element of SCM-Instr S
g . x is Relation-like Function-like Element of K70((product (SCM-OK * (S))),(product (SCM-OK * (S))))
s . x is Relation-like Function-like Element of K70((product (SCM-OK * (S))),(product (SCM-OK * (S))))
fx is Relation-like product (SCM-OK * (S)) -defined product (SCM-OK * (S)) -valued Function-like non empty V14( product (SCM-OK * (S))) V18( product (SCM-OK * (S)), product (SCM-OK * (S))) Function-yielding V128() Element of bool [:(product (SCM-OK * (S))),(product (SCM-OK * (S))):]
y is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
fx . y is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
(S,x,y) is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
gx is Relation-like product (SCM-OK * (S)) -defined product (SCM-OK * (S)) -valued Function-like non empty V14( product (SCM-OK * (S))) V18( product (SCM-OK * (S)), product (SCM-OK * (S))) Function-yielding V128() Element of bool [:(product (SCM-OK * (S))),(product (SCM-OK * (S))):]
gx . y is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))
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))
proj1 s is set
proj1 (SCM-OK * (S)) is set