:: SCMRING4 semantic presentation

REAL is non empty non trivial non finite non empty-membered set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V37() V38() V127() V128() non empty-membered Element of K24(REAL)

K24(REAL) is non empty non trivial non finite non empty-membered set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V37() V38() V127() V128() non empty-membered set

K24(omega) is non empty non trivial non finite non empty-membered set

K24(NAT) is non empty non trivial non finite non empty-membered set

2 is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() Element of NAT

K25(2,2) is Relation-like non empty finite V127() set

K25(K25(2,2),2) is Relation-like non empty finite V127() set

K24(K25(K25(2,2),2)) is non empty finite V36() V127() set

9 is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() Element of NAT

K107(9) is V127() Element of K24(omega)

K224() is set

SCM-Memory is non empty set

{NAT} is non empty trivial finite V39(1) V127() with_non-empty_elements non empty-membered set

1 is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() Element of NAT

{NAT} \/ K224() is non empty set

K24(SCM-Memory) is non empty set

K25(SCM-Memory,2) is Relation-like non empty set

K24(K25(SCM-Memory,2)) is non empty set

SCM-OK is Relation-like SCM-Memory -defined 2 -valued Function-like non empty total V21( SCM-Memory ,2) Element of K24(K25(SCM-Memory,2))

SCM-VAL is Relation-like 2 -defined Function-like non empty total V204() set

INT is non empty non trivial non finite non empty-membered set

K290(NAT,INT) is set

SCM-OK * SCM-VAL is Relation-like non-empty non empty-yielding SCM-Memory -defined SCM-Memory -defined Function-like non empty total total set

K213((SCM-OK * SCM-VAL)) is functional non empty V125() V126() set

K225() is non empty set

K75(K213((SCM-OK * SCM-VAL)),K213((SCM-OK * SCM-VAL))) is functional non empty set

K25(K225(),K75(K213((SCM-OK * SCM-VAL)),K213((SCM-OK * SCM-VAL)))) is Relation-like non empty set

K24(K25(K225(),K75(K213((SCM-OK * SCM-VAL)),K213((SCM-OK * SCM-VAL))))) is non empty set

SCM is non empty with_non-empty_values IC-Ins-separated strict strict V157(2) IC-recognized CurIns-recognized AMI-Struct over 2

K549(NAT,SCM-Memory) is Element of SCM-Memory

SCM-Exec is Relation-like K225() -defined K75(K213((SCM-OK * SCM-VAL)),K213((SCM-OK * SCM-VAL))) -valued Function-like non empty total V21(K225(),K75(K213((SCM-OK * SCM-VAL)),K213((SCM-OK * SCM-VAL)))) Function-yielding V161() Element of K24(K25(K225(),K75(K213((SCM-OK * SCM-VAL)),K213((SCM-OK * SCM-VAL)))))

