:: 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 (SCM R) -compatible the_Values_of (SCM R) -compatible non empty finite V127() s -started V204() set
I is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
da is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty total set
Comput (da,I,1) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
dom (Comput (da,I,1)) is non empty set
(Comput (da,I,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 (da,I,1)) | (dom q)) is finite V127() set
(dom q) /\ {(0. (SCM R))} is finite V127() Element of K24( the carrier of (SCM R))
loc is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty total set
x is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty total set
(dom (R,P2,(0. R))) \/ {(0. (SCM R))} is non empty finite V127() set
{P2} \/ {(0. (SCM R))} is non empty finite V127() Element of K24( the carrier of (SCM R))
(dom q) /\ (dom ((R,P2,(0. R)) +* (Start-At (s,(SCM R))))) is finite V127() set
(dom q) /\ {P2} is finite V127() Element of K24( the carrier of (SCM R))
((dom q) /\ {P2}) \/ {} is finite V127() set
dom ((R,P2,Cs1i1) +* (Start-At (s,(SCM R)))) is non empty finite V127() set
dom (R,P2,Cs1i1) is non empty trivial finite V39(1) V127() set
(dom (R,P2,Cs1i1)) \/ (dom (Start-At (s,(SCM R)))) is non empty finite V127() set
(dom (R,P2,Cs1i1)) \/ {(0. (SCM R))} is non empty finite V127() set
(dom q) /\ (dom ((R,P2,Cs1i1) +* (Start-At (s,(SCM R))))) is finite V127() set
Comput (loc,Cs3i,1) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
(Comput (loc,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
Comput (x,I,1) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
(Comput (x,I,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 (q +* ((R,P2,Cs1i1) +* (Start-At (s,(SCM R))))) is non empty finite V127() set
(dom q) \/ (dom ((R,P2,Cs1i1) +* (Start-At (s,(SCM R))))) is non empty finite V127() set
IC I is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
I . (0. (SCM R)) is set
(q +* ((R,P2,Cs1i1) +* (Start-At (s,(SCM R))))) . (0. (SCM R)) is set
((R,P2,Cs1i1) +* (Start-At (s,(SCM R)))) . (0. (SCM R)) is set
da . s is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
I . P2 is Element of the carrier of R
(q +* ((R,P2,Cs1i1) +* (Start-At (s,(SCM R))))) . P2 is set
((R,P2,Cs1i1) +* (Start-At (s,(SCM R)))) . P2 is set
(R,P2,Cs1i1) . P2 is set
da /. s is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
0 + 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
Comput (da,I,(0 + 1)) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
(Comput (da,I,(0 + 1))) . DPp is Element of the carrier of R
Comput (da,I,0) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
Following (da,(Comput (da,I,0))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
CurInstr (da,(Comput (da,I,0))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
IC (Comput (da,I,0)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (da,I,0)) . (0. (SCM R)) is set
da /. (IC (Comput (da,I,0))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
Exec ((CurInstr (da,(Comput (da,I,0)))),(Comput (da,I,0))) 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),(CurInstr (da,(Comput (da,I,0))))) 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),(CurInstr (da,(Comput (da,I,0))))) . (Comput (da,I,0)) is set
(Following (da,(Comput (da,I,0)))) . DPp is Element of the carrier of R
Following (da,I) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
CurInstr (da,I) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
da /. (IC I) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
Exec ((CurInstr (da,I)),I) 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),(CurInstr (da,I))) 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),(CurInstr (da,I))) . I is set
(Following (da,I)) . DPp is Element of the carrier of R
Cs2i /. s is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
Comput (Cs2i,Cs3i,(0 + 1)) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
(Comput (Cs2i,Cs3i,(0 + 1))) . DPp is Element of the carrier of R
Comput (Cs2i,Cs3i,0) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
Following (Cs2i,(Comput (Cs2i,Cs3i,0))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
CurInstr (Cs2i,(Comput (Cs2i,Cs3i,0))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
IC (Comput (Cs2i,Cs3i,0)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (Cs2i,Cs3i,0)) . (0. (SCM R)) is set
Cs2i /. (IC (Comput (Cs2i,Cs3i,0))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
Exec ((CurInstr (Cs2i,(Comput (Cs2i,Cs3i,0)))),(Comput (Cs2i,Cs3i,0))) 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),(CurInstr (Cs2i,(Comput (Cs2i,Cs3i,0))))) 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),(CurInstr (Cs2i,(Comput (Cs2i,Cs3i,0))))) . (Comput (Cs2i,Cs3i,0)) is set
(Following (Cs2i,(Comput (Cs2i,Cs3i,0)))) . DPp is Element of the carrier of R
Following (Cs2i,Cs3i) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
CurInstr (Cs2i,Cs3i) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
Cs2i /. (IC Cs3i) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
Exec ((CurInstr (Cs2i,Cs3i)),Cs3i) 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),(CurInstr (Cs2i,Cs3i))) 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),(CurInstr (Cs2i,Cs3i))) . Cs3i is set
(Following (Cs2i,Cs3i)) . DPp is Element of the carrier of R
((Comput (loc,Cs3i,1)) | (dom q)) . DPp 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 IC-recognized 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
k is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like finite V127() non halt-free V204() set
dom k is finite V127() V187() set
q is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty finite V127() k -autonomic V204() set
p is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
s1 is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty total set
s2 is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
Comput (s1,p,s2) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
IC (Comput (s1,p,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)
(Comput (s1,p,s2)) . (0. (SCM R)) is set
(IC (Comput (s1,p,s2))) + 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
dl. (R,0) is Int-like Element of the carrier of (SCM R)
(dl. (R,0)) := (dl. (R,0)) 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)
(IC (Comput (s1,p,s2))) .--> ((dl. (R,0)) := (dl. (R,0))) is Relation-like NAT -defined {(IC (Comput (s1,p,s2)))} -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
{(IC (Comput (s1,p,s2)))} is non empty trivial finite V36() V39(1) V127() set
{(IC (Comput (s1,p,s2)))} --> ((dl. (R,0)) := (dl. (R,0))) is Relation-like {(IC (Comput (s1,p,s2)))} -defined the InstructionsF of (SCM R) -valued {((dl. (R,0)) := (dl. (R,0)))} -valued Function-like constant non empty total V21({(IC (Comput (s1,p,s2)))},{((dl. (R,0)) := (dl. (R,0)))}) finite V127() V204() Element of K24(K25({(IC (Comput (s1,p,s2)))},{((dl. (R,0)) := (dl. (R,0)))}))
{((dl. (R,0)) := (dl. (R,0)))} is non empty trivial finite V39(1) V127() set
K25({(IC (Comput (s1,p,s2)))},{((dl. (R,0)) := (dl. (R,0)))}) is Relation-like non empty finite V127() set
K24(K25({(IC (Comput (s1,p,s2)))},{((dl. (R,0)) := (dl. (R,0)))})) is non empty finite V36() V127() set
k +* ((IC (Comput (s1,p,s2))) .--> ((dl. (R,0)) := (dl. (R,0)))) is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty finite V127() V204() 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) relocable Element of the InstructionsF of (SCM R)
halt the InstructionsF of (SCM R) is ins-loc-free with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
K47(0,{},{}) is set
(IC (Comput (s1,p,s2))) .--> (halt (SCM R)) is Relation-like NAT -defined {(IC (Comput (s1,p,s2)))} -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
{(IC (Comput (s1,p,s2)))} --> (halt (SCM R)) is Relation-like {(IC (Comput (s1,p,s2)))} -defined the InstructionsF of (SCM R) -valued {(halt (SCM R))} -valued Function-like constant non empty total V21({(IC (Comput (s1,p,s2)))},{(halt (SCM R))}) finite V127() V204() Element of K24(K25({(IC (Comput (s1,p,s2)))},{(halt (SCM R))}))
{(halt (SCM R))} is non empty trivial finite V39(1) V127() set
K25({(IC (Comput (s1,p,s2)))},{(halt (SCM R))}) is Relation-like non empty finite V127() set
K24(K25({(IC (Comput (s1,p,s2)))},{(halt (SCM R))})) is non empty finite V36() V127() set
k +* ((IC (Comput (s1,p,s2))) .--> (halt (SCM R))) is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty finite V127() V204() set
s1 +* ((IC (Comput (s1,p,s2))) .--> ((dl. (R,0)) := (dl. (R,0)))) is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty total set
s1 +* ((IC (Comput (s1,p,s2))) .--> (halt (SCM R))) is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty total set
dom ((IC (Comput (s1,p,s2))) .--> (halt (SCM R))) is non empty trivial finite V39(1) V127() V187() set
{(IC (Comput (s1,p,s2)))} is non empty trivial finite V36() V39(1) V127() Element of K24(NAT)
dom ((IC (Comput (s1,p,s2))) .--> ((dl. (R,0)) := (dl. (R,0)))) is non empty trivial finite V39(1) V127() V187() set
Cs3i is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty total set
Cs2i is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty total set
Comput (Cs2i,p,s2) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
Comput (Cs3i,p,s2) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
((IC (Comput (s1,p,s2))) .--> (halt (SCM R))) . (IC (Comput (s1,p,s2))) is set
Cs2i . (IC (Comput (s1,p,s2))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
((IC (Comput (s1,p,s2))) .--> ((dl. (R,0)) := (dl. (R,0)))) . (IC (Comput (s1,p,s2))) is set
dom q is non empty finite V127() set
(Comput (Cs3i,p,s2)) | (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
(Comput (s1,p,s2)) | (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
(Comput (Cs2i,p,s2)) | (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
s2 + 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
Cs3i1 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
Comput (Cs3i,p,Cs3i1) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
(Comput (Cs3i,p,Cs3i1)) | (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
Comput (Cs2i,p,Cs3i1) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
(Comput (Cs2i,p,Cs3i1)) | (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
IC ((Comput (s1,p,s2)) | (dom q)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
((Comput (s1,p,s2)) | (dom q)) . (0. (SCM R)) is set
IC (Comput (Cs3i,p,s2)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (Cs3i,p,s2)) . (0. (SCM R)) is set
CurInstr (Cs3i,(Comput (Cs3i,p,s2))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
Cs3i /. (IC (Comput (Cs3i,p,s2))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
Cs3i . (IC (Comput (s1,p,s2))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
Following (Cs3i,(Comput (Cs3i,p,s2))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
Exec ((CurInstr (Cs3i,(Comput (Cs3i,p,s2)))),(Comput (Cs3i,p,s2))) 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),(CurInstr (Cs3i,(Comput (Cs3i,p,s2))))) 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),(CurInstr (Cs3i,(Comput (Cs3i,p,s2))))) . (Comput (Cs3i,p,s2)) is set
Exec (((dl. (R,0)) := (dl. (R,0))),(Comput (Cs3i,p,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),((dl. (R,0)) := (dl. (R,0)))) 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),((dl. (R,0)) := (dl. (R,0)))) . (Comput (Cs3i,p,s2)) is set
IC (Exec (((dl. (R,0)) := (dl. (R,0))),(Comput (Cs3i,p,s2)))) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Exec (((dl. (R,0)) := (dl. (R,0))),(Comput (Cs3i,p,s2)))) . (0. (SCM R)) is set
succ (IC (Comput (Cs3i,p,s2))) is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() set
(IC (Comput (Cs3i,p,s2))) + 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
IC (Comput (Cs3i,p,Cs3i1)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (Cs3i,p,Cs3i1)) . (0. (SCM R)) is set
Following (Cs2i,(Comput (Cs2i,p,s2))) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
CurInstr (Cs2i,(Comput (Cs2i,p,s2))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
IC (Comput (Cs2i,p,s2)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (Cs2i,p,s2)) . (0. (SCM R)) is set
Cs2i /. (IC (Comput (Cs2i,p,s2))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
Exec ((CurInstr (Cs2i,(Comput (Cs2i,p,s2)))),(Comput (Cs2i,p,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),(CurInstr (Cs2i,(Comput (Cs2i,p,s2))))) 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),(CurInstr (Cs2i,(Comput (Cs2i,p,s2))))) . (Comput (Cs2i,p,s2)) is set
Cs2i . (IC (Comput (Cs2i,p,s2))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
IC (Comput (Cs2i,p,Cs3i1)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (Cs2i,p,Cs3i1)) . (0. (SCM R)) is set
IC ((Comput (Cs3i,p,Cs3i1)) | (dom q)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
((Comput (Cs3i,p,Cs3i1)) | (dom q)) . (0. (SCM R)) is set
IC ((Comput (Cs2i,p,Cs3i1)) | (dom q)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
((Comput (Cs2i,p,Cs3i1)) | (dom q)) . (0. (SCM R)) is set
R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
k is non empty non trivial V70() V95() V96() V97() V106() V113() V114() L11()
SCM k is non empty with_non-empty_values IC-Ins-separated strict V157(2) with_explicit_jumps IC-relocable V208(2) relocable IC-recognized CurIns-recognized AMI-Struct over 2
the carrier of (SCM k) is non empty set
the_Values_of (SCM k) is Relation-like non-empty non empty-yielding the carrier of (SCM k) -defined Function-like non empty total set
the Object-Kind of (SCM k) is Relation-like the carrier of (SCM k) -defined 2 -valued Function-like non empty total V21( the carrier of (SCM k),2) Element of K24(K25( the carrier of (SCM k),2))
K25( the carrier of (SCM k),2) is Relation-like non empty set
K24(K25( the carrier of (SCM k),2)) is non empty set
the ValuesF of (SCM k) is Relation-like 2 -defined Function-like non empty total V204() set
the Object-Kind of (SCM k) * the ValuesF of (SCM k) is Relation-like the carrier of (SCM k) -defined Function-like non empty total set
the InstructionsF of (SCM k) is Relation-like non empty standard-ins V139() J/A-independent V142() set
q is Int-like Element of the carrier of (SCM k)
p is Int-like Element of the carrier of (SCM k)
q := p is ins-loc-free V156(2, SCM k) with_explicit_jumps IC-relocable V207(2, SCM k) V209(2, SCM k) relocable Element of the InstructionsF of (SCM k)
s1 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
s2 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
P1 is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like non empty total set
Comput (P1,s1,R) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
CurInstr (P1,(Comput (P1,s1,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IC (Comput (P1,s1,R)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
0. (SCM k) is V51( SCM k) Element of the carrier of (SCM k)
the ZeroF of (SCM k) is Element of the carrier of (SCM k)
(Comput (P1,s1,R)) . (0. (SCM k)) is set
P1 /. (IC (Comput (P1,s1,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
(Comput (P1,s1,R)) . p is Element of the carrier of k
the carrier of k is non empty non trivial non empty-membered set
P2 is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like non empty total set
Comput (P2,s2,R) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
(Comput (P2,s2,R)) . p is Element of the carrier of k
R + 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
Comput (P2,s2,(R + 1)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Comput (P1,s1,(R + 1)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Cs2i is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like finite V127() non halt-free V204() set
Cs1i1 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty finite V127() Cs2i -autonomic V204() set
dom Cs1i1 is non empty finite V127() set
(Comput (P1,s1,(R + 1))) | (dom Cs1i1) is Relation-like dom Cs1i1 -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
((Comput (P1,s1,(R + 1))) | (dom Cs1i1)) . q is set
(Comput (P1,s1,(R + 1))) . q is Element of the carrier of k
(Comput (P2,s2,(R + 1))) | (dom Cs1i1) is Relation-like dom Cs1i1 -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
((Comput (P2,s2,(R + 1))) | (dom Cs1i1)) . q is set
(Comput (P2,s2,(R + 1))) . q is Element of the carrier of k
Following (P2,(Comput (P2,s2,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
CurInstr (P2,(Comput (P2,s2,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IC (Comput (P2,s2,R)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P2,s2,R)) . (0. (SCM k)) is set
P2 /. (IC (Comput (P2,s2,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
Exec ((CurInstr (P2,(Comput (P2,s2,R)))),(Comput (P2,s2,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))) is functional V125() V126() set
K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))) is functional non empty set
the Execution of (SCM k) is Relation-like the InstructionsF of (SCM k) -defined K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))) -valued Function-like non empty total V21( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))) Function-yielding V161() Element of K24(K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))))
K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))) is Relation-like non empty set
K24(K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))))) is non empty set
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P2,(Comput (P2,s2,R))))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P2,(Comput (P2,s2,R))))) . (Comput (P2,s2,R)) is set
Following (P1,(Comput (P1,s1,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Exec ((CurInstr (P1,(Comput (P1,s1,R)))),(Comput (P1,s1,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P1,(Comput (P1,s1,R))))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P1,(Comput (P1,s1,R))))) . (Comput (P1,s1,R)) is set
R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
k is non empty non trivial V70() V95() V96() V97() V106() V113() V114() L11()
SCM k is non empty with_non-empty_values IC-Ins-separated strict V157(2) with_explicit_jumps IC-relocable V208(2) relocable IC-recognized CurIns-recognized AMI-Struct over 2
the carrier of (SCM k) is non empty set
the_Values_of (SCM k) is Relation-like non-empty non empty-yielding the carrier of (SCM k) -defined Function-like non empty total set
the Object-Kind of (SCM k) is Relation-like the carrier of (SCM k) -defined 2 -valued Function-like non empty total V21( the carrier of (SCM k),2) Element of K24(K25( the carrier of (SCM k),2))
K25( the carrier of (SCM k),2) is Relation-like non empty set
K24(K25( the carrier of (SCM k),2)) is non empty set
the ValuesF of (SCM k) is Relation-like 2 -defined Function-like non empty total V204() set
the Object-Kind of (SCM k) * the ValuesF of (SCM k) is Relation-like the carrier of (SCM k) -defined Function-like non empty total set
the InstructionsF of (SCM k) is Relation-like non empty standard-ins V139() J/A-independent V142() set
q is Int-like Element of the carrier of (SCM k)
p is Int-like Element of the carrier of (SCM k)
AddTo (q,p) is ins-loc-free V156(2, SCM k) with_explicit_jumps IC-relocable V207(2, SCM k) V209(2, SCM k) relocable Element of the InstructionsF of (SCM k)
s1 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
s2 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
P1 is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like non empty total set
Comput (P1,s1,R) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
CurInstr (P1,(Comput (P1,s1,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IC (Comput (P1,s1,R)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
0. (SCM k) is V51( SCM k) Element of the carrier of (SCM k)
the ZeroF of (SCM k) is Element of the carrier of (SCM k)
(Comput (P1,s1,R)) . (0. (SCM k)) is set
P1 /. (IC (Comput (P1,s1,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
(Comput (P1,s1,R)) . q is Element of the carrier of k
the carrier of k is non empty non trivial non empty-membered set
(Comput (P1,s1,R)) . p is Element of the carrier of k
((Comput (P1,s1,R)) . q) + ((Comput (P1,s1,R)) . p) is Element of the carrier of k
P2 is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like non empty total set
Comput (P2,s2,R) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
(Comput (P2,s2,R)) . q is Element of the carrier of k
(Comput (P2,s2,R)) . p is Element of the carrier of k
((Comput (P2,s2,R)) . q) + ((Comput (P2,s2,R)) . p) is Element of the carrier of k
R + 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
Comput (P2,s2,(R + 1)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Comput (P1,s1,(R + 1)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Cs2i is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like finite V127() non halt-free V204() set
Cs1i1 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty finite V127() Cs2i -autonomic V204() set
dom Cs1i1 is non empty finite V127() set
(Comput (P1,s1,(R + 1))) | (dom Cs1i1) is Relation-like dom Cs1i1 -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
((Comput (P1,s1,(R + 1))) | (dom Cs1i1)) . q is set
(Comput (P1,s1,(R + 1))) . q is Element of the carrier of k
(Comput (P2,s2,(R + 1))) | (dom Cs1i1) is Relation-like dom Cs1i1 -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
((Comput (P2,s2,(R + 1))) | (dom Cs1i1)) . q is set
(Comput (P2,s2,(R + 1))) . q is Element of the carrier of k
Following (P2,(Comput (P2,s2,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
CurInstr (P2,(Comput (P2,s2,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IC (Comput (P2,s2,R)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P2,s2,R)) . (0. (SCM k)) is set
P2 /. (IC (Comput (P2,s2,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
Exec ((CurInstr (P2,(Comput (P2,s2,R)))),(Comput (P2,s2,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))) is functional V125() V126() set
K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))) is functional non empty set
the Execution of (SCM k) is Relation-like the InstructionsF of (SCM k) -defined K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))) -valued Function-like non empty total V21( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))) Function-yielding V161() Element of K24(K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))))
K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))) is Relation-like non empty set
K24(K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))))) is non empty set
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P2,(Comput (P2,s2,R))))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P2,(Comput (P2,s2,R))))) . (Comput (P2,s2,R)) is set
Following (P1,(Comput (P1,s1,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Exec ((CurInstr (P1,(Comput (P1,s1,R)))),(Comput (P1,s1,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P1,(Comput (P1,s1,R))))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P1,(Comput (P1,s1,R))))) . (Comput (P1,s1,R)) is set
R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
k is non empty non trivial V70() V95() V96() V97() V106() V113() V114() L11()
SCM k is non empty with_non-empty_values IC-Ins-separated strict V157(2) with_explicit_jumps IC-relocable V208(2) relocable IC-recognized CurIns-recognized AMI-Struct over 2
the carrier of (SCM k) is non empty set
the_Values_of (SCM k) is Relation-like non-empty non empty-yielding the carrier of (SCM k) -defined Function-like non empty total set
the Object-Kind of (SCM k) is Relation-like the carrier of (SCM k) -defined 2 -valued Function-like non empty total V21( the carrier of (SCM k),2) Element of K24(K25( the carrier of (SCM k),2))
K25( the carrier of (SCM k),2) is Relation-like non empty set
K24(K25( the carrier of (SCM k),2)) is non empty set
the ValuesF of (SCM k) is Relation-like 2 -defined Function-like non empty total V204() set
the Object-Kind of (SCM k) * the ValuesF of (SCM k) is Relation-like the carrier of (SCM k) -defined Function-like non empty total set
the InstructionsF of (SCM k) is Relation-like non empty standard-ins V139() J/A-independent V142() set
q is Int-like Element of the carrier of (SCM k)
p is Int-like Element of the carrier of (SCM k)
SubFrom (q,p) is ins-loc-free V156(2, SCM k) with_explicit_jumps IC-relocable V207(2, SCM k) V209(2, SCM k) relocable Element of the InstructionsF of (SCM k)
s1 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
s2 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
P1 is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like non empty total set
Comput (P1,s1,R) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
CurInstr (P1,(Comput (P1,s1,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IC (Comput (P1,s1,R)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
0. (SCM k) is V51( SCM k) Element of the carrier of (SCM k)
the ZeroF of (SCM k) is Element of the carrier of (SCM k)
(Comput (P1,s1,R)) . (0. (SCM k)) is set
P1 /. (IC (Comput (P1,s1,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
(Comput (P1,s1,R)) . q is Element of the carrier of k
the carrier of k is non empty non trivial non empty-membered set
(Comput (P1,s1,R)) . p is Element of the carrier of k
((Comput (P1,s1,R)) . q) - ((Comput (P1,s1,R)) . p) is Element of the carrier of k
P2 is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like non empty total set
Comput (P2,s2,R) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
(Comput (P2,s2,R)) . q is Element of the carrier of k
(Comput (P2,s2,R)) . p is Element of the carrier of k
((Comput (P2,s2,R)) . q) - ((Comput (P2,s2,R)) . p) is Element of the carrier of k
R + 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
Comput (P2,s2,(R + 1)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Comput (P1,s1,(R + 1)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Cs2i is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like finite V127() non halt-free V204() set
Cs1i1 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty finite V127() Cs2i -autonomic V204() set
dom Cs1i1 is non empty finite V127() set
(Comput (P1,s1,(R + 1))) | (dom Cs1i1) is Relation-like dom Cs1i1 -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
((Comput (P1,s1,(R + 1))) | (dom Cs1i1)) . q is set
(Comput (P1,s1,(R + 1))) . q is Element of the carrier of k
(Comput (P2,s2,(R + 1))) | (dom Cs1i1) is Relation-like dom Cs1i1 -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
((Comput (P2,s2,(R + 1))) | (dom Cs1i1)) . q is set
(Comput (P2,s2,(R + 1))) . q is Element of the carrier of k
Following (P2,(Comput (P2,s2,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
CurInstr (P2,(Comput (P2,s2,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IC (Comput (P2,s2,R)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P2,s2,R)) . (0. (SCM k)) is set
P2 /. (IC (Comput (P2,s2,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
Exec ((CurInstr (P2,(Comput (P2,s2,R)))),(Comput (P2,s2,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))) is functional V125() V126() set
K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))) is functional non empty set
the Execution of (SCM k) is Relation-like the InstructionsF of (SCM k) -defined K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))) -valued Function-like non empty total V21( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))) Function-yielding V161() Element of K24(K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))))
K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))) is Relation-like non empty set
K24(K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))))) is non empty set
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P2,(Comput (P2,s2,R))))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P2,(Comput (P2,s2,R))))) . (Comput (P2,s2,R)) is set
Following (P1,(Comput (P1,s1,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Exec ((CurInstr (P1,(Comput (P1,s1,R)))),(Comput (P1,s1,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P1,(Comput (P1,s1,R))))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P1,(Comput (P1,s1,R))))) . (Comput (P1,s1,R)) is set
R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
k is non empty non trivial V70() V95() V96() V97() V106() V113() V114() L11()
SCM k is non empty with_non-empty_values IC-Ins-separated strict V157(2) with_explicit_jumps IC-relocable V208(2) relocable IC-recognized CurIns-recognized AMI-Struct over 2
the carrier of (SCM k) is non empty set
the_Values_of (SCM k) is Relation-like non-empty non empty-yielding the carrier of (SCM k) -defined Function-like non empty total set
the Object-Kind of (SCM k) is Relation-like the carrier of (SCM k) -defined 2 -valued Function-like non empty total V21( the carrier of (SCM k),2) Element of K24(K25( the carrier of (SCM k),2))
K25( the carrier of (SCM k),2) is Relation-like non empty set
K24(K25( the carrier of (SCM k),2)) is non empty set
the ValuesF of (SCM k) is Relation-like 2 -defined Function-like non empty total V204() set
the Object-Kind of (SCM k) * the ValuesF of (SCM k) is Relation-like the carrier of (SCM k) -defined Function-like non empty total set
the InstructionsF of (SCM k) is Relation-like non empty standard-ins V139() J/A-independent V142() set
q is Int-like Element of the carrier of (SCM k)
p is Int-like Element of the carrier of (SCM k)
MultBy (q,p) is ins-loc-free V156(2, SCM k) with_explicit_jumps IC-relocable V207(2, SCM k) V209(2, SCM k) relocable Element of the InstructionsF of (SCM k)
s1 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
s2 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
P1 is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like non empty total set
Comput (P1,s1,R) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
CurInstr (P1,(Comput (P1,s1,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IC (Comput (P1,s1,R)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
0. (SCM k) is V51( SCM k) Element of the carrier of (SCM k)
the ZeroF of (SCM k) is Element of the carrier of (SCM k)
(Comput (P1,s1,R)) . (0. (SCM k)) is set
P1 /. (IC (Comput (P1,s1,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
(Comput (P1,s1,R)) . q is Element of the carrier of k
the carrier of k is non empty non trivial non empty-membered set
(Comput (P1,s1,R)) . p is Element of the carrier of k
((Comput (P1,s1,R)) . q) * ((Comput (P1,s1,R)) . p) is Element of the carrier of k
P2 is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like non empty total set
Comput (P2,s2,R) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
(Comput (P2,s2,R)) . q is Element of the carrier of k
(Comput (P2,s2,R)) . p is Element of the carrier of k
((Comput (P2,s2,R)) . q) * ((Comput (P2,s2,R)) . p) is Element of the carrier of k
R + 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
Comput (P2,s2,(R + 1)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Comput (P1,s1,(R + 1)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Cs2i is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like finite V127() non halt-free V204() set
Cs1i1 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty finite V127() Cs2i -autonomic V204() set
dom Cs1i1 is non empty finite V127() set
(Comput (P1,s1,(R + 1))) | (dom Cs1i1) is Relation-like dom Cs1i1 -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
((Comput (P1,s1,(R + 1))) | (dom Cs1i1)) . q is set
(Comput (P1,s1,(R + 1))) . q is Element of the carrier of k
(Comput (P2,s2,(R + 1))) | (dom Cs1i1) is Relation-like dom Cs1i1 -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
((Comput (P2,s2,(R + 1))) | (dom Cs1i1)) . q is set
(Comput (P2,s2,(R + 1))) . q is Element of the carrier of k
Following (P2,(Comput (P2,s2,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
CurInstr (P2,(Comput (P2,s2,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IC (Comput (P2,s2,R)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P2,s2,R)) . (0. (SCM k)) is set
P2 /. (IC (Comput (P2,s2,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
Exec ((CurInstr (P2,(Comput (P2,s2,R)))),(Comput (P2,s2,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))) is functional V125() V126() set
K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))) is functional non empty set
the Execution of (SCM k) is Relation-like the InstructionsF of (SCM k) -defined K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))) -valued Function-like non empty total V21( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))) Function-yielding V161() Element of K24(K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))))
K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))) is Relation-like non empty set
K24(K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))))) is non empty set
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P2,(Comput (P2,s2,R))))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P2,(Comput (P2,s2,R))))) . (Comput (P2,s2,R)) is set
Following (P1,(Comput (P1,s1,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Exec ((CurInstr (P1,(Comput (P1,s1,R)))),(Comput (P1,s1,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P1,(Comput (P1,s1,R))))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P1,(Comput (P1,s1,R))))) . (Comput (P1,s1,R)) is set
R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
k is non empty non trivial V70() V95() V96() V97() V106() V113() V114() L11()
SCM k is non empty with_non-empty_values IC-Ins-separated strict V157(2) with_explicit_jumps IC-relocable V208(2) relocable IC-recognized CurIns-recognized AMI-Struct over 2
the carrier of (SCM k) is non empty set
the_Values_of (SCM k) is Relation-like non-empty non empty-yielding the carrier of (SCM k) -defined Function-like non empty total set
the Object-Kind of (SCM k) is Relation-like the carrier of (SCM k) -defined 2 -valued Function-like non empty total V21( the carrier of (SCM k),2) Element of K24(K25( the carrier of (SCM k),2))
K25( the carrier of (SCM k),2) is Relation-like non empty set
K24(K25( the carrier of (SCM k),2)) is non empty set
the ValuesF of (SCM k) is Relation-like 2 -defined Function-like non empty total V204() set
the Object-Kind of (SCM k) * the ValuesF of (SCM k) is Relation-like the carrier of (SCM k) -defined Function-like non empty total set
the InstructionsF of (SCM k) is Relation-like non empty standard-ins V139() J/A-independent V142() set
0. k is V51(k) Element of the carrier of k
the carrier of k is non empty non trivial non empty-membered set
the ZeroF of k is Element of the carrier of k
q is Int-like Element of the carrier of (SCM k)
p is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
q =0_goto p is non ins-loc-free V156(2, SCM k) with_explicit_jumps IC-relocable V207(2, SCM k) V209(2, SCM k) relocable Element of the InstructionsF of (SCM k)
s1 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
s2 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
P1 is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like non empty total set
Comput (P1,s1,R) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
CurInstr (P1,(Comput (P1,s1,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IC (Comput (P1,s1,R)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
0. (SCM k) is V51( SCM k) Element of the carrier of (SCM k)
the ZeroF of (SCM k) is Element of the carrier of (SCM k)
(Comput (P1,s1,R)) . (0. (SCM k)) is set
P1 /. (IC (Comput (P1,s1,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
succ (IC (Comput (P1,s1,R))) is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() set
(IC (Comput (P1,s1,R))) + 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
(Comput (P1,s1,R)) . q is Element of the carrier of k
P2 is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like non empty total set
Comput (P2,s2,R) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
(Comput (P2,s2,R)) . q is Element of the carrier of k
R + 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
Comput (P2,s2,(R + 1)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Comput (P1,s1,(R + 1)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Cs2i1 is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like finite V127() non halt-free V204() set
Cs3i is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty finite V127() Cs2i1 -autonomic V204() set
CurInstr (P2,(Comput (P2,s2,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IC (Comput (P2,s2,R)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P2,s2,R)) . (0. (SCM k)) is set
P2 /. (IC (Comput (P2,s2,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
Following (P1,(Comput (P1,s1,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Exec ((CurInstr (P1,(Comput (P1,s1,R)))),(Comput (P1,s1,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))) is functional V125() V126() set
K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))) is functional non empty set
the Execution of (SCM k) is Relation-like the InstructionsF of (SCM k) -defined K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))) -valued Function-like non empty total V21( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))) Function-yielding V161() Element of K24(K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))))
K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))) is Relation-like non empty set
K24(K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))))) is non empty set
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P1,(Comput (P1,s1,R))))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P1,(Comput (P1,s1,R))))) . (Comput (P1,s1,R)) is set
Following (P2,(Comput (P2,s2,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Exec ((CurInstr (P2,(Comput (P2,s2,R)))),(Comput (P2,s2,R))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P2,(Comput (P2,s2,R))))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P2,(Comput (P2,s2,R))))) . (Comput (P2,s2,R)) is set
dom Cs3i is non empty finite V127() set
(Comput (P1,s1,(R + 1))) | (dom Cs3i) is Relation-like dom Cs3i -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
((Comput (P1,s1,(R + 1))) | (dom Cs3i)) . (0. (SCM k)) is set
(Comput (P1,s1,(R + 1))) . (0. (SCM k)) is set
(Comput (P2,s2,(R + 1))) | (dom Cs3i) is Relation-like dom Cs3i -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
((Comput (P2,s2,(R + 1))) | (dom Cs3i)) . (0. (SCM k)) is set
(Comput (P2,s2,(R + 1))) . (0. (SCM k)) is set
succ (IC (Comput (P2,s2,R))) is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() set
(IC (Comput (P2,s2,R))) + 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
R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
k is non empty non trivial V70() V95() V96() V97() V106() V113() V114() L11()
SCM k is non empty with_non-empty_values IC-Ins-separated strict V157(2) with_explicit_jumps IC-relocable V208(2) relocable IC-recognized CurIns-recognized AMI-Struct over 2
the carrier of (SCM k) is non empty set
the_Values_of (SCM k) is Relation-like non-empty non empty-yielding the carrier of (SCM k) -defined Function-like non empty total set
the Object-Kind of (SCM k) is Relation-like the carrier of (SCM k) -defined 2 -valued Function-like non empty total V21( the carrier of (SCM k),2) Element of K24(K25( the carrier of (SCM k),2))
K25( the carrier of (SCM k),2) is Relation-like non empty set
K24(K25( the carrier of (SCM k),2)) is non empty set
the ValuesF of (SCM k) is Relation-like 2 -defined Function-like non empty total V204() set
the Object-Kind of (SCM k) * the ValuesF of (SCM k) is Relation-like the carrier of (SCM k) -defined Function-like non empty total set
the InstructionsF of (SCM k) is Relation-like non empty standard-ins V139() J/A-independent V142() set
q is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
p is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
DataPart p is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible data-only set
NonZero (SCM k) is Element of K24( the carrier of (SCM k))
K24( the carrier of (SCM k)) is non empty set
[#] (SCM k) is non empty non proper Element of K24( the carrier of (SCM k))
0. (SCM k) is V51( SCM k) Element of the carrier of (SCM k)
the ZeroF of (SCM k) is Element of the carrier of (SCM k)
{(0. (SCM k))} is non empty trivial finite V39(1) V127() set
([#] (SCM k)) \ {(0. (SCM k))} is Element of K24( the carrier of (SCM k))
p | (NonZero (SCM k)) is Relation-like NonZero (SCM k) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible set
q +* (DataPart p) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
s1 is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like finite V127() non halt-free V204() set
Reloc (s1,R) is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like finite V127() non halt-free V204() set
IncAddr (s1,R) is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like finite V127() V204() set
K464((IncAddr (s1,R)),R) is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like finite V127() V204() set
s2 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty finite V127() s1 -autonomic V204() set
IncIC (s2,R) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
IC s2 is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
s2 . (0. (SCM k)) is set
(IC s2) + R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
Start-At (((IC s2) + R),(SCM k)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty finite V127() (IC s2) + R -started V204() set
(0. (SCM k)) .--> ((IC s2) + R) is Relation-like the carrier of (SCM k) -defined {(0. (SCM k))} -defined NAT -valued Function-like one-to-one constant non empty trivial finite V39(1) V124() V127() V204() set
{(0. (SCM k))} --> ((IC s2) + R) is Relation-like {(0. (SCM k))} -defined NAT -valued {((IC s2) + R)} -valued Function-like constant non empty total V21({(0. (SCM k))},{((IC s2) + R)}) finite V124() V127() V204() Element of K24(K25({(0. (SCM k))},{((IC s2) + R)}))
{((IC s2) + R)} is non empty trivial finite V36() V39(1) V127() set
K25({(0. (SCM k))},{((IC s2) + R)}) is Relation-like non empty finite V127() set
K24(K25({(0. (SCM k))},{((IC s2) + R)})) is non empty finite V36() V127() set
s2 +* (Start-At (((IC s2) + R),(SCM k))) is Relation-like the carrier of (SCM k) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible the_Values_of (SCM k) -compatible non empty finite V127() (IC s2) + R -started V204() set
DataPart s2 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() data-only V204() set
s2 | (NonZero (SCM k)) is Relation-like NonZero (SCM k) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
dom (DataPart s2) is finite V127() set
dom s2 is non empty finite V127() set
P1 is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like non empty total set
P2 is Relation-like NAT -defined the InstructionsF of (SCM k) -valued Function-like 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 k)) is set
Comput (P1,q,0) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
IC (Comput (P1,q,0)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P1,q,0)) . (0. (SCM k)) is set
dom s1 is finite V127() V187() set
i is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
Comput (P1,q,i) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
IC (Comput (P1,q,i)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P1,q,i)) . (0. (SCM k)) is set
(IC (Comput (P1,q,i))) + R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
Comput (P2,p,i) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
IC (Comput (P2,p,i)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P2,p,i)) . (0. (SCM k)) is set
CurInstr (P1,(Comput (P1,q,i))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
P1 /. (IC (Comput (P1,q,i))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IncAddr ((CurInstr (P1,(Comput (P1,q,i)))),R) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
CurInstr (P2,(Comput (P2,p,i))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
P2 /. (IC (Comput (P2,p,i))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
(Comput (P1,q,i)) | (dom (DataPart s2)) is Relation-like dom (DataPart s2) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
(Comput (P2,p,i)) | (dom (DataPart s2)) is Relation-like dom (DataPart s2) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
Comput (P1,(q +* (DataPart p)),i) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
DataPart (Comput (P1,(q +* (DataPart p)),i)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible data-only set
(Comput (P1,(q +* (DataPart p)),i)) | (NonZero (SCM k)) is Relation-like NonZero (SCM k) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible set
DataPart (Comput (P2,p,i)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible data-only set
(Comput (P2,p,i)) | (NonZero (SCM k)) is Relation-like NonZero (SCM k) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible set
i + 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
Comput (P1,q,(i + 1)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
IC (Comput (P1,q,(i + 1))) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P1,q,(i + 1))) . (0. (SCM k)) is set
(IC (Comput (P1,q,(i + 1)))) + R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
Comput (P2,p,(i + 1)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
IC (Comput (P2,p,(i + 1))) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P2,p,(i + 1))) . (0. (SCM k)) is set
CurInstr (P1,(Comput (P1,q,(i + 1)))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
P1 /. (IC (Comput (P1,q,(i + 1)))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IncAddr ((CurInstr (P1,(Comput (P1,q,(i + 1))))),R) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
CurInstr (P2,(Comput (P2,p,(i + 1)))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
P2 /. (IC (Comput (P2,p,(i + 1)))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
(Comput (P1,q,(i + 1))) | (dom (DataPart s2)) is Relation-like dom (DataPart s2) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
(Comput (P2,p,(i + 1))) | (dom (DataPart s2)) is Relation-like dom (DataPart s2) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
Comput (P1,(q +* (DataPart p)),(i + 1)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
DataPart (Comput (P1,(q +* (DataPart p)),(i + 1))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible data-only set
(Comput (P1,(q +* (DataPart p)),(i + 1))) | (NonZero (SCM k)) is Relation-like NonZero (SCM k) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible set
DataPart (Comput (P2,p,(i + 1))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible data-only set
(Comput (P2,p,(i + 1))) | (NonZero (SCM k)) is Relation-like NonZero (SCM k) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible set
Following (P2,(Comput (P2,p,i))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Exec ((CurInstr (P2,(Comput (P2,p,i)))),(Comput (P2,p,i))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))) is functional V125() V126() set
K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))) is functional non empty set
the Execution of (SCM k) is Relation-like the InstructionsF of (SCM k) -defined K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))) -valued Function-like non empty total V21( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))) Function-yielding V161() Element of K24(K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))))
K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))) is Relation-like non empty set
K24(K25( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))))) is non empty set
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P2,(Comput (P2,p,i))))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P2,(Comput (P2,p,i))))) . (Comput (P2,p,i)) is set
Cs1i is Int-like Element of the carrier of (SCM k)
Cs1i1 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
DataPart Cs1i1 is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible data-only set
Cs1i1 | (NonZero (SCM k)) is Relation-like NonZero (SCM k) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible set
dom (DataPart Cs1i1) is set
Cs1i1 is Int-like Element of the carrier of (SCM k)
dom (DataPart (Comput (P1,(q +* (DataPart p)),i))) is set
(Comput (P1,(q +* (DataPart p)),i)) . Cs1i1 is Element of the carrier of k
the carrier of k is non empty non trivial non empty-membered set
(DataPart (Comput (P1,(q +* (DataPart p)),i))) . Cs1i1 is set
(Comput (P2,p,i)) . Cs1i1 is Element of the carrier of k
dom (Comput (P1,q,(i + 1))) is non empty set
{(0. (SCM k))} is non empty trivial finite V39(1) V127() Element of K24( the carrier of (SCM k))
{(0. (SCM k))} \/ (NonZero (SCM k)) is non empty Element of K24( the carrier of (SCM k))
succ ((IC (Comput (P1,q,i))) + R) is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() set
((IC (Comput (P1,q,i))) + R) + 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
succ (IC (Comput (P1,q,i))) is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() set
(IC (Comput (P1,q,i))) + 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
(succ (IC (Comput (P1,q,i)))) + R 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
Cs3i1 is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
Cs3i1 + R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
dom (Reloc (s1,R)) is finite V127() V187() set
(Reloc (s1,R)) . (Cs3i1 + R) is set
P2 . (Cs3i1 + R) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
P2 . (IC (Comput (P2,p,(i + 1)))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
P1 . Cs3i1 is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
s1 . Cs3i1 is set
dom (Comput (P2,p,i)) is non empty set
(dom s2) /\ (NonZero (SCM k)) is finite V127() Element of K24( the carrier of (SCM k))
dom (DataPart (Comput (P2,p,i))) is set
dom (DataPart (Comput (P1,(q +* (DataPart p)),(i + 1)))) is set
dom (DataPart (Comput (P2,p,(i + 1)))) is set
I is set
(Comput (P1,(q +* (DataPart p)),(i + 1))) . I is set
(Comput (P2,p,(i + 1))) . I is set
(DataPart (Comput (P1,(q +* (DataPart p)),(i + 1)))) . I is set
(DataPart (Comput (P2,p,(i + 1)))) . I is set
I is set
(Comput (P1,(q +* (DataPart p)),(i + 1))) . I is set
(Comput (P1,(q +* (DataPart p)),i)) . I is set
(Comput (P2,p,(i + 1))) . I is set
(Comput (P2,p,i)) . I is set
(DataPart (Comput (P1,(q +* (DataPart p)),i))) . I is set
(DataPart (Comput (P1,(q +* (DataPart p)),(i + 1)))) . I is set
(DataPart (Comput (P2,p,(i + 1)))) . I is set
dom (Comput (P1,q,i)) is non empty set
dom (Comput (P2,p,(i + 1))) is non empty set
Following (P1,(Comput (P1,q,i))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
Exec ((CurInstr (P1,(Comput (P1,q,i)))),(Comput (P1,q,i))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P1,(Comput (P1,q,i))))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P1,(Comput (P1,q,i))))) . (Comput (P1,q,i)) is set
dom ((Comput (P1,q,i)) | (dom (DataPart s2))) is finite V127() set
(dom (Comput (P1,q,i))) /\ (dom (DataPart s2)) is finite V127() set
dom ((Comput (P1,q,(i + 1))) | (dom (DataPart s2))) is finite V127() set
(dom (Comput (P1,q,(i + 1)))) /\ (dom (DataPart s2)) is finite V127() set
dom ((Comput (P2,p,(i + 1))) | (dom (DataPart s2))) is finite V127() set
(dom (Comput (P2,p,(i + 1)))) /\ (dom (DataPart s2)) is finite V127() set
dom ((Comput (P2,p,i)) | (dom (DataPart s2))) is finite V127() set
(dom (Comput (P2,p,i))) /\ (dom (DataPart s2)) is finite V127() set
loc is Int-like Element of the carrier of (SCM k)
da is set
(Comput (P1,q,(i + 1))) . loc is Element of the carrier of k
(Comput (P1,q,i)) . loc is Element of the carrier of k
(Comput (P2,p,(i + 1))) . loc is Element of the carrier of k
(Comput (P2,p,i)) . loc is Element of the carrier of k
((Comput (P1,q,i)) | (dom (DataPart s2))) . loc is set
((Comput (P2,p,i)) | (dom (DataPart s2))) . loc is set
((Comput (P1,q,(i + 1))) | (dom (DataPart s2))) . da is set
((Comput (P2,p,(i + 1))) | (dom (DataPart s2))) . da is set
loc is Int-like Element of the carrier of (SCM k)
da is set
(Comput (P1,q,(i + 1))) . loc is Element of the carrier of k
(Comput (P2,p,(i + 1))) . loc is Element of the carrier of k
((Comput (P1,q,(i + 1))) | (dom (DataPart s2))) . da is set
((Comput (P2,p,(i + 1))) | (dom (DataPart s2))) . da is set
Following (P1,(Comput (P1,(q +* (DataPart p)),i))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
CurInstr (P1,(Comput (P1,(q +* (DataPart p)),i))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IC (Comput (P1,(q +* (DataPart p)),i)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P1,(q +* (DataPart p)),i)) . (0. (SCM k)) is set
P1 /. (IC (Comput (P1,(q +* (DataPart p)),i))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
Exec ((CurInstr (P1,(Comput (P1,(q +* (DataPart p)),i)))),(Comput (P1,(q +* (DataPart p)),i))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P1,(Comput (P1,(q +* (DataPart p)),i))))) is Relation-like Function-like Element of K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))))
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P1,(Comput (P1,(q +* (DataPart p)),i))))) . (Comput (P1,(q +* (DataPart p)),i)) is set
Exec ((CurInstr (P1,(Comput (P1,q,i)))),(Comput (P1,(q +* (DataPart p)),i))) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
K77( the InstructionsF of (SCM k),K75(K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k))),K213(( the Object-Kind of (SCM k) * the ValuesF of (SCM k)))), the Execution of (SCM k),(CurInstr (P1,(Comput (P1,q,i))))) . (Comput (P1,(q +* (DataPart p)),i)) is set
InsCode (CurInstr (P1,(Comput (P1,q,i)))) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM k)
InsCodes the InstructionsF of (SCM k) is non empty set
K55( the InstructionsF of (SCM k)) is set
halt (SCM k) is ins-loc-free V156(2, SCM k) V156(2, SCM k) with_explicit_jumps IC-relocable V207(2, SCM k) relocable Element of the InstructionsF of (SCM k)
halt the InstructionsF of (SCM k) is ins-loc-free with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
K47(0,{},{}) is set
InsCode (CurInstr (P1,(Comput (P1,q,i)))) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM k)
InsCodes the InstructionsF of (SCM k) is non empty set
K55( the InstructionsF of (SCM k)) is set
da is Int-like Element of the carrier of (SCM k)
loc is Int-like Element of the carrier of (SCM k)
da := loc is ins-loc-free V156(2, SCM k) with_explicit_jumps IC-relocable V207(2, SCM k) V209(2, SCM k) relocable Element of the InstructionsF of (SCM k)
(Exec ((CurInstr (P1,(Comput (P1,q,i)))),(Comput (P1,q,i)))) . (0. (SCM k)) is set
(Comput (P1,(q +* (DataPart p)),i)) . loc is Element of the carrier of k
(Comput (P2,p,i)) . loc is Element of the carrier of k
x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,q,(i + 1))) . d is Element of the carrier of k
(Comput (P1,q,i)) . loc is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
((Comput (P1,q,(i + 1))) | (dom (DataPart s2))) . x is set
((Comput (P2,p,(i + 1))) | (dom (DataPart s2))) . x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,q,(i + 1))) . d is Element of the carrier of k
(Comput (P1,q,i)) . d is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
(Comput (P2,p,i)) . d is Element of the carrier of k
((Comput (P1,q,(i + 1))) | (dom (DataPart s2))) . x is set
((Comput (P2,p,(i + 1))) | (dom (DataPart s2))) . x is set
d is Int-like Element of the carrier of (SCM k)
x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),(i + 1))) . d is Element of the carrier of k
(DataPart (Comput (P1,(q +* (DataPart p)),(i + 1)))) . x is set
(DataPart (Comput (P2,p,(i + 1)))) . x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,(q +* (DataPart p)),(i + 1))) . d is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),i)) . d is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
(Comput (P2,p,i)) . d is Element of the carrier of k
(DataPart (Comput (P1,(q +* (DataPart p)),(i + 1)))) . x is set
(DataPart (Comput (P2,p,(i + 1)))) . x is set
d is Int-like Element of the carrier of (SCM k)
InsCode (CurInstr (P1,(Comput (P1,q,i)))) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM k)
InsCodes the InstructionsF of (SCM k) is non empty set
K55( the InstructionsF of (SCM k)) is set
da is Int-like Element of the carrier of (SCM k)
loc is Int-like Element of the carrier of (SCM k)
AddTo (da,loc) is ins-loc-free V156(2, SCM k) with_explicit_jumps IC-relocable V207(2, SCM k) V209(2, SCM k) relocable Element of the InstructionsF of (SCM k)
(Exec ((CurInstr (P1,(Comput (P1,q,i)))),(Comput (P1,q,i)))) . (0. (SCM k)) is set
(Comput (P1,(q +* (DataPart p)),i)) . da is Element of the carrier of k
(Comput (P2,p,i)) . da is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),i)) . loc is Element of the carrier of k
(Comput (P2,p,i)) . loc is Element of the carrier of k
x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,q,(i + 1))) . d is Element of the carrier of k
(Comput (P1,q,i)) . da is Element of the carrier of k
(Comput (P1,q,i)) . loc is Element of the carrier of k
((Comput (P1,q,i)) . da) + ((Comput (P1,q,i)) . loc) is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
((Comput (P2,p,i)) . da) + ((Comput (P2,p,i)) . loc) is Element of the carrier of k
((Comput (P1,q,(i + 1))) | (dom (DataPart s2))) . x is set
((Comput (P2,p,(i + 1))) | (dom (DataPart s2))) . x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,q,(i + 1))) . d is Element of the carrier of k
(Comput (P1,q,i)) . d is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
(Comput (P2,p,i)) . d is Element of the carrier of k
((Comput (P1,q,(i + 1))) | (dom (DataPart s2))) . x is set
((Comput (P2,p,(i + 1))) | (dom (DataPart s2))) . x is set
d is Int-like Element of the carrier of (SCM k)
x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
((Comput (P2,p,i)) . da) + ((Comput (P2,p,i)) . loc) is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),(i + 1))) . d is Element of the carrier of k
((Comput (P1,(q +* (DataPart p)),i)) . da) + ((Comput (P1,(q +* (DataPart p)),i)) . loc) is Element of the carrier of k
(DataPart (Comput (P1,(q +* (DataPart p)),(i + 1)))) . x is set
(DataPart (Comput (P2,p,(i + 1)))) . x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,(q +* (DataPart p)),(i + 1))) . d is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),i)) . d is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
(Comput (P2,p,i)) . d is Element of the carrier of k
(DataPart (Comput (P1,(q +* (DataPart p)),(i + 1)))) . x is set
(DataPart (Comput (P2,p,(i + 1)))) . x is set
d is Int-like Element of the carrier of (SCM k)
InsCode (CurInstr (P1,(Comput (P1,q,i)))) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM k)
InsCodes the InstructionsF of (SCM k) is non empty set
K55( the InstructionsF of (SCM k)) is set
da is Int-like Element of the carrier of (SCM k)
loc is Int-like Element of the carrier of (SCM k)
SubFrom (da,loc) is ins-loc-free V156(2, SCM k) with_explicit_jumps IC-relocable V207(2, SCM k) V209(2, SCM k) relocable Element of the InstructionsF of (SCM k)
(Exec ((CurInstr (P1,(Comput (P1,q,i)))),(Comput (P1,q,i)))) . (0. (SCM k)) is set
(Comput (P1,(q +* (DataPart p)),i)) . da is Element of the carrier of k
(Comput (P2,p,i)) . da is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),i)) . loc is Element of the carrier of k
(Comput (P2,p,i)) . loc is Element of the carrier of k
x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,q,(i + 1))) . d is Element of the carrier of k
(Comput (P1,q,i)) . da is Element of the carrier of k
(Comput (P1,q,i)) . loc is Element of the carrier of k
((Comput (P1,q,i)) . da) - ((Comput (P1,q,i)) . loc) is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
((Comput (P2,p,i)) . da) - ((Comput (P2,p,i)) . loc) is Element of the carrier of k
((Comput (P1,q,(i + 1))) | (dom (DataPart s2))) . x is set
((Comput (P2,p,(i + 1))) | (dom (DataPart s2))) . x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,q,(i + 1))) . d is Element of the carrier of k
(Comput (P1,q,i)) . d is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
(Comput (P2,p,i)) . d is Element of the carrier of k
((Comput (P1,q,(i + 1))) | (dom (DataPart s2))) . x is set
((Comput (P2,p,(i + 1))) | (dom (DataPart s2))) . x is set
d is Int-like Element of the carrier of (SCM k)
x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
((Comput (P2,p,i)) . da) - ((Comput (P2,p,i)) . loc) is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),(i + 1))) . d is Element of the carrier of k
((Comput (P1,(q +* (DataPart p)),i)) . da) - ((Comput (P1,(q +* (DataPart p)),i)) . loc) is Element of the carrier of k
(DataPart (Comput (P1,(q +* (DataPart p)),(i + 1)))) . x is set
(DataPart (Comput (P2,p,(i + 1)))) . x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,(q +* (DataPart p)),(i + 1))) . d is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),i)) . d is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
(Comput (P2,p,i)) . d is Element of the carrier of k
(DataPart (Comput (P1,(q +* (DataPart p)),(i + 1)))) . x is set
(DataPart (Comput (P2,p,(i + 1)))) . x is set
d is Int-like Element of the carrier of (SCM k)
InsCode (CurInstr (P1,(Comput (P1,q,i)))) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM k)
InsCodes the InstructionsF of (SCM k) is non empty set
K55( the InstructionsF of (SCM k)) is set
da is Int-like Element of the carrier of (SCM k)
loc is Int-like Element of the carrier of (SCM k)
MultBy (da,loc) is ins-loc-free V156(2, SCM k) with_explicit_jumps IC-relocable V207(2, SCM k) V209(2, SCM k) relocable Element of the InstructionsF of (SCM k)
(Exec ((CurInstr (P1,(Comput (P1,q,i)))),(Comput (P1,q,i)))) . (0. (SCM k)) is set
(Comput (P1,(q +* (DataPart p)),i)) . da is Element of the carrier of k
(Comput (P2,p,i)) . da is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),i)) . loc is Element of the carrier of k
(Comput (P2,p,i)) . loc is Element of the carrier of k
x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,q,(i + 1))) . d is Element of the carrier of k
(Comput (P1,q,i)) . da is Element of the carrier of k
(Comput (P1,q,i)) . loc is Element of the carrier of k
((Comput (P1,q,i)) . da) * ((Comput (P1,q,i)) . loc) is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
((Comput (P2,p,i)) . da) * ((Comput (P2,p,i)) . loc) is Element of the carrier of k
((Comput (P1,q,(i + 1))) | (dom (DataPart s2))) . x is set
((Comput (P2,p,(i + 1))) | (dom (DataPart s2))) . x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,q,(i + 1))) . d is Element of the carrier of k
(Comput (P1,q,i)) . d is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
(Comput (P2,p,i)) . d is Element of the carrier of k
((Comput (P1,q,(i + 1))) | (dom (DataPart s2))) . x is set
((Comput (P2,p,(i + 1))) | (dom (DataPart s2))) . x is set
d is Int-like Element of the carrier of (SCM k)
x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
((Comput (P2,p,i)) . da) * ((Comput (P2,p,i)) . loc) is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),(i + 1))) . d is Element of the carrier of k
((Comput (P1,(q +* (DataPart p)),i)) . da) * ((Comput (P1,(q +* (DataPart p)),i)) . loc) is Element of the carrier of k
(DataPart (Comput (P1,(q +* (DataPart p)),(i + 1)))) . x is set
(DataPart (Comput (P2,p,(i + 1)))) . x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,(q +* (DataPart p)),(i + 1))) . d is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),i)) . d is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
(Comput (P2,p,i)) . d is Element of the carrier of k
(DataPart (Comput (P1,(q +* (DataPart p)),(i + 1)))) . x is set
(DataPart (Comput (P2,p,(i + 1)))) . x is set
d is Int-like Element of the carrier of (SCM k)
InsCode (CurInstr (P1,(Comput (P1,q,i)))) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM k)
InsCodes the InstructionsF of (SCM k) is non empty set
K55( the InstructionsF of (SCM k)) is set
da is Int-like Element of the carrier of (SCM k)
loc is Element of the carrier of k
da := loc is ins-loc-free V156(2, SCM k) with_explicit_jumps IC-relocable V207(2, SCM k) V209(2, SCM k) relocable Element of the InstructionsF of (SCM k)
(Exec ((CurInstr (P1,(Comput (P1,q,i)))),(Comput (P1,q,i)))) . (0. (SCM k)) is set
x is set
d is Int-like Element of the carrier of (SCM k)
((Comput (P1,q,(i + 1))) | (dom (DataPart s2))) . x is set
(Comput (P1,q,(i + 1))) . d is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
((Comput (P2,p,(i + 1))) | (dom (DataPart s2))) . x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,q,(i + 1))) . d is Element of the carrier of k
(Comput (P1,q,i)) . d is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
(Comput (P2,p,i)) . d is Element of the carrier of k
((Comput (P1,q,(i + 1))) | (dom (DataPart s2))) . x is set
((Comput (P2,p,(i + 1))) | (dom (DataPart s2))) . x is set
d is Int-like Element of the carrier of (SCM k)
x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),(i + 1))) . d is Element of the carrier of k
(DataPart (Comput (P1,(q +* (DataPart p)),(i + 1)))) . x is set
(DataPart (Comput (P2,p,(i + 1)))) . x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,(q +* (DataPart p)),(i + 1))) . d is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),i)) . d is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
(Comput (P2,p,i)) . d is Element of the carrier of k
(DataPart (Comput (P1,(q +* (DataPart p)),(i + 1)))) . x is set
(DataPart (Comput (P2,p,(i + 1)))) . x is set
d is Int-like Element of the carrier of (SCM k)
InsCode (CurInstr (P1,(Comput (P1,q,i)))) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM k)
InsCodes the InstructionsF of (SCM k) is non empty set
K55( the InstructionsF of (SCM k)) is set
da is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
goto (da,k) is non ins-loc-free V156(2, SCM k) with_explicit_jumps IC-relocable V207(2, SCM k) V209(2, SCM k) relocable Element of the InstructionsF of (SCM k)
da + R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
goto ((da + R),k) is non ins-loc-free V156(2, SCM k) with_explicit_jumps IC-relocable V207(2, SCM k) V209(2, SCM k) relocable Element of the InstructionsF of (SCM k)
loc is set
x is Int-like Element of the carrier of (SCM k)
(Comput (P1,q,(i + 1))) . x is Element of the carrier of k
(Comput (P1,q,i)) . x is Element of the carrier of k
(Comput (P2,p,(i + 1))) . x is Element of the carrier of k
(Comput (P2,p,i)) . x is Element of the carrier of k
((Comput (P1,q,(i + 1))) | (dom (DataPart s2))) . loc is set
((Comput (P2,p,(i + 1))) | (dom (DataPart s2))) . loc is set
loc is set
x is Int-like Element of the carrier of (SCM k)
(Comput (P1,(q +* (DataPart p)),(i + 1))) . x is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),i)) . x is Element of the carrier of k
(Comput (P2,p,(i + 1))) . x is Element of the carrier of k
(Comput (P2,p,i)) . x is Element of the carrier of k
(DataPart (Comput (P1,(q +* (DataPart p)),(i + 1)))) . loc is set
(DataPart (Comput (P2,p,(i + 1)))) . loc is set
InsCode (CurInstr (P1,(Comput (P1,q,i)))) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM k)
InsCodes the InstructionsF of (SCM k) is non empty set
K55( the InstructionsF of (SCM k)) is set
loc is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
da is Int-like Element of the carrier of (SCM k)
da =0_goto loc is non ins-loc-free V156(2, SCM k) with_explicit_jumps IC-relocable V207(2, SCM k) V209(2, SCM k) relocable Element of the InstructionsF of (SCM k)
(Comput (P1,q,i)) . da is Element of the carrier of k
0. k is V51(k) Element of the carrier of k
the ZeroF of k is Element of the carrier of k
loc + R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P1,q,i)) . da is Element of the carrier of k
0. k is V51(k) Element of the carrier of k
the ZeroF of k is Element of the carrier of k
succ (IC (Comput (P2,p,i))) is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() set
(IC (Comput (P2,p,i))) + 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
(Comput (P1,q,i)) . da is Element of the carrier of k
0. k is V51(k) Element of the carrier of k
the ZeroF of k is Element of the carrier of k
loc + R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
succ (IC (Comput (P2,p,i))) is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() set
(IC (Comput (P2,p,i))) + 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
(Comput (P1,q,i)) . da is Element of the carrier of k
0. k is V51(k) Element of the carrier of k
the ZeroF of k is Element of the carrier of k
loc + R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
succ (IC (Comput (P2,p,i))) is V1() V3() non empty epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() non with_non-empty_elements V170() set
(IC (Comput (P2,p,i))) + 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
da =0_goto (loc + R) is non ins-loc-free V156(2, SCM k) with_explicit_jumps IC-relocable V207(2, SCM k) V209(2, SCM k) relocable Element of the InstructionsF of (SCM k)
(Comput (P2,p,i)) . da is Element of the carrier of k
(Comput (P2,p,i)) . da is Element of the carrier of k
(Comput (P2,p,i)) . da is Element of the carrier of k
(Comput (P2,p,i)) . da is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),i)) . da is Element of the carrier of k
x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,q,(i + 1))) . d is Element of the carrier of k
(Comput (P1,q,i)) . d is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
(Comput (P2,p,i)) . d is Element of the carrier of k
((Comput (P1,q,(i + 1))) | (dom (DataPart s2))) . x is set
((Comput (P2,p,(i + 1))) | (dom (DataPart s2))) . x is set
x is set
d is Int-like Element of the carrier of (SCM k)
(Comput (P1,(q +* (DataPart p)),(i + 1))) . d is Element of the carrier of k
(Comput (P1,(q +* (DataPart p)),i)) . d is Element of the carrier of k
(Comput (P2,p,(i + 1))) . d is Element of the carrier of k
(Comput (P2,p,i)) . d is Element of the carrier of k
(DataPart (Comput (P1,(q +* (DataPart p)),(i + 1)))) . x is set
(DataPart (Comput (P2,p,(i + 1)))) . x is set
InsCode (CurInstr (P1,(Comput (P1,q,i)))) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of InsCodes the InstructionsF of (SCM k)
InsCodes the InstructionsF of (SCM k) is non empty set
K55( the InstructionsF of (SCM k)) is set
DataPart (IncIC (s2,R)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() data-only V204() set
(IncIC (s2,R)) | (NonZero (SCM k)) is Relation-like NonZero (SCM k) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
(Comput (P1,q,0)) | (dom (DataPart s2)) is Relation-like dom (DataPart s2) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
q | (dom (DataPart s2)) is Relation-like dom (DataPart s2) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
p | (dom (DataPart s2)) is Relation-like dom (DataPart s2) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
Comput (P2,p,0) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
(Comput (P2,p,0)) | (dom (DataPart s2)) is Relation-like dom (DataPart s2) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
Comput (P1,(q +* (DataPart p)),0) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
DataPart (Comput (P1,(q +* (DataPart p)),0)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible data-only set
(Comput (P1,(q +* (DataPart p)),0)) | (NonZero (SCM k)) is Relation-like NonZero (SCM k) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible set
DataPart (q +* (DataPart p)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible data-only set
(q +* (DataPart p)) | (NonZero (SCM k)) is Relation-like NonZero (SCM k) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible set
DataPart (Comput (P2,p,0)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible data-only set
(Comput (P2,p,0)) | (NonZero (SCM k)) is Relation-like NonZero (SCM k) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible set
dom (IncIC (s2,R)) is finite V127() set
(IC (Comput (P1,q,0))) + R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(IC q) + R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
IC (IncIC (s2,R)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(IncIC (s2,R)) . (0. (SCM k)) is set
IC p is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
p . (0. (SCM k)) is set
IC (Comput (P2,p,0)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P2,p,0)) . (0. (SCM k)) is set
dom (Reloc (s1,R)) is finite V127() V187() set
P2 /. (IC p) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
P2 . (IC p) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
CurInstr (P2,(Comput (P2,p,0))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
P2 /. (IC (Comput (P2,p,0))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
P2 . (IC (IncIC (s2,R))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
P2 . ((IC s2) + R) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
(Reloc (s1,R)) . ((IC s2) + R) is set
s1 . (IC s2) is set
P1 . (IC q) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
CurInstr (P1,q) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
P1 /. (IC q) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
CurInstr (P1,(Comput (P1,q,0))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
P1 /. (IC (Comput (P1,q,0))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IncAddr ((CurInstr (P1,(Comput (P1,q,0)))),R) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IncAddr ((CurInstr (P1,q)),R) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
DPp is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
Comput (P1,q,DPp) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
IC (Comput (P1,q,DPp)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P1,q,DPp)) . (0. (SCM k)) is set
(IC (Comput (P1,q,DPp))) + R is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
Comput (P2,p,DPp) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
IC (Comput (P2,p,DPp)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P2,p,DPp)) . (0. (SCM k)) is set
i is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
Comput (P1,q,i) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
CurInstr (P1,(Comput (P1,q,i))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IC (Comput (P1,q,i)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P1,q,i)) . (0. (SCM k)) is set
P1 /. (IC (Comput (P1,q,i))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IncAddr ((CurInstr (P1,(Comput (P1,q,i)))),R) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
Comput (P2,p,i) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
CurInstr (P2,(Comput (P2,p,i))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
IC (Comput (P2,p,i)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P2,p,i)) . (0. (SCM k)) is set
P2 /. (IC (Comput (P2,p,i))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM k)
Cs2i1 is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
Comput (P1,q,Cs2i1) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
(Comput (P1,q,Cs2i1)) | (dom (DataPart s2)) is Relation-like dom (DataPart s2) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
Comput (P2,p,Cs2i1) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
(Comput (P2,p,Cs2i1)) | (dom (DataPart s2)) is Relation-like dom (DataPart s2) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible finite V127() V204() set
Cs3i is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
Comput (P1,(q +* (DataPart p)),Cs3i) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
DataPart (Comput (P1,(q +* (DataPart p)),Cs3i)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible data-only set
(Comput (P1,(q +* (DataPart p)),Cs3i)) | (NonZero (SCM k)) is Relation-like NonZero (SCM k) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible set
Comput (P2,p,Cs3i) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible non empty total set
DataPart (Comput (P2,p,Cs3i)) is Relation-like the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible data-only set
(Comput (P2,p,Cs3i)) | (NonZero (SCM k)) is Relation-like NonZero (SCM k) -defined the carrier of (SCM k) -defined Function-like the_Values_of (SCM k) -compatible 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 IC-recognized CurIns-recognized 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
q is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like finite V127() non halt-free V204() set
p is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty finite V127() q -autonomic V204() set
s1 is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
k is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
IncIC (p,k) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible finite V127() V204() set
IC p 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)
p . (0. (SCM R)) is set
(IC p) + k is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
Start-At (((IC p) + 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 p) + k -started V204() set
(0. (SCM R)) .--> ((IC p) + 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))} is non empty trivial finite V39(1) V127() set
{(0. (SCM R))} --> ((IC p) + k) is Relation-like {(0. (SCM R))} -defined NAT -valued {((IC p) + k)} -valued Function-like constant non empty total V21({(0. (SCM R))},{((IC p) + k)}) finite V124() V127() V204() Element of K24(K25({(0. (SCM R))},{((IC p) + k)}))
{((IC p) + k)} is non empty trivial finite V36() V39(1) V127() set
K25({(0. (SCM R))},{((IC p) + k)}) is Relation-like non empty finite V127() set
K24(K25({(0. (SCM R))},{((IC p) + k)})) is non empty finite V36() V127() set
p +* (Start-At (((IC p) + 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 finite V127() (IC p) + k -started V204() set
s2 is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
P1 is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty total set
Reloc (q,k) is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like finite V127() non halt-free V204() set
IncAddr (q,k) is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like finite V127() V204() set
K464((IncAddr (q,k)),k) is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like finite V127() V204() set
P2 is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty total set
s is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
Comput (P1,s1,s) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
CurInstr (P1,(Comput (P1,s1,s))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
IC (Comput (P1,s1,s)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P1,s1,s)) . (0. (SCM R)) is set
P1 /. (IC (Comput (P1,s1,s))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
IncAddr ((CurInstr (P1,(Comput (P1,s1,s)))),k) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
Comput (P2,s2,s) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
CurInstr (P2,(Comput (P2,s2,s))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
IC (Comput (P2,s2,s)) is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
(Comput (P2,s2,s)) . (0. (SCM R)) is set
P2 /. (IC (Comput (P2,s2,s))) is with_explicit_jumps IC-relocable relocable Element of the InstructionsF of (SCM R)
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
k is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
q is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like finite V127() non halt-free V204() set
Reloc (q,k) is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like finite V127() non halt-free V204() set
IncAddr (q,k) is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like finite V127() V204() set
K464((IncAddr (q,k)),k) is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like finite V127() V204() set
p is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty finite V127() q -autonomic V204() set
IncIC (p,k) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible finite V127() V204() set
IC p 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)
p . (0. (SCM R)) is set
(IC p) + k is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
Start-At (((IC p) + 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 p) + k -started V204() set
(0. (SCM R)) .--> ((IC p) + 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))} is non empty trivial finite V39(1) V127() set
{(0. (SCM R))} --> ((IC p) + k) is Relation-like {(0. (SCM R))} -defined NAT -valued {((IC p) + k)} -valued Function-like constant non empty total V21({(0. (SCM R))},{((IC p) + k)}) finite V124() V127() V204() Element of K24(K25({(0. (SCM R))},{((IC p) + k)}))
{((IC p) + k)} is non empty trivial finite V36() V39(1) V127() set
K25({(0. (SCM R))},{((IC p) + k)}) is Relation-like non empty finite V127() set
K24(K25({(0. (SCM R))},{((IC p) + k)})) is non empty finite V36() V127() set
p +* (Start-At (((IC p) + 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 finite V127() (IC p) + k -started V204() set
DataPart p 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))
([#] (SCM R)) \ {(0. (SCM R))} is Element of K24( the carrier of (SCM R))
p | (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 (DataPart p) is finite V127() set
s1 is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
s2 is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
P1 is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty total set
P2 is Relation-like NAT -defined the InstructionsF of (SCM R) -valued Function-like non empty total set
s is V1() V3() epsilon-transitive epsilon-connected ordinal natural V31() finite V37() V103() V127() V170() Element of NAT
Comput (P1,s1,s) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
(Comput (P1,s1,s)) | (dom (DataPart p)) is Relation-like dom (DataPart p) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible finite V127() V204() set
Comput (P2,s2,s) is Relation-like the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible non empty total set
(Comput (P2,s2,s)) | (dom (DataPart p)) is Relation-like dom (DataPart p) -defined the carrier of (SCM R) -defined Function-like the_Values_of (SCM R) -compatible finite V127() V204() set