:: 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

c

<*c

<*c

[1,c

{1,c

{{1,c

{[1,c

<*c

[1,c

{1,c

{{1,c

{[1,c

K109(<*c

[3,{},<*c

[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

{[3,{}],<*c

{[3,{}]} is Function-like non empty trivial 1 -element set

{{[3,{}],<*c

c

c

<*c

<*c

[1,c

{1,c

{{1,c

{[1,c

<*c

[1,c

{1,c

{{1,c

{[1,c

K109(<*c

[4,{},<*c

[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

{[4,{}],<*c

{[4,{}]} is Function-like non empty trivial 1 -element set

{{[4,{}],<*c

c

<*c

[1,c

{1,c

{{1,c

{[1,c

[6,<*c

[6,<*c

{6,<*c

{6} is non empty trivial 1 -element set

{{6,<*c

[[6,<*c

{[6,<*c

{[6,<*c

{{[6,<*c

c

<*c

[1,c

{1,c

{{1,c

{[1,c

c

<*c

[1,c

{1,c

{{1,c

{[1,c

[7,<*c

[7,<*c

{7,<*c

{7} is non empty trivial 1 -element set

{{7,<*c

[[7,<*c

{[7,<*c

{[7,<*c

{{[7,<*c

c

c

(S,c

SCM-Data-Loc \/ the carrier of S is non empty set

<*c

[1,c

{1,c

{{1,c

{[1,c

<*c

[1,c

{1,c

{{1,c

{[1,c

K109(<*c

[5,{},(S,c

[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

{[5,{}],(S,c

{[5,{}]} is Function-like non empty trivial 1 -element set

{{[5,{}],(S,c

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

<*y,c

<*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

[1,c

{1,c

{{1,c

{[1,c

K109(<*y*>,<*c

[2,{},<*y,c

[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

{[2,{}],<*y,c

{[2,{}]} is Function-like non empty trivial 1 -element set

{{[2,{}],<*y,c

x is Relation-like Function-like SCM-OK * (S) -compatible Element of product (SCM-OK * (S))

c

c

<*c

<*c

[1,c

{1,c

{{1,c

{[1,c

<*c

[1,c

{1,c

{{1,c

{[1,c

K109(<*c

[1,{},<*c

[[1,{}],<*c

{[1,{}],<*c

{{[1,{}],<*c

c

c

<*c

<*c

[1,c

{1,c

{{1,c

{[1,c

<*c

[1,c

{1,c

{{1,c

{[1,c

K109(<*c

[3,{},<*c

[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

{[3,{}],<*c

{[3,{}]} is Function-like non empty trivial 1 -element set

{{[3,{}],<*c

c

c

c

<*c

<*c

[1,c

{1,c

{{1,c

{[1,c

<*c

[1,c

{1,c

{{1,c

{[1,c

K109(<*c

[1,{},<*c

[[1,{}],<*c

{[1,{}],<*c

{{[1,{}],<*c

c

c

<*c

<*c

[1,c

{1,c

{{1,c

{[1,c

<*c

[1,c

{1,c

{{1,c

{[1,c

K109(<*c

[4,{},<*c

[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

{[4,{}],<*c

{[4,{}]} is Function-like non empty trivial 1 -element set

{{[4,{}],<*c

c

c

c

<*c

<*c

[1,c

{1,c

{{1,c

{[1,c

<*c

[1,c

{1,c

{{1,c

{[1,c

K109(<*c

[1,{},<*c

[[1,{}],<*c

{[1,{}],<*c

{{[1,{}],<*c

c

<*c

[1,c

{1,c

{{1,c

{[1,c

[6,<*c

[6,<*c

{6,<*c

{6} is non empty trivial 1 -element set

{{6,<*c

[[6,<*c

{[6,<*c

{[6,<*c

{{[6,<*c

c

c

c

<*c

<*c

[1,c

{1,c

{{1,c

{[1,c

<*c

[1,c

{1,c

{{1,c

{[1,c

K109(<*c

[1,{},<*c

[[1,{}],<*c

{[1,{}],<*c

{{[1,{}],<*c

c

<*c

[1,c

{1,c

{{1,c

{[1,c

c

<*c

[1,c

{1,c

{{1,c

{[1,c

[7,<*c

[7,<*c

{7,<*c

{7} is non empty trivial 1 -element set

{{7,<*c

[[7,<*c

{[7,<*c

{[7,<*c

{{[7,<*c

c

c

c

<*c

<*c

[1,c

{1,c

{{1,c

{[1,c

<*c

[1,c

{1,c

{{1,c

{[1,c

K109(<*c

[1,{},<*c

[[1,{}],<*c

{[1,{}],<*c

{{[1,{}],<*c

c

c

(S,c

SCM-Data-Loc \/ the carrier of S is non empty set

<*c

[1,c

{1,c

{{1,c

{[1,c

<*c

[1,c

{1,c

{{1,c

{[1,c

K109(<*c

[5,{},(S,c

[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

{[5,{}],(S,c

{[5,{}]} is Function-like non empty trivial 1 -element set

{{[5,{}],(S,c

c

c

c

<*c

<*c

[1,c

{1,c

{{1,c

{[1,c

<*c

[1,c

{1,c

{{1,c

{[1,c

K109(<*c

[2,{},<*c

[[2,{}],<*c

{[2,{}],<*c

{{[2,{}],<*c

c

c

<*c

<*c

[1,c

{1,c

{{1,c

{[1,c

<*c

[1,c

{1,c

{{1,c

{[1,c

K109(<*c

[3,{},<*c

[[3,{}],<*c

{[3,{}],<*c

{{[3,{}],<*c

c

c

c

<*c