AMI-Struct(# SCM-Memory,K549(NAT,SCM-Memory),K225(),SCM-OK,SCM-VAL,SCM-Exec #) is strict AMI-Struct over 2

the InstructionsF of SCM is Relation-like non empty standard-ins V139() J/A-independent V142() set

the carrier of SCM is non empty set

the_Values_of SCM is Relation-like non-empty non empty-yielding the carrier of SCM -defined Function-like non empty total set

the Object-Kind of SCM is Relation-like the carrier of SCM -defined 2 -valued Function-like non empty total V21( the carrier of SCM,2) Element of K24(K25( the carrier of SCM,2))

K25( the carrier of SCM,2) is Relation-like non empty set

K24(K25( the carrier of SCM,2)) is non empty set

the ValuesF of SCM is Relation-like 2 -defined Function-like non empty total V204() set

the Object-Kind of SCM * the ValuesF of SCM is Relation-like the carrier of SCM -defined Function-like non empty total set

COMPLEX is non empty non trivial non finite non empty-membered set

RAT is non empty non trivial non finite non empty-membered set

{} is V1() V3() Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() finite finite-yielding V36() V37() V39( {} ) V103() V124() V127() Function-yielding V161() V170() V203() V204() set

K540() is non empty non trivial non finite strict V113() V222() L11()

the carrier of K540() is non empty non trivial non finite non empty-membered V186() set

K25( the carrier of K540(),NAT) is Relation-like non empty non trivial non finite non empty-membered set

K24(K25( the carrier of K540(),NAT)) is non empty non trivial non finite non empty-membered set

SCM-Data-Loc is Element of K24(SCM-Memory)

0 is V1() V3() Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() finite finite-yielding V36() V37() V39( {} ) V103() V124() V127() Function-yielding V161() V170() V203() V204() Element of NAT

7 is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() Element of NAT

3 is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() Element of NAT

4 is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() Element of NAT

5 is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() Element of NAT

6 is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() Element of NAT

NonZero SCM is non empty non trivial non finite non empty-membered Element of K24( the carrier of SCM)

K24( the carrier of SCM) is non empty set

[#] SCM is non empty non proper Element of K24( the carrier of SCM)

0. SCM is V51( SCM ) Element of the carrier of SCM

the ZeroF of SCM is Element of the carrier of SCM

{(0. SCM)} is non empty trivial finite V39(1) V127() set

([#] SCM) \ {(0. SCM)} is Element of K24( the carrier of SCM)

R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

[1,R] is non empty Element of K25(NAT,NAT)

K25(NAT,NAT) is Relation-like non empty non trivial non finite non empty-membered set

k is non empty non trivial V70() V95() V96() V97() V106() V113() V114() L11()

dl. (k,R) is Int-like Element of the carrier of (SCM k)

SCM k is non empty with_non-empty_values IC-Ins-separated strict V157(2) with_explicit_jumps IC-relocable V208(2) AMI-Struct over 2

the carrier of (SCM k) is non empty set

dl. R is Int-like Element of the carrier of SCM

[1,R] is non empty set

R is non empty non trivial V70() V95() V96() V97() V106() V113() V114() L11()

SCM R is non empty with_non-empty_values IC-Ins-separated strict V157(2) with_explicit_jumps IC-relocable V208(2) AMI-Struct over 2

the carrier of (SCM R) is non empty set

k is Int-like Element of the carrier of (SCM R)

q is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

[1,q] is non empty Element of K25(NAT,NAT)

K25(NAT,NAT) is Relation-like non empty non trivial non finite non empty-membered set

dl. (R,q) is Int-like Element of the carrier of (SCM R)

R is non empty non trivial V70() V95() V96() V97() V106() V113() V114() L11()

k is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

q is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

dl. (R,k) is Int-like Element of the carrier of (SCM R)

SCM R is non empty with_non-empty_values IC-Ins-separated strict V157(2) with_explicit_jumps IC-relocable V208(2) AMI-Struct over 2

the carrier of (SCM R) is non empty set

dl. (R,q) is Int-like Element of the carrier of (SCM R)

[1,q] is non empty Element of K25(NAT,NAT)

K25(NAT,NAT) is Relation-like non empty non trivial non finite non empty-membered set

[1,k] is non empty Element of K25(NAT,NAT)

R is non empty non trivial V70() V95() V96() V97() V106() V113() V114() L11()

SCM R is non empty with_non-empty_values IC-Ins-separated strict V157(2) with_explicit_jumps IC-relocable V208(2) AMI-Struct over 2

the carrier of (SCM R) is non empty set

the_Values_of (SCM R) is Relation-like non-empty non empty-yielding the carrier of (SCM R) -defined Function-like non empty total set

the Object-Kind of (SCM R) is Relation-like the carrier of (SCM R) -defined 2 -valued Function-like non empty total V21( the carrier of (SCM R),2) Element of K24(K25( the carrier of (SCM R),2))

K25( the carrier of (SCM R),2) is Relation-like non empty set

K24(K25( the carrier of (SCM R),2)) is non empty set

the ValuesF of (SCM R) is Relation-like 2 -defined Function-like non empty total V204() set

the Object-Kind of (SCM R) * the ValuesF of (SCM R) is Relation-like the carrier of (SCM R) -defined Function-like non empty total set

k is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

dom k is non empty set

NonZero (SCM R) is Element of K24( the carrier of (SCM R))

K24( the carrier of (SCM R)) is non empty set

[#] (SCM R) is non empty non proper Element of K24( the carrier of (SCM R))

0. (SCM R) is V51( SCM R) Element of the carrier of (SCM R)

the ZeroF of (SCM R) is Element of the carrier of (SCM R)

{(0. (SCM R))} is non empty trivial finite V39(1) V127() set

([#] (SCM R)) \ {(0. (SCM R))} is Element of K24( the carrier of (SCM R))

R is non empty non trivial V70() V95() V96() V97() V106() V113() V114() L11()

SCM R is non empty with_non-empty_values IC-Ins-separated strict V157(2) with_explicit_jumps IC-relocable V208(2) AMI-Struct over 2

the carrier of (SCM R) is non empty set

the_Values_of (SCM R) is Relation-like non-empty non empty-yielding the carrier of (SCM R) -defined Function-like non empty total set

the Object-Kind of (SCM R) is Relation-like the carrier of (SCM R) -defined 2 -valued Function-like non empty total V21( the carrier of (SCM R),2) Element of K24(K25( the carrier of (SCM R),2))

K25( the carrier of (SCM R),2) is Relation-like non empty set

K24(K25( the carrier of (SCM R),2)) is non empty set

the ValuesF of (SCM R) is Relation-like 2 -defined Function-like non empty total V204() set

the Object-Kind of (SCM R) * the ValuesF of (SCM R) is Relation-like the carrier of (SCM R) -defined Function-like non empty total set

k is Int-like Element of the carrier of (SCM R)

q is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

Start-At (q,(SCM R)) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty finite V127() q -started V204() set

0. (SCM R) is V51( SCM R) Element of the carrier of (SCM R)

the ZeroF of (SCM R) is Element of the carrier of (SCM R)

(0. (SCM R)) .--> q is Relation-like the carrier of (SCM R) -defined {(0. (SCM R))} -defined NAT -valued Function-like one-to-one constant non empty trivial finite V39(1) V124() V127() V204() set

{(0. (SCM R))} is non empty trivial finite V39(1) V127() set

{(0. (SCM R))} --> q is Relation-like {(0. (SCM R))} -defined NAT -valued {q} -valued Function-like constant non empty total V21({(0. (SCM R))},{q}) finite V124() V127() V204() Element of K24(K25({(0. (SCM R))},{q}))

{q} is non empty trivial finite V36() V39(1) V127() set

K25({(0. (SCM R))},{q}) is Relation-like non empty finite V127() set

K24(K25({(0. (SCM R))},{q})) is non empty finite V36() V127() set

p is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

p . k is Element of the carrier of R

the carrier of R is non empty non trivial non empty-membered set

p +* (Start-At (q,(SCM R))) is Relation-like the carrier of (SCM R) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible the_Values_of (SCM R) -compatible non empty total q -started set

(p +* (Start-At (q,(SCM R)))) . k is Element of the carrier of R

dom p is non empty set

dom (Start-At (q,(SCM R))) is non empty finite V127() set

{(0. (SCM R))} is non empty trivial finite V39(1) V127() Element of K24( the carrier of (SCM R))

K24( the carrier of (SCM R)) is non empty set

(dom p) \/ (dom (Start-At (q,(SCM R)))) is non empty set

R is non empty non trivial V70() V95() V96() V97() V106() V113() V114() L11()

SCM R is non empty with_non-empty_values IC-Ins-separated strict V157(2) with_explicit_jumps IC-relocable V208(2) AMI-Struct over 2

the carrier of (SCM R) is non empty set

the_Values_of (SCM R) is Relation-like non-empty non empty-yielding the carrier of (SCM R) -defined Function-like non empty total set

the Object-Kind of (SCM R) is Relation-like the carrier of (SCM R) -defined 2 -valued Function-like non empty total V21( the carrier of (SCM R),2) Element of K24(K25( the carrier of (SCM R),2))

K25( the carrier of (SCM R),2) is Relation-like non empty set

K24(K25( the carrier of (SCM R),2)) is non empty set

the ValuesF of (SCM R) is Relation-like 2 -defined Function-like non empty total V204() set

the Object-Kind of (SCM R) * the ValuesF of (SCM R) is Relation-like the carrier of (SCM R) -defined Function-like non empty total set

k is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

IC k is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

0. (SCM R) is V51( SCM R) Element of the carrier of (SCM R)

the ZeroF of (SCM R) is Element of the carrier of (SCM R)

k . (0. (SCM R)) is set

q is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

IC q is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

q . (0. (SCM R)) is set

dom k is non empty set

dom q is non empty set

DataPart k is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible data-only set

NonZero (SCM R) is Element of K24( the carrier of (SCM R))

K24( the carrier of (SCM R)) is non empty set

[#] (SCM R) is non empty non proper Element of K24( the carrier of (SCM R))

{(0. (SCM R))} is non empty trivial finite V39(1) V127() set

([#] (SCM R)) \ {(0. (SCM R))} is Element of K24( the carrier of (SCM R))

k | (NonZero (SCM R)) is Relation-like NonZero (SCM R) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible set

Start-At ((IC k),(SCM R)) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty finite V127() IC k -started V204() set

(0. (SCM R)) .--> (IC k) is Relation-like the carrier of (SCM R) -defined {(0. (SCM R))} -defined NAT -valued Function-like one-to-one constant non empty trivial finite V39(1) V124() V127() V204() set

{(0. (SCM R))} --> (IC k) is Relation-like {(0. (SCM R))} -defined NAT -valued {(IC k)} -valued Function-like constant non empty total V21({(0. (SCM R))},{(IC k)}) finite V124() V127() V204() Element of K24(K25({(0. (SCM R))},{(IC k)}))

{(IC k)} is non empty trivial finite V36() V39(1) V127() set

K25({(0. (SCM R))},{(IC k)}) is Relation-like non empty finite V127() set

K24(K25({(0. (SCM R))},{(IC k)})) is non empty finite V36() V127() set

(DataPart k) +* (Start-At ((IC k),(SCM R))) is Relation-like the carrier of (SCM R) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible the_Values_of (SCM R) -compatible non empty IC k -started set

DataPart q is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible data-only set

q | (NonZero (SCM R)) is Relation-like NonZero (SCM R) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible set

Start-At ((IC q),(SCM R)) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty finite V127() IC q -started V204() set

(0. (SCM R)) .--> (IC q) is Relation-like the carrier of (SCM R) -defined {(0. (SCM R))} -defined NAT -valued Function-like one-to-one constant non empty trivial finite V39(1) V124() V127() V204() set

{(0. (SCM R))} --> (IC q) is Relation-like {(0. (SCM R))} -defined NAT -valued {(IC q)} -valued Function-like constant non empty total V21({(0. (SCM R))},{(IC q)}) finite V124() V127() V204() Element of K24(K25({(0. (SCM R))},{(IC q)}))

{(IC q)} is non empty trivial finite V36() V39(1) V127() set

K25({(0. (SCM R))},{(IC q)}) is Relation-like non empty finite V127() set

K24(K25({(0. (SCM R))},{(IC q)})) is non empty finite V36() V127() set

(DataPart q) +* (Start-At ((IC q),(SCM R))) is Relation-like the carrier of (SCM R) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible the_Values_of (SCM R) -compatible non empty IC q -started set

dom (DataPart k) is set

dom (DataPart q) is set

p is set

(DataPart k) . p is set

(DataPart q) . p is set

k . p is set

q . p is set

R is non empty non trivial V70() V95() V96() V97() V106() V113() V114() L11()

SCM R is non empty with_non-empty_values IC-Ins-separated strict V157(2) with_explicit_jumps IC-relocable V208(2) AMI-Struct over 2

the InstructionsF of (SCM R) is Relation-like non empty standard-ins V139() J/A-independent V142() set

k is with_explicit_jumps IC-relocable Element of the InstructionsF of (SCM R)

the carrier of (SCM R) is non empty set

the_Values_of (SCM R) is Relation-like non-empty non empty-yielding the carrier of (SCM R) -defined Function-like non empty total set

the Object-Kind of (SCM R) is Relation-like the carrier of (SCM R) -defined 2 -valued Function-like non empty total V21( the carrier of (SCM R),2) Element of K24(K25( the carrier of (SCM R),2))

K25( the carrier of (SCM R),2) is Relation-like non empty set

K24(K25( the carrier of (SCM R),2)) is non empty set

the ValuesF of (SCM R) is Relation-like 2 -defined Function-like non empty total V204() set

the Object-Kind of (SCM R) * the ValuesF of (SCM R) is Relation-like the carrier of (SCM R) -defined Function-like non empty total set

q is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() set

p is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() set

q + p is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() set

IncAddr (k,(q + p)) is with_explicit_jumps IC-relocable Element of the InstructionsF of (SCM R)

IncAddr (k,q) is with_explicit_jumps IC-relocable Element of the InstructionsF of (SCM R)

s2 is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

IncIC (s2,p) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

IC s2 is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

0. (SCM R) is V51( SCM R) Element of the carrier of (SCM R)

the ZeroF of (SCM R) is Element of the carrier of (SCM R)

s2 . (0. (SCM R)) is set

(IC s2) + p is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

Start-At (((IC s2) + p),(SCM R)) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty finite V127() (IC s2) + p -started V204() set

(0. (SCM R)) .--> ((IC s2) + p) is Relation-like the carrier of (SCM R) -defined {(0. (SCM R))} -defined NAT -valued Function-like one-to-one constant non empty trivial finite V39(1) V124() V127() V204() set

{(0. (SCM R))} is non empty trivial finite V39(1) V127() set

{(0. (SCM R))} --> ((IC s2) + p) is Relation-like {(0. (SCM R))} -defined NAT -valued {((IC s2) + p)} -valued Function-like constant non empty total V21({(0. (SCM R))},{((IC s2) + p)}) finite V124() V127() V204() Element of K24(K25({(0. (SCM R))},{((IC s2) + p)}))

{((IC s2) + p)} is non empty trivial finite V36() V39(1) V127() set

K25({(0. (SCM R))},{((IC s2) + p)}) is Relation-like non empty finite V127() set

K24(K25({(0. (SCM R))},{((IC s2) + p)})) is non empty finite V36() V127() set

s2 +* (Start-At (((IC s2) + p),(SCM R))) is Relation-like the carrier of (SCM R) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible the_Values_of (SCM R) -compatible non empty total (IC s2) + p -started set

Exec ((IncAddr (k,(q + p))),(IncIC (s2,p))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))) is functional V125() V126() set

K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))) is functional non empty set

the Execution of (SCM R) is Relation-like the InstructionsF of (SCM R) -defined K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))) -valued Function-like non empty total V21( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))) Function-yielding V161() Element of K24(K25( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))))

K25( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))) is Relation-like non empty set

K24(K25( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))))) is non empty set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),(IncAddr (k,(q + p)))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),(IncAddr (k,(q + p)))) . (IncIC (s2,p)) is set

Exec ((IncAddr (k,q)),s2) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),(IncAddr (k,q))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),(IncAddr (k,q))) . s2 is set

IncIC ((Exec ((IncAddr (k,q)),s2)),p) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

IC (Exec ((IncAddr (k,q)),s2)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

(Exec ((IncAddr (k,q)),s2)) . (0. (SCM R)) is set

(IC (Exec ((IncAddr (k,q)),s2))) + p is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

Start-At (((IC (Exec ((IncAddr (k,q)),s2))) + p),(SCM R)) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty finite V127() (IC (Exec ((IncAddr (k,q)),s2))) + p -started V204() set

(0. (SCM R)) .--> ((IC (Exec ((IncAddr (k,q)),s2))) + p) is Relation-like the carrier of (SCM R) -defined {(0. (SCM R))} -defined NAT -valued Function-like one-to-one constant non empty trivial finite V39(1) V124() V127() V204() set

{(0. (SCM R))} --> ((IC (Exec ((IncAddr (k,q)),s2))) + p) is Relation-like {(0. (SCM R))} -defined NAT -valued {((IC (Exec ((IncAddr (k,q)),s2))) + p)} -valued Function-like constant non empty total V21({(0. (SCM R))},{((IC (Exec ((IncAddr (k,q)),s2))) + p)}) finite V124() V127() V204() Element of K24(K25({(0. (SCM R))},{((IC (Exec ((IncAddr (k,q)),s2))) + p)}))

{((IC (Exec ((IncAddr (k,q)),s2))) + p)} is non empty trivial finite V36() V39(1) V127() set

K25({(0. (SCM R))},{((IC (Exec ((IncAddr (k,q)),s2))) + p)}) is Relation-like non empty finite V127() set

K24(K25({(0. (SCM R))},{((IC (Exec ((IncAddr (k,q)),s2))) + p)})) is non empty finite V36() V127() set

(Exec ((IncAddr (k,q)),s2)) +* (Start-At (((IC (Exec ((IncAddr (k,q)),s2))) + p),(SCM R))) is Relation-like the carrier of (SCM R) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible the_Values_of (SCM R) -compatible non empty total (IC (Exec ((IncAddr (k,q)),s2))) + p -started set

s1 is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

IncIC ((Exec ((IncAddr (k,q)),s2)),s1) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

(IC (Exec ((IncAddr (k,q)),s2))) + s1 is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

Start-At (((IC (Exec ((IncAddr (k,q)),s2))) + s1),(SCM R)) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty finite V127() (IC (Exec ((IncAddr (k,q)),s2))) + s1 -started V204() set

(0. (SCM R)) .--> ((IC (Exec ((IncAddr (k,q)),s2))) + s1) is Relation-like the carrier of (SCM R) -defined {(0. (SCM R))} -defined NAT -valued Function-like one-to-one constant non empty trivial finite V39(1) V124() V127() V204() set

{(0. (SCM R))} --> ((IC (Exec ((IncAddr (k,q)),s2))) + s1) is Relation-like {(0. (SCM R))} -defined NAT -valued {((IC (Exec ((IncAddr (k,q)),s2))) + s1)} -valued Function-like constant non empty total V21({(0. (SCM R))},{((IC (Exec ((IncAddr (k,q)),s2))) + s1)}) finite V124() V127() V204() Element of K24(K25({(0. (SCM R))},{((IC (Exec ((IncAddr (k,q)),s2))) + s1)}))

{((IC (Exec ((IncAddr (k,q)),s2))) + s1)} is non empty trivial finite V36() V39(1) V127() set

K25({(0. (SCM R))},{((IC (Exec ((IncAddr (k,q)),s2))) + s1)}) is Relation-like non empty finite V127() set

K24(K25({(0. (SCM R))},{((IC (Exec ((IncAddr (k,q)),s2))) + s1)})) is non empty finite V36() V127() set

(Exec ((IncAddr (k,q)),s2)) +* (Start-At (((IC (Exec ((IncAddr (k,q)),s2))) + s1),(SCM R))) is Relation-like the carrier of (SCM R) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible the_Values_of (SCM R) -compatible non empty total (IC (Exec ((IncAddr (k,q)),s2))) + s1 -started set

IC (IncIC ((Exec ((IncAddr (k,q)),s2)),s1)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

(IncIC ((Exec ((IncAddr (k,q)),s2)),s1)) . (0. (SCM R)) is set

q + s1 is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

IncAddr (k,(q + s1)) is with_explicit_jumps IC-relocable Element of the InstructionsF of (SCM R)

IncIC (s2,s1) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

(IC s2) + s1 is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

Start-At (((IC s2) + s1),(SCM R)) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty finite V127() (IC s2) + s1 -started V204() set

(0. (SCM R)) .--> ((IC s2) + s1) is Relation-like the carrier of (SCM R) -defined {(0. (SCM R))} -defined NAT -valued Function-like one-to-one constant non empty trivial finite V39(1) V124() V127() V204() set

{(0. (SCM R))} --> ((IC s2) + s1) is Relation-like {(0. (SCM R))} -defined NAT -valued {((IC s2) + s1)} -valued Function-like constant non empty total V21({(0. (SCM R))},{((IC s2) + s1)}) finite V124() V127() V204() Element of K24(K25({(0. (SCM R))},{((IC s2) + s1)}))

{((IC s2) + s1)} is non empty trivial finite V36() V39(1) V127() set

K25({(0. (SCM R))},{((IC s2) + s1)}) is Relation-like non empty finite V127() set

K24(K25({(0. (SCM R))},{((IC s2) + s1)})) is non empty finite V36() V127() set

s2 +* (Start-At (((IC s2) + s1),(SCM R))) is Relation-like the carrier of (SCM R) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible the_Values_of (SCM R) -compatible non empty total (IC s2) + s1 -started set

Exec ((IncAddr (k,(q + s1))),(IncIC (s2,s1))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),(IncAddr (k,(q + s1)))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),(IncAddr (k,(q + s1)))) . (IncIC (s2,s1)) is set

IC (Exec ((IncAddr (k,(q + s1))),(IncIC (s2,s1)))) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

(Exec ((IncAddr (k,(q + s1))),(IncIC (s2,s1)))) . (0. (SCM R)) is set

InsCode k is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM R)

InsCodes the InstructionsF of (SCM R) is non empty set

K55( the InstructionsF of (SCM R)) is set

halt (SCM R) is ins-loc-free V156(2, SCM R) V156(2, SCM R) with_explicit_jumps IC-relocable V207(2, SCM R) Element of the InstructionsF of (SCM R)

halt the InstructionsF of (SCM R) is ins-loc-free with_explicit_jumps IC-relocable Element of the InstructionsF of (SCM R)

K47(0,{},{}) is set

InsCode k is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM R)

InsCodes the InstructionsF of (SCM R) is non empty set

K55( the InstructionsF of (SCM R)) is set

P1 is Int-like Element of the carrier of (SCM R)

P2 is Int-like Element of the carrier of (SCM R)

P1 := P2 is ins-loc-free V156(2, SCM R) with_explicit_jumps IC-relocable V207(2, SCM R) V209(2, SCM R) Element of the InstructionsF of (SCM R)

s is Int-like Element of the carrier of (SCM R)

(Exec ((IncAddr (k,(q + s1))),(IncIC (s2,s1)))) . s is Element of the carrier of R

the carrier of R is non empty non trivial non empty-membered set

Exec (k,(IncIC (s2,s1))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . (IncIC (s2,s1)) is set

(Exec (k,(IncIC (s2,s1)))) . s is Element of the carrier of R

(IncIC (s2,s1)) . P2 is Element of the carrier of R

s2 . P2 is Element of the carrier of R

Exec (k,s2) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . s2 is set

(Exec (k,s2)) . s is Element of the carrier of R

(Exec ((IncAddr (k,q)),s2)) . s is Element of the carrier of R

(IncIC ((Exec ((IncAddr (k,q)),s2)),s1)) . s is Element of the carrier of R

s is Int-like Element of the carrier of (SCM R)

(Exec ((IncAddr (k,(q + s1))),(IncIC (s2,s1)))) . s is Element of the carrier of R

the carrier of R is non empty non trivial non empty-membered set

Exec (k,(IncIC (s2,s1))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . (IncIC (s2,s1)) is set

(Exec (k,(IncIC (s2,s1)))) . s is Element of the carrier of R

(IncIC (s2,s1)) . s is Element of the carrier of R

s2 . s is Element of the carrier of R

Exec (k,s2) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . s2 is set

(Exec (k,s2)) . s is Element of the carrier of R

(Exec ((IncAddr (k,q)),s2)) . s is Element of the carrier of R

(IncIC ((Exec ((IncAddr (k,q)),s2)),s1)) . s is Element of the carrier of R

s is Int-like Element of the carrier of (SCM R)

InsCode k is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM R)

InsCodes the InstructionsF of (SCM R) is non empty set

K55( the InstructionsF of (SCM R)) is set

P1 is Int-like Element of the carrier of (SCM R)

P2 is Int-like Element of the carrier of (SCM R)

AddTo (P1,P2) is ins-loc-free V156(2, SCM R) with_explicit_jumps IC-relocable V207(2, SCM R) V209(2, SCM R) Element of the InstructionsF of (SCM R)

s is Int-like Element of the carrier of (SCM R)

(Exec ((IncAddr (k,(q + s1))),(IncIC (s2,s1)))) . s is Element of the carrier of R

the carrier of R is non empty non trivial non empty-membered set

Exec (k,(IncIC (s2,s1))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . (IncIC (s2,s1)) is set

(Exec (k,(IncIC (s2,s1)))) . s is Element of the carrier of R

(IncIC (s2,s1)) . P1 is Element of the carrier of R

(IncIC (s2,s1)) . P2 is Element of the carrier of R

((IncIC (s2,s1)) . P1) + ((IncIC (s2,s1)) . P2) is Element of the carrier of R

s2 . P1 is Element of the carrier of R

(s2 . P1) + ((IncIC (s2,s1)) . P2) is Element of the carrier of R

s2 . P2 is Element of the carrier of R

(s2 . P1) + (s2 . P2) is Element of the carrier of R

Exec (k,s2) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . s2 is set

(Exec (k,s2)) . s is Element of the carrier of R

(Exec ((IncAddr (k,q)),s2)) . s is Element of the carrier of R

(IncIC ((Exec ((IncAddr (k,q)),s2)),s1)) . s is Element of the carrier of R

s is Int-like Element of the carrier of (SCM R)

(Exec ((IncAddr (k,(q + s1))),(IncIC (s2,s1)))) . s is Element of the carrier of R

the carrier of R is non empty non trivial non empty-membered set

Exec (k,(IncIC (s2,s1))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . (IncIC (s2,s1)) is set

(Exec (k,(IncIC (s2,s1)))) . s is Element of the carrier of R

(IncIC (s2,s1)) . s is Element of the carrier of R

s2 . s is Element of the carrier of R

Exec (k,s2) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . s2 is set

(Exec (k,s2)) . s is Element of the carrier of R

(Exec ((IncAddr (k,q)),s2)) . s is Element of the carrier of R

(IncIC ((Exec ((IncAddr (k,q)),s2)),s1)) . s is Element of the carrier of R

s is Int-like Element of the carrier of (SCM R)

InsCode k is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM R)

InsCodes the InstructionsF of (SCM R) is non empty set

K55( the InstructionsF of (SCM R)) is set

P1 is Int-like Element of the carrier of (SCM R)

P2 is Int-like Element of the carrier of (SCM R)

SubFrom (P1,P2) is ins-loc-free V156(2, SCM R) with_explicit_jumps IC-relocable V207(2, SCM R) V209(2, SCM R) Element of the InstructionsF of (SCM R)

s is Int-like Element of the carrier of (SCM R)

(Exec ((IncAddr (k,(q + s1))),(IncIC (s2,s1)))) . s is Element of the carrier of R

the carrier of R is non empty non trivial non empty-membered set

Exec (k,(IncIC (s2,s1))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . (IncIC (s2,s1)) is set

(Exec (k,(IncIC (s2,s1)))) . s is Element of the carrier of R

(IncIC (s2,s1)) . P1 is Element of the carrier of R

(IncIC (s2,s1)) . P2 is Element of the carrier of R

((IncIC (s2,s1)) . P1) - ((IncIC (s2,s1)) . P2) is Element of the carrier of R

s2 . P1 is Element of the carrier of R

(s2 . P1) - ((IncIC (s2,s1)) . P2) is Element of the carrier of R

s2 . P2 is Element of the carrier of R

(s2 . P1) - (s2 . P2) is Element of the carrier of R

Exec (k,s2) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . s2 is set

(Exec (k,s2)) . s is Element of the carrier of R

(Exec ((IncAddr (k,q)),s2)) . s is Element of the carrier of R

(IncIC ((Exec ((IncAddr (k,q)),s2)),s1)) . s is Element of the carrier of R

s is Int-like Element of the carrier of (SCM R)

(Exec ((IncAddr (k,(q + s1))),(IncIC (s2,s1)))) . s is Element of the carrier of R

the carrier of R is non empty non trivial non empty-membered set

Exec (k,(IncIC (s2,s1))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . (IncIC (s2,s1)) is set

(Exec (k,(IncIC (s2,s1)))) . s is Element of the carrier of R

(IncIC (s2,s1)) . s is Element of the carrier of R

s2 . s is Element of the carrier of R

Exec (k,s2) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . s2 is set

(Exec (k,s2)) . s is Element of the carrier of R

(Exec ((IncAddr (k,q)),s2)) . s is Element of the carrier of R

(IncIC ((Exec ((IncAddr (k,q)),s2)),s1)) . s is Element of the carrier of R

s is Int-like Element of the carrier of (SCM R)

InsCode k is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM R)

InsCodes the InstructionsF of (SCM R) is non empty set

K55( the InstructionsF of (SCM R)) is set

P1 is Int-like Element of the carrier of (SCM R)

P2 is Int-like Element of the carrier of (SCM R)

MultBy (P1,P2) is ins-loc-free V156(2, SCM R) with_explicit_jumps IC-relocable V207(2, SCM R) V209(2, SCM R) Element of the InstructionsF of (SCM R)

s is Int-like Element of the carrier of (SCM R)

(Exec ((IncAddr (k,(q + s1))),(IncIC (s2,s1)))) . s is Element of the carrier of R

the carrier of R is non empty non trivial non empty-membered set

Exec (k,(IncIC (s2,s1))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . (IncIC (s2,s1)) is set

(Exec (k,(IncIC (s2,s1)))) . s is Element of the carrier of R

(IncIC (s2,s1)) . P1 is Element of the carrier of R

(IncIC (s2,s1)) . P2 is Element of the carrier of R

((IncIC (s2,s1)) . P1) * ((IncIC (s2,s1)) . P2) is Element of the carrier of R

s2 . P1 is Element of the carrier of R

(s2 . P1) * ((IncIC (s2,s1)) . P2) is Element of the carrier of R

s2 . P2 is Element of the carrier of R

(s2 . P1) * (s2 . P2) is Element of the carrier of R

Exec (k,s2) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . s2 is set

(Exec (k,s2)) . s is Element of the carrier of R

(Exec ((IncAddr (k,q)),s2)) . s is Element of the carrier of R

(IncIC ((Exec ((IncAddr (k,q)),s2)),s1)) . s is Element of the carrier of R

s is Int-like Element of the carrier of (SCM R)

(Exec ((IncAddr (k,(q + s1))),(IncIC (s2,s1)))) . s is Element of the carrier of R

the carrier of R is non empty non trivial non empty-membered set

Exec (k,(IncIC (s2,s1))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . (IncIC (s2,s1)) is set

(Exec (k,(IncIC (s2,s1)))) . s is Element of the carrier of R

(IncIC (s2,s1)) . s is Element of the carrier of R

s2 . s is Element of the carrier of R

Exec (k,s2) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . s2 is set

(Exec (k,s2)) . s is Element of the carrier of R

(Exec ((IncAddr (k,q)),s2)) . s is Element of the carrier of R

(IncIC ((Exec ((IncAddr (k,q)),s2)),s1)) . s is Element of the carrier of R

s is Int-like Element of the carrier of (SCM R)

InsCode k is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM R)

InsCodes the InstructionsF of (SCM R) is non empty set

K55( the InstructionsF of (SCM R)) is set

the carrier of R is non empty non trivial non empty-membered set

P1 is Int-like Element of the carrier of (SCM R)

P2 is Element of the carrier of R

P1 := P2 is ins-loc-free V156(2, SCM R) with_explicit_jumps IC-relocable V207(2, SCM R) V209(2, SCM R) Element of the InstructionsF of (SCM R)

s is Int-like Element of the carrier of (SCM R)

(Exec ((IncAddr (k,(q + s1))),(IncIC (s2,s1)))) . s is Element of the carrier of R

Exec (k,(IncIC (s2,s1))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . (IncIC (s2,s1)) is set

(Exec (k,(IncIC (s2,s1)))) . s is Element of the carrier of R

Exec (k,s2) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . s2 is set

(Exec (k,s2)) . s is Element of the carrier of R

(Exec ((IncAddr (k,q)),s2)) . s is Element of the carrier of R

(IncIC ((Exec ((IncAddr (k,q)),s2)),s1)) . s is Element of the carrier of R

s is Int-like Element of the carrier of (SCM R)

(Exec ((IncAddr (k,(q + s1))),(IncIC (s2,s1)))) . s is Element of the carrier of R

Exec (k,(IncIC (s2,s1))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))))

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . (IncIC (s2,s1)) is set

(Exec (k,(IncIC (s2,s1)))) . s is Element of the carrier of R

(IncIC (s2,s1)) . s is Element of the carrier of R

s2 . s is Element of the carrier of R

Exec (k,s2) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

K77( the InstructionsF of (SCM R),K75(K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R))),K213(( the Object-Kind of (SCM R) * the ValuesF of (SCM R)))), the Execution of (SCM R),k) . s2 is set

(Exec (k,s2)) . s is Element of the carrier of R

(Exec ((IncAddr (k,q)),s2)) . s is Element of the carrier of R

(IncIC ((Exec ((IncAddr (k,q)),s2)),s1)) . s is Element of the carrier of R

s is Int-like Element of the carrier of (SCM R)

InsCode k is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM R)

InsCodes the InstructionsF of (SCM R) is non empty set

K55( the InstructionsF of (SCM R)) is set

P1 is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

goto (P1,R) is non ins-loc-free V156(2, SCM R) with_explicit_jumps IC-relocable V207(2, SCM R) V209(2, SCM R) Element of the InstructionsF of (SCM R)

P1 + (q + s1) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

goto ((P1 + (q + s1)),R) is non ins-loc-free V156(2, SCM R) with_explicit_jumps IC-relocable V207(2, SCM R) V209(2, SCM R) Element of the InstructionsF of (SCM R)

P1 + q is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

goto ((P1 + q),R) is non ins-loc-free V156(2, SCM R) with_explicit_jumps IC-relocable V207(2, SCM R) V209(2, SCM R) Element of the InstructionsF of (SCM R)

P2 is Int-like Element of the carrier of (SCM R)

(Exec ((IncAddr (k,(q + s1))),(IncIC (s2,s1)))) . P2 is Element of the carrier of R

the carrier of R is non empty non trivial non empty-membered set

(IncIC (s2,s1)) . P2 is Element of the carrier of R

s2 . P2 is Element of the carrier of R

(Exec ((IncAddr (k,q)),s2)) . P2 is Element of the carrier of R

(IncIC ((Exec ((IncAddr (k,q)),s2)),s1)) . P2 is Element of the carrier of R

InsCode k is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM R)

InsCodes the InstructionsF of (SCM R) is non empty set

K55( the InstructionsF of (SCM R)) is set

P2 is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

P1 is Int-like Element of the carrier of (SCM R)

P1 =0_goto P2 is non ins-loc-free V156(2, SCM R) with_explicit_jumps IC-relocable V207(2, SCM R) V209(2, SCM R) Element of the InstructionsF of (SCM R)

P2 + (q + s1) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

P1 =0_goto (P2 + (q + s1)) is non ins-loc-free V156(2, SCM R) with_explicit_jumps IC-relocable V207(2, SCM R) V209(2, SCM R) Element of the InstructionsF of (SCM R)

P2 + q is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

P1 =0_goto (P2 + q) is non ins-loc-free V156(2, SCM R) with_explicit_jumps IC-relocable V207(2, SCM R) V209(2, SCM R) Element of the InstructionsF of (SCM R)

s is Int-like Element of the carrier of (SCM R)

(Exec ((IncAddr (k,(q + s1))),(IncIC (s2,s1)))) . s is Element of the carrier of R

the carrier of R is non empty non trivial non empty-membered set

(IncIC (s2,s1)) . s is Element of the carrier of R

s2 . s is Element of the carrier of R

(Exec ((IncAddr (k,q)),s2)) . s is Element of the carrier of R

(IncIC ((Exec ((IncAddr (k,q)),s2)),s1)) . s is Element of the carrier of R

InsCode k is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM R)

InsCodes the InstructionsF of (SCM R) is non empty set

K55( the InstructionsF of (SCM R)) is set

R is non empty non trivial V70() V95() V96() V97() V106() V113() V114() L11()

SCM R is non empty with_non-empty_values IC-Ins-separated strict V157(2) with_explicit_jumps IC-relocable V208(2) relocable AMI-Struct over 2

the carrier of (SCM R) is non empty set

the carrier of R is non empty non trivial non empty-membered set

k is Int-like Element of the carrier of (SCM R)

q is Element of the carrier of R

k .--> q is Relation-like the carrier of (SCM R) -defined {k} -defined the carrier of R -valued Function-like one-to-one constant non empty trivial finite V39(1) V127() V204() set

{k} is non empty trivial finite V39(1) V127() set

{k} --> q is Relation-like {k} -defined the carrier of R -valued {q} -valued Function-like constant non empty total V21({k},{q}) finite V127() V204() Element of K24(K25({k},{q}))

{q} is non empty trivial finite V39(1) V127() set

K25({k},{q}) is Relation-like non empty finite V127() set

K24(K25({k},{q})) is non empty finite V36() V127() set

the_Values_of (SCM R) is Relation-like non-empty non empty-yielding the carrier of (SCM R) -defined Function-like non empty total set

the Object-Kind of (SCM R) is Relation-like the carrier of (SCM R) -defined 2 -valued Function-like non empty total V21( the carrier of (SCM R),2) Element of K24(K25( the carrier of (SCM R),2))

K25( the carrier of (SCM R),2) is Relation-like non empty set

K24(K25( the carrier of (SCM R),2)) is non empty set

the ValuesF of (SCM R) is Relation-like 2 -defined Function-like non empty total V204() set

the Object-Kind of (SCM R) * the ValuesF of (SCM R) is Relation-like the carrier of (SCM R) -defined Function-like non empty total set

dom (k .--> q) is non empty trivial finite V39(1) V127() set

{k} is non empty trivial finite V39(1) V127() Element of K24( the carrier of (SCM R))

K24( the carrier of (SCM R)) is non empty set

P1 is set

(k .--> q) . P1 is set

(the_Values_of (SCM R)) . P1 is set

Values k is non empty set

(the_Values_of (SCM R)) . k is non empty set

SCM-VAL R is Relation-like 2 -defined Function-like non empty total V204() set

SCM-OK * (SCM-VAL R) is Relation-like SCM-Memory -defined Function-like non empty total set

(SCM-OK * (SCM-VAL R)) . k is set

R is non empty non trivial V70() V95() V96() V97() V106() V113() V114() L11()

SCM R is non empty with_non-empty_values IC-Ins-separated strict V157(2) with_explicit_jumps IC-relocable V208(2) relocable AMI-Struct over 2

the InstructionsF of (SCM R) is Relation-like non empty standard-ins V139() J/A-independent V142() set

the carrier of (SCM R) is non empty set

the_Values_of (SCM R) is Relation-like non-empty non empty-yielding the carrier of (SCM R) -defined Function-like non empty total set

the Object-Kind of (SCM R) is Relation-like the carrier of (SCM R) -defined 2 -valued Function-like non empty total V21( the carrier of (SCM R),2) Element of K24(K25( the carrier of (SCM R),2))

K25( the carrier of (SCM R),2) is Relation-like non empty set

K24(K25( the carrier of (SCM R),2)) is non empty set

the ValuesF of (SCM R) is Relation-like 2 -defined Function-like non empty total V204() set

the Object-Kind of (SCM R) * the ValuesF of (SCM R) is Relation-like the carrier of (SCM R) -defined Function-like non empty total set

0. (SCM R) is V51( SCM R) Element of the carrier of (SCM R)

the ZeroF of (SCM R) is Element of the carrier of (SCM R)

k is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like finite V127() non halt-free V204() set

q is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible finite V127() k -autonomic V204() set

DataPart q is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible finite V127() data-only V204() set

NonZero (SCM R) is Element of K24( the carrier of (SCM R))

K24( the carrier of (SCM R)) is non empty set

[#] (SCM R) is non empty non proper Element of K24( the carrier of (SCM R))

{(0. (SCM R))} is non empty trivial finite V39(1) V127() set

([#] (SCM R)) \ {(0. (SCM R))} is Element of K24( the carrier of (SCM R))

q | (NonZero (SCM R)) is Relation-like NonZero (SCM R) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible finite V127() V204() set

dom q is finite V127() set

dom (DataPart q) is finite V127() set

dom k is finite V127() V187() set

NAT \ (dom k) is Element of K24(REAL)

the Element of NAT \ (dom k) is Element of NAT \ (dom k)

(NonZero SCM) \ (dom q) is Element of K24( the carrier of SCM)

the Element of (NonZero SCM) \ (dom q) is Element of (NonZero SCM) \ (dom q)

the Element of dom (DataPart q) is Element of dom (DataPart q)

P2 is Int-like Element of the carrier of (SCM R)

{P2} is non empty trivial finite V39(1) V127() Element of K24( the carrier of (SCM R))

s is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

P1 is Element of the carrier of (SCM R)

0. R is V51(R) Element of the carrier of R

the carrier of R is non empty non trivial non empty-membered set

the ZeroF of R is Element of the carrier of R

(R,P2,(0. R)) is Relation-like the carrier of (SCM R) -defined {P2} -defined the carrier of (SCM R) -defined the carrier of R -valued Function-like one-to-one constant the_Values_of (SCM R) -compatible non empty trivial finite V39(1) V127() V204() set

{P2} is non empty trivial finite V39(1) V127() set

{P2} --> (0. R) is Relation-like {P2} -defined the carrier of R -valued {(0. R)} -valued Function-like constant non empty total V21({P2},{(0. R)}) finite V127() V204() Element of K24(K25({P2},{(0. R)}))

{(0. R)} is non empty trivial finite V39(1) V127() set

K25({P2},{(0. R)}) is Relation-like non empty finite V127() set

K24(K25({P2},{(0. R)})) is non empty finite V36() V127() set

Start-At (s,(SCM R)) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty finite V127() s -started V204() set

(0. (SCM R)) .--> s is Relation-like the carrier of (SCM R) -defined {(0. (SCM R))} -defined NAT -valued Function-like one-to-one constant non empty trivial finite V39(1) V124() V127() V204() set

{(0. (SCM R))} --> s is Relation-like {(0. (SCM R))} -defined NAT -valued {s} -valued Function-like constant non empty total V21({(0. (SCM R))},{s}) finite V124() V127() V204() Element of K24(K25({(0. (SCM R))},{s}))

{s} is non empty trivial finite V36() V39(1) V127() set

K25({(0. (SCM R))},{s}) is Relation-like non empty finite V127() set

K24(K25({(0. (SCM R))},{s})) is non empty finite V36() V127() set

(R,P2,(0. R)) +* (Start-At (s,(SCM R))) is Relation-like the carrier of (SCM R) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible the_Values_of (SCM R) -compatible non empty finite V127() s -started V204() set

dom ((R,P2,(0. R)) +* (Start-At (s,(SCM R)))) is non empty finite V127() set

dom (R,P2,(0. R)) is non empty trivial finite V39(1) V127() set

dom (Start-At (s,(SCM R))) is non empty finite V127() set

(dom (R,P2,(0. R))) \/ (dom (Start-At (s,(SCM R)))) is non empty finite V127() set

q +* ((R,P2,(0. R)) +* (Start-At (s,(SCM R)))) is Relation-like the carrier of (SCM R) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible the_Values_of (SCM R) -compatible non empty finite V127() s -started V204() set

DPp is Int-like Element of the carrier of (SCM R)

DPp := P2 is ins-loc-free V156(2, SCM R) with_explicit_jumps IC-relocable V207(2, SCM R) V209(2, SCM R) relocable Element of the InstructionsF of (SCM R)

s .--> (DPp := P2) is Relation-like NAT -defined {s} -defined the InstructionsF of (SCM R) -valued the InstructionsF of (SCM R) -valued Function-like one-to-one constant non empty trivial finite V39(1) V127() V147( SCM R) V204() set

{s} --> (DPp := P2) is Relation-like {s} -defined the InstructionsF of (SCM R) -valued {(DPp := P2)} -valued Function-like constant non empty total V21({s},{(DPp := P2)}) finite V127() V204() Element of K24(K25({s},{(DPp := P2)}))

{(DPp := P2)} is non empty trivial finite V39(1) V127() set

K25({s},{(DPp := P2)}) is Relation-like non empty finite V127() set

K24(K25({s},{(DPp := P2)})) is non empty finite V36() V127() set

k +* (s .--> (DPp := P2)) is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty finite V127() V204() set

Cs3i is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

Cs2i is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty total set

dom (q +* ((R,P2,(0. R)) +* (Start-At (s,(SCM R))))) is non empty finite V127() set

(dom q) \/ (dom ((R,P2,(0. R)) +* (Start-At (s,(SCM R))))) is non empty finite V127() set

{(0. (SCM R))} is non empty trivial finite V39(1) V127() Element of K24( the carrier of (SCM R))

IC Cs3i is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT

Cs3i . (0. (SCM R)) is set

(q +* ((R,P2,(0. R)) +* (Start-At (s,(SCM R))))) . (0. (SCM R)) is set

((R,P2,(0. R)) +* (Start-At (s,(SCM R)))) . (0. (SCM R)) is set

(Start-At (s,(SCM R))) . (0. (SCM R)) is set

Cs3i . P2 is Element of the carrier of R

(q +* ((R,P2,(0. R)) +* (Start-At (s,(SCM R))))) . P2 is set

((R,P2,(0. R)) +* (Start-At (s,(SCM R)))) . P2 is set

(R,P2,(0. R)) . P2 is set

dom (s .--> (DPp := P2)) is non empty trivial finite V39(1) V127() V187() set

{s} is non empty trivial finite V36() V39(1) V127() Element of K24(NAT)

dom (k +* (s .--> (DPp := P2))) is non empty finite V127() V187() set

(dom k) \/ (dom (s .--> (DPp := P2))) is non empty finite V127() set

Cs2i . s is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)

(k +* (s .--> (DPp := P2))) . s is set

(s .--> (DPp := P2)) . s is set

Comput (Cs2i,Cs3i,1) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set

dom (Comput (Cs2i,Cs3i,1)) is non empty set

(Comput (Cs2i,Cs3i,1)) | (dom q) is Relation-like dom q -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible finite V127() V204() set

dom ((Comput (Cs2i,Cs3i,1)) | (dom q)) is finite V127() set

Cs1i1 is Element of the carrier of R

(R,P2,Cs1i1) is Relation-like the carrier of (SCM R) -defined {P2} -defined the carrier of (SCM R) -defined the carrier of R -valued Function-like one-to-one constant the_Values_of (SCM R) -compatible non empty trivial finite V39(1) V127() V204() set

{P2} --> Cs1i1 is Relation-like {P2} -defined the carrier of R -valued {Cs1i1} -valued Function-like constant non empty total V21({P2},{Cs1i1}) finite V127() V204() Element of K24(K25({P2},{Cs1i1}))

{Cs1i1} is non empty trivial finite V39(1) V127() set

K25({P2},{Cs1i1}) is Relation-like non empty finite V127() set

K24(K25({P2},{Cs1i1})) is non empty finite V36() V127() set

(R,P2,Cs1i1) +* (Start-At (s,(SCM R))) is Relation-like the carrier of (SCM R) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible the_Values_of (SCM R) -compatible non empty finite V127() s -started V204() set

q +* ((R,P2,Cs1i1) +* (Start-At (s,(SCM R)))) is Relation-like the carrier of (SCM R) -defined the carrier of (SCM R) -defined Function-like the_Values_of (