REAL is non empty V20() V33() V45() set
NAT is V9() V10() V11() non empty Element of K43(REAL)
K43(REAL) is set
SCM+FSA is non empty with_non-empty_values IC-Ins-separated strict V91(3) V101(3) with_explicit_jumps IC-relocable V146(3) AMI-Struct over 3
3 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
K524() is set
K501(NAT,K524()) is Element of K524()
K517() is non empty set
K527() is Relation-like Function-like V30(K524(),3) Element of K43(K44(K524(),3))
K44(K524(),3) is Relation-like set
K43(K44(K524(),3)) is set
K528() is Relation-like 3 -defined non empty Function-like total set
K535() is Relation-like Function-like V30(K517(),K97(K221((K527() (#) K528())),K221((K527() (#) K528())))) Element of K43(K44(K517(),K97(K221((K527() (#) K528())),K221((K527() (#) K528())))))
K527() (#) K528() is Relation-like Function-like set
K221((K527() (#) K528())) is set
K97(K221((K527() (#) K528())),K221((K527() (#) K528()))) is set
K44(K517(),K97(K221((K527() (#) K528())),K221((K527() (#) K528())))) is Relation-like set
K43(K44(K517(),K97(K221((K527() (#) K528())),K221((K527() (#) K528()))))) is set
AMI-Struct(# K524(),K501(NAT,K524()),K517(),K527(),K528(),K535() #) is strict AMI-Struct over 3
the carrier of SCM+FSA is non empty set
NAT is V9() V10() V11() non empty set
K43(NAT) is set
K43(NAT) is set
9 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Segm 9 is Element of K43(NAT)
Int-Locations is non empty set
K258() is set
K43(K258()) is set
2 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
K44(K258(),2) is Relation-like set
K43(K44(K258(),2)) is set
K260() is Relation-like Function-like V30(K258(),2) Element of K43(K44(K258(),2))
K261() is Relation-like 2 -defined non empty Function-like total set
K260() (#) K261() is Relation-like Function-like set
K221((K260() (#) K261())) is set
K252() is non empty set
K97(K221((K260() (#) K261())),K221((K260() (#) K261()))) is set
K44(K252(),K97(K221((K260() (#) K261())),K221((K260() (#) K261())))) is Relation-like set
K43(K44(K252(),K97(K221((K260() (#) K261())),K221((K260() (#) K261()))))) is set
K43( the carrier of SCM+FSA) is set
the InstructionsF of SCM+FSA is Relation-like non empty standard-ins V53() J/A-independent V56() set
INT is non empty V20() V33() V45() set
Int-Locations is non empty Element of K43( the carrier of SCM+FSA)
K295(Int-Locations) is V98() set
K43(Int-Locations) is set
FinSeq-Locations is non empty V20() V33() V45() Element of K43( the carrier of SCM+FSA)
K526() is Element of K43(K524())
K43(K524()) is set
K295(FinSeq-Locations) is V98() set
K43(FinSeq-Locations) is set
COMPLEX is non empty V20() V33() V45() set
RAT is non empty V20() V33() V45() set
K489() is non empty with_non-empty_values IC-Ins-separated strict strict V91(2) AMI-Struct over 2
the InstructionsF of K489() is Relation-like non empty standard-ins V53() J/A-independent V56() set
the carrier of K489() is non empty set
the_Values_of K489() is Relation-like non-empty non empty-yielding the carrier of K489() -defined non empty Function-like total set
the Object-Kind of K489() is Relation-like Function-like V30( the carrier of K489(),2) Element of K43(K44( the carrier of K489(),2))
K44( the carrier of K489(),2) is Relation-like set
K43(K44( the carrier of K489(),2)) is set
the ValuesF of K489() is Relation-like 2 -defined non empty Function-like total set
the Object-Kind of K489() (#) the ValuesF of K489() is Relation-like Function-like set
K516() is set
the_Values_of SCM+FSA is Relation-like non-empty non empty-yielding the carrier of SCM+FSA -defined non empty Function-like total set
the Object-Kind of SCM+FSA is Relation-like Function-like V30( the carrier of SCM+FSA,3) Element of K43(K44( the carrier of SCM+FSA,3))
K44( the carrier of SCM+FSA,3) is Relation-like set
K43(K44( the carrier of SCM+FSA,3)) is set
the ValuesF of SCM+FSA is Relation-like 3 -defined non empty Function-like total set
the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA is Relation-like Function-like set
K44(NAT,K43(NAT)) is Relation-like set
K43(K44(NAT,K43(NAT))) is set
FinPartSt SCM+FSA is non empty Element of K43(K225((the_Values_of SCM+FSA)))
K225((the_Values_of SCM+FSA)) is set
K43(K225((the_Values_of SCM+FSA))) is set
{ b1 where b1 is Element of K225((the_Values_of SCM+FSA)) : b1 is V33() } is set
K44((FinPartSt SCM+FSA),(FinPartSt SCM+FSA)) is Relation-like set
K43(K44((FinPartSt SCM+FSA),(FinPartSt SCM+FSA))) is set
1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
{} is ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() empty Function-like one-to-one constant functional V27() integer V33() V34() V37() V41() V42() V43() V110() V143() V144() Function-yielding V153() V156() set
0 is ext-real non positive non negative Relation-like non-empty empty-yielding NAT -defined V9() V10() V11() V13() V14() V15() empty Function-like one-to-one constant functional V27() integer V33() V34() V37() V41() V42() V43() V110() V143() V144() Function-yielding V153() V156() Element of NAT
IC is V70( SCM+FSA ) Element of the carrier of SCM+FSA
halt SCM+FSA is ins-loc-free V90(3, SCM+FSA ) V100(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
halt the InstructionsF of SCM+FSA is ins-loc-free with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K26(0,{},{}) is set
NonZero SCM+FSA is Element of K43( the carrier of SCM+FSA)
Int-Locations \/ FinSeq-Locations is non empty Element of K43( the carrier of SCM+FSA)
Start-At (0,SCM+FSA) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible V33() 0 -started V144() set
(IC ) .--> 0 is Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued non empty V20() Function-like one-to-one constant V33() V144() Function-yielding V153() set
{(IC )} is non empty V33() set
{(IC )} --> 0 is Relation-like {(IC )} -defined NAT -valued non empty Function-like constant total V30({(IC )},{0}) V33() V144() Function-yielding V153() Element of K43(K44({(IC )},{0}))
{0} is non empty functional V33() V37() set
K44({(IC )},{0}) is Relation-like V33() set
K43(K44({(IC )},{0})) is V33() V37() set
K444(NAT,0,1) is non empty V33() Element of K43(NAT)
K259() is non empty Element of K43(K258())
intloc 0 is V94() read-only Element of the carrier of SCM+FSA
K498(0) is V94() Element of the carrier of K489()
(intloc 0) .--> 1 is Relation-like the carrier of SCM+FSA -defined {(intloc 0)} -defined {(intloc 0)} -defined NAT -valued non empty V20() Function-like one-to-one constant the_Values_of SCM+FSA -compatible V33() data-only V144() set
{(intloc 0)} is non empty V33() set
{(intloc 0)} --> 1 is Relation-like non-empty non empty-yielding {(intloc 0)} -defined NAT -valued non empty Function-like constant total V30({(intloc 0)},{1}) V33() V144() Element of K43(K44({(intloc 0)},{1}))
{1} is non empty V33() V44() V45() set
K44({(intloc 0)},{1}) is Relation-like V33() set
K43(K44({(intloc 0)},{1})) is V33() V37() set
Initialize ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible V33() 0 -started V144() set
((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible V33() 0 -started V144() set
dom (Initialize ((intloc 0) .--> 1)) is V33() set
K444( the carrier of SCM+FSA,(intloc 0),(IC )) is non empty V33() Element of K43( the carrier of SCM+FSA)
(Initialize ((intloc 0) .--> 1)) . (intloc 0) is set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
D +* s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
P is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Initialized P is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
P +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
Result ((D +* s),(Initialized P)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Macro (halt SCM+FSA) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
K207(SCM+FSA,(halt SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
stop K207(SCM+FSA,(halt SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
dom (Start-At (0,SCM+FSA)) is non empty V33() set
Comput (D,s,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (D,s,0)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (D,s,0)) . (IC ) is set
dom D is non empty set
CurInstr (D,(Comput (D,s,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D /. (IC (Comput (D,s,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (Macro (halt SCM+FSA)) is non empty V33() set
{0,1} is non empty V33() set
IC s is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
s . (IC ) is set
D . (IC s) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Start-At (0,SCM+FSA)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Start-At (0,SCM+FSA)) . (IC ) is set
D . (IC (Start-At (0,SCM+FSA))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (halt SCM+FSA)) . 0 is set
dom (Macro (halt SCM+FSA)) is non empty V33() set
{0,1} is non empty V33() set
P is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
P . (intloc 0) is ext-real V27() integer V110() set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
A is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (D,P,A) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Comput (D,P,A)) . (intloc 0) is ext-real V27() integer V110() set
Comput (D,P,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
dom D is non empty set
IC P is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
P . (IC ) is set
D /. (IC P) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D . (IC P) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (D,P) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Macro (halt SCM+FSA)) . 0 is set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() parahalting V144() set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() parahalting V144() set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC s is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
s . (IC ) is set
goto (IC s) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) V100(3, SCM+FSA ) V102(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K495((IC s)) is Element of the InstructionsF of K489()
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
P +* ((IC s),(goto (IC s))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
dom P is non empty set
dom (P +* ((IC s),(goto (IC s)))) is non empty set
A is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((P +* ((IC s),(goto (IC s)))),s,A) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((P +* ((IC s),(goto (IC s)))),s,A)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* ((IC s),(goto (IC s)))),s,A)) . (IC ) is set
CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,A))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(P +* ((IC s),(goto (IC s)))) /. (IC (Comput ((P +* ((IC s),(goto (IC s)))),s,A))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(P +* ((IC s),(goto (IC s)))) . (IC s) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
A + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput ((P +* ((IC s),(goto (IC s)))),s,(A + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((P +* ((IC s),(goto (IC s)))),s,(A + 1))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* ((IC s),(goto (IC s)))),s,(A + 1))) . (IC ) is set
Following ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,A))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Exec ((CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,A)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,A))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)) is set
K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V30( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) Element of K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))))
K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) is Relation-like set
K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))))) is set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,A))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,A))))) . (Comput ((P +* ((IC s),(goto (IC s)))),s,A)) is set
IC (Following ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,A)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Following ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,A)))) . (IC ) is set
A is ext-real non negative V9() V10() V11() V15() V27() integer V110() set
Comput ((P +* ((IC s),(goto (IC s)))),s,A) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((P +* ((IC s),(goto (IC s)))),s,A)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* ((IC s),(goto (IC s)))),s,A)) . (IC ) is set
CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,A))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(P +* ((IC s),(goto (IC s)))) /. (IC (Comput ((P +* ((IC s),(goto (IC s)))),s,A))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput ((P +* ((IC s),(goto (IC s)))),s,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((P +* ((IC s),(goto (IC s)))),s,0)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* ((IC s),(goto (IC s)))),s,0)) . (IC ) is set
I is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((P +* ((IC s),(goto (IC s)))),s,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr ((P +* ((IC s),(goto (IC s)))),(Comput ((P +* ((IC s),(goto (IC s)))),s,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((P +* ((IC s),(goto (IC s)))),s,I)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* ((IC s),(goto (IC s)))),s,I)) . (IC ) is set
(P +* ((IC s),(goto (IC s)))) /. (IC (Comput ((P +* ((IC s),(goto (IC s)))),s,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(P +* ((IC s),(goto (IC s)))) . (IC (Comput ((P +* ((IC s),(goto (IC s)))),s,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
P is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
K306(NAT,s) is non empty V33() Element of K43(NAT)
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
A is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (D,P,A) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (D,P,A)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (D,P,A)) . (IC ) is set
dom s is non empty V33() set
I is ext-real non negative V9() V10() V11() V15() V27() integer V110() set
Comput (D,P,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (D,P,I)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (D,P,I)) . (IC ) is set
J is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
s1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (D,P,s1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (D,P,s1)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (D,P,s1)) . (IC ) is set
Comput (D,P,J) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (D,P,J)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (D,P,J)) . (IC ) is set
goto (IC (Comput (D,P,J))) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) V100(3, SCM+FSA ) V102(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K495((IC (Comput (D,P,J)))) is Element of the InstructionsF of K489()
D +* ((IC (Comput (D,P,J))),(goto (IC (Comput (D,P,J))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
Comput ((D +* ((IC (Comput (D,P,J))),(goto (IC (Comput (D,P,J)))))),P,J) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
FirstNotUsed s is V94() non read-only Element of the carrier of SCM+FSA
D is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
K306(NAT,s) is non empty V33() Element of K43(NAT)
A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
I is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (A,D,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (A,D,I)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (A,D,I)) . (IC ) is set
dom s is non empty V33() set
J is ext-real non negative V9() V10() V11() V15() V27() integer V110() set
Comput (A,D,J) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (A,D,J)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (A,D,J)) . (IC ) is set
s1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (A,D,s1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
D . (intloc 0) is ext-real V27() integer V110() set
(D . (intloc 0)) + 1 is ext-real V27() integer V110() set
D +* ((FirstNotUsed s),((D . (intloc 0)) + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (A,D,s1)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (A,D,s1)) . (IC ) is set
(intloc 0) := (FirstNotUsed s) is ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) V102(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
dom (A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))) is non empty set
UsedInt*Loc s is V33() Element of K43(FinSeq-Locations)
P2 is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
P2 | (UsedInt*Loc s) is Relation-like UsedInt*Loc s -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible V33() V144() set
D | (UsedInt*Loc s) is Relation-like UsedInt*Loc s -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible V33() V144() set
dom A is non empty set
(A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))) . (IC (Comput (A,D,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P2 . (intloc 0) is ext-real V27() integer V110() set
dom D is non empty set
P2 . (FirstNotUsed s) is ext-real V27() integer V110() set
Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
dom (Start-At (0,SCM+FSA)) is non empty V33() set
m1 is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
m1 . (intloc 0) is ext-real V27() integer V110() set
s1 + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
m3 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),m1,m3) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),m1,m3)) . (intloc 0) is ext-real V27() integer V110() set
UsedIntLoc s is V33() Element of K43(Int-Locations)
m1 | (UsedIntLoc s) is Relation-like UsedIntLoc s -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible V33() V144() set
D | (UsedIntLoc s) is Relation-like UsedIntLoc s -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible V33() V144() set
l is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (A,D,l) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (A,D,l)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (A,D,l)) . (IC ) is set
l is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),m1,l) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),m1,l)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),m1,l)) . (IC ) is set
(Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1)) . (FirstNotUsed s) is ext-real V27() integer V110() set
Following ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),(Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),(Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1)) . (IC ) is set
(A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))) /. (IC (Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),(Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1)))),(Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)) is set
K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V30( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) Element of K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))))
K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) is Relation-like set
K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))))) is set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),(Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),(Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1))))) . (Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1)) is set
(A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))) . (IC (Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec (((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))) . (IC (Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1)))),(Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))) . (IC (Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))) . (IC (Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1))))) . (Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1)) is set
Exec (((intloc 0) := (FirstNotUsed s)),(Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,((intloc 0) := (FirstNotUsed s))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,((intloc 0) := (FirstNotUsed s))) . (Comput ((A +* ((IC (Comput (A,D,s1))),((intloc 0) := (FirstNotUsed s)))),P2,s1)) is set
s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() set
UsedIntLoc D is V33() Element of K43(Int-Locations)
(D,s,P) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
P +* D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
Initialized s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
Result ((P +* D),(Initialized s)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
A is V94() non read-only Element of the carrier of SCM+FSA
(D,s,P) . A is ext-real V27() integer V110() set
s . A is ext-real V27() integer V110() set
Result ((P +* D),(s +* (Initialize ((intloc 0) .--> 1)))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr ((P +* D),(Result ((P +* D),(s +* (Initialize ((intloc 0) .--> 1)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Result ((P +* D),(s +* (Initialize ((intloc 0) .--> 1))))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Result ((P +* D),(s +* (Initialize ((intloc 0) .--> 1))))) . (IC ) is set
(P +* D) /. (IC (Result ((P +* D),(s +* (Initialize ((intloc 0) .--> 1)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
I is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((P +* D),(s +* (Initialize ((intloc 0) .--> 1))),I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
dom ((intloc 0) .--> 1) is non empty V20() V33() set
dom (Start-At (0,SCM+FSA)) is non empty V33() set
(dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) is non empty V33() set
{(intloc 0)} is non empty V33() Element of K43(Int-Locations)
dom D is non empty V33() set
J is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((P +* D),(s +* (Initialize ((intloc 0) .--> 1))),J) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((P +* D),(s +* (Initialize ((intloc 0) .--> 1))),J)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* D),(s +* (Initialize ((intloc 0) .--> 1))),J)) . (IC ) is set
(s +* (Initialize ((intloc 0) .--> 1))) . A is ext-real V27() integer V110() set
s is FinSeq-Location
P is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
P . s is Relation-like NAT -defined INT -valued Function-like V33() V41() V42() V144() M7( INT )
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() set
UsedInt*Loc A is V33() Element of K43(FinSeq-Locations)
(A,P,D) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
D +* A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
Initialized P is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
P +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
Result ((D +* A),(Initialized P)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(A,P,D) . s is Relation-like NAT -defined INT -valued Function-like V33() V41() V42() V144() M7( INT )
Result ((D +* A),(P +* (Initialize ((intloc 0) .--> 1)))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr ((D +* A),(Result ((D +* A),(P +* (Initialize ((intloc 0) .--> 1)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Result ((D +* A),(P +* (Initialize ((intloc 0) .--> 1))))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Result ((D +* A),(P +* (Initialize ((intloc 0) .--> 1))))) . (IC ) is set
(D +* A) /. (IC (Result ((D +* A),(P +* (Initialize ((intloc 0) .--> 1)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
I is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((D +* A),(P +* (Initialize ((intloc 0) .--> 1))),I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
dom ((intloc 0) .--> 1) is non empty V20() V33() set
dom (Start-At (0,SCM+FSA)) is non empty V33() set
(dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) is non empty V33() set
{(intloc 0)} is non empty V33() Element of K43(Int-Locations)
dom A is non empty V33() set
J is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((D +* A),(P +* (Initialize ((intloc 0) .--> 1))),J) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((D +* A),(P +* (Initialize ((intloc 0) .--> 1))),J)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((D +* A),(P +* (Initialize ((intloc 0) .--> 1))),J)) . (IC ) is set
(P +* (Initialize ((intloc 0) .--> 1))) . s is Relation-like NAT -defined INT -valued Function-like V33() V41() V42() V144() M7( INT )
s is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
goto s is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) V100(3, SCM+FSA ) V102(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K495(s) is Element of the InstructionsF of K489()
P is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC P is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
P . (IC ) is set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
D . s is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D /. (IC P) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D . (IC P) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
A is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (D,P,A) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
A + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput (D,P,(A + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Exec ((goto s),P) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)) is set
K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V30( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) Element of K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))))
K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) is Relation-like set
K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))))) is set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(goto s)) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(goto s)) . P is set
I is FinSeq-Location
(Exec ((goto s),P)) . I is Relation-like NAT -defined INT -valued Function-like V33() V41() V42() V144() M7( INT )
P . I is Relation-like NAT -defined INT -valued Function-like V33() V41() V42() V144() M7( INT )
IC (Exec ((goto s),P)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Exec ((goto s),P)) . (IC ) is set
I is V94() Element of the carrier of SCM+FSA
(Exec ((goto s),P)) . I is ext-real V27() integer V110() set
P . I is ext-real V27() integer V110() set
Following (D,P) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (D,P) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (D,P)),P) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (D,P))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (D,P))) . P is set
A is ext-real non negative V9() V10() V11() V15() V27() integer V110() set
Comput (D,P,A) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (D,P,A)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (D,P,A)) . (IC ) is set
dom D is non empty set
CurInstr (D,(Comput (D,P,A))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D /. (IC (Comput (D,P,A))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (D,P,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
I is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (D,P,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC s is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
s . (IC ) is set
DataPart s is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
s | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
P is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
DataPart P is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
P | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() set
dom I is non empty V33() set
dom (Start-At (0,SCM+FSA)) is non empty V33() set
IC P is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
P . (IC ) is set
D . (IC P) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Start-At (0,SCM+FSA)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Start-At (0,SCM+FSA)) . (IC ) is set
D . (IC (Start-At (0,SCM+FSA))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D . 0 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
I . 0 is set
Comput (D,P,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (D,P,0)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (D,P,0)) . (IC ) is set
s1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Reloc (I,s1) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
IncAddr (I,s1) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Shift ((IncAddr (I,s1)),s1) is Relation-like Function-like set
DataPart (Comput (D,P,0)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (D,P,0)) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Comput (A,s,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
DataPart (Comput (A,s,0)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (A,s,0)) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
P1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (D,P,P1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (D,P,P1)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (D,P,P1)) . (IC ) is set
(IC (Comput (D,P,P1))) + s1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (A,s,P1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (A,s,P1)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (A,s,P1)) . (IC ) is set
CurInstr (D,(Comput (D,P,P1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D /. (IC (Comput (D,P,P1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (D,(Comput (D,P,P1)))),s1) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (A,(Comput (A,s,P1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
A /. (IC (Comput (A,s,P1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
DataPart (Comput (D,P,P1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (D,P,P1)) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart (Comput (A,s,P1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (A,s,P1)) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
P1 + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput (D,P,(P1 + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (D,P,(P1 + 1))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (D,P,(P1 + 1))) . (IC ) is set
(IC (Comput (D,P,(P1 + 1)))) + s1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (A,s,(P1 + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (A,s,(P1 + 1))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (A,s,(P1 + 1))) . (IC ) is set
CurInstr (D,(Comput (D,P,(P1 + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D /. (IC (Comput (D,P,(P1 + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (D,(Comput (D,P,(P1 + 1))))),s1) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (A,(Comput (A,s,(P1 + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
A /. (IC (Comput (A,s,(P1 + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
DataPart (Comput (D,P,(P1 + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (D,P,(P1 + 1))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart (Comput (A,s,(P1 + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (A,s,(P1 + 1))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Following (D,(Comput (D,P,P1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Exec ((CurInstr (D,(Comput (D,P,P1)))),(Comput (D,P,P1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)) is set
K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V30( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) Element of K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))))
K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) is Relation-like set
K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))))) is set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (D,(Comput (D,P,P1))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (D,(Comput (D,P,P1))))) . (Comput (D,P,P1)) is set
Following (A,(Comput (A,s,P1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Exec ((CurInstr (A,(Comput (A,s,P1)))),(Comput (A,s,P1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (A,(Comput (A,s,P1))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (A,(Comput (A,s,P1))))) . (Comput (A,s,P1)) is set
dom (Reloc (I,s1)) is V33() set
s2 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
dom D is non empty set
dom A is non empty set
P2 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D . (IC (Comput (D,P,(P1 + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
I . s2 is set
s2 + s1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Reloc (I,s1)) . (s2 + s1) is set
(Reloc (I,s1)) . (IC (Comput (A,s,(P1 + 1)))) is set
A . (IC (Comput (A,s,(P1 + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (D,P,P1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (D,P,P1)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (D,P,P1)) . (IC ) is set
(IC (Comput (D,P,P1))) + s1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (A,s,P1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (A,s,P1)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (A,s,P1)) . (IC ) is set
CurInstr (D,(Comput (D,P,P1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D /. (IC (Comput (D,P,P1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (D,(Comput (D,P,P1)))),s1) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (A,(Comput (A,s,P1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
A /. (IC (Comput (A,s,P1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
DataPart (Comput (D,P,P1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (D,P,P1)) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart (Comput (A,s,P1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (A,s,P1)) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
0 + s1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
dom (Reloc (I,s1)) is V33() set
dom A is non empty set
dom D is non empty set
CurInstr (D,(Comput (D,P,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D /. (IC (Comput (D,P,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (D,(Comput (D,P,0)))),s1) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Reloc (I,s1)) . (0 + s1) is set
IC (Comput (A,s,0)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (A,s,0)) . (IC ) is set
A . (IC (Comput (A,s,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (A,(Comput (A,s,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
A /. (IC (Comput (A,s,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(IC (Comput (D,P,0))) + s1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
D is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() set
I is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (s,D,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (s,D,I)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (s,D,I)) . (IC ) is set
dom A is non empty V33() set
Comput (P,D,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (P,D,I)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (P,D,I)) . (IC ) is set
J is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (P,D,J) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (P,D,J)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (P,D,J)) . (IC ) is set
CurInstr (P,(Comput (P,D,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P /. (IC (Comput (P,D,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P . (IC (Comput (P,D,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
A . (IC (Comput (P,D,I))) is set
s . (IC (Comput (s,D,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (s,(Comput (s,D,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s /. (IC (Comput (s,D,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
D is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
LifeSpan (s,D) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
LifeSpan (P,D) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Result (s,D) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Result (P,D) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() set
I is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (P,D,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (P,(Comput (P,D,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (P,D,I)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (P,D,I)) . (IC ) is set
P /. (IC (Comput (P,D,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (s,D,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (s,(Comput (s,D,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (s,D,I)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (s,D,I)) . (IC ) is set
s /. (IC (Comput (s,D,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (P,D,(LifeSpan (s,D))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (P,(Comput (P,D,(LifeSpan (s,D))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (P,D,(LifeSpan (s,D)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (P,D,(LifeSpan (s,D)))) . (IC ) is set
P /. (IC (Comput (P,D,(LifeSpan (s,D))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (s,D,(LifeSpan (s,D))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (s,(Comput (s,D,(LifeSpan (s,D))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (s,D,(LifeSpan (s,D)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (s,D,(LifeSpan (s,D)))) . (IC ) is set
s /. (IC (Comput (s,D,(LifeSpan (s,D))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() () set
(D,s,P) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
P +* D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
Initialized s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
Result ((P +* D),(Initialized s)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(D,s,P) . (intloc 0) is ext-real V27() integer V110() set
Result ((P +* D),(s +* (Initialize ((intloc 0) .--> 1)))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr ((P +* D),(Result ((P +* D),(s +* (Initialize ((intloc 0) .--> 1)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Result ((P +* D),(s +* (Initialize ((intloc 0) .--> 1))))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Result ((P +* D),(s +* (Initialize ((intloc 0) .--> 1))))) . (IC ) is set
(P +* D) /. (IC (Result ((P +* D),(s +* (Initialize ((intloc 0) .--> 1)))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Initialized s) . (intloc 0) is ext-real V27() integer V110() set
A is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((P +* D),(s +* (Initialize ((intloc 0) .--> 1))),A) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
the Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() set is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() set
s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed V144() set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
P ";" D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
stop P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty V20() Function-like constant V33() V51() non halt-free V60( SCM+FSA ) V61( SCM+FSA ) V103(3, SCM+FSA ) V144() set
K179((halt SCM+FSA)) is set
K169(P,(Stop SCM+FSA)) is Relation-like V13() Function-like set
CutLastLoc (stop P) is Relation-like Function-like set
Directed (CutLastLoc (stop P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
card P is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Reloc (D,(card P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
IncAddr (D,(card P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Shift ((IncAddr (D,(card P))),(card P)) is Relation-like Function-like set
(Directed (CutLastLoc (stop P))) +* (Reloc (D,(card P))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
LifeSpan (A,s) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
A +* (P ";" D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
I is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (A,s,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((A +* (P ";" D)),s,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
I + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput (A,s,(I + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((A +* (P ";" D)),s,(I + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
dom (P ";" D) is non empty V33() set
Directed P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() halt-free V61( SCM+FSA ) V144() set
Directed (P,(card P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() halt-free V144() set
goto (card P) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) V100(3, SCM+FSA ) V102(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K495((card P)) is Element of the InstructionsF of K489()
P +~ ((halt SCM+FSA),(goto (card P))) is Relation-like Function-like set
dom (Directed P) is non empty V33() set
dom (Reloc (D,(card P))) is V33() set
(dom (Directed P)) \/ (dom (Reloc (D,(card P)))) is non empty V33() set
dom P is non empty V33() set
(dom P) \/ (dom (Reloc (D,(card P)))) is non empty V33() set
Following (A,(Comput (A,s,I))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (A,(Comput (A,s,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (A,s,I)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (A,s,I)) . (IC ) is set
A /. (IC (Comput (A,s,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (A,(Comput (A,s,I)))),(Comput (A,s,I))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)) is set
K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V30( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) Element of K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))))
K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) is Relation-like set
K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))))) is set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (A,(Comput (A,s,I))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (A,(Comput (A,s,I))))) . (Comput (A,s,I)) is set
Following ((A +* (P ";" D)),(Comput ((A +* (P ";" D)),s,I))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr ((A +* (P ";" D)),(Comput ((A +* (P ";" D)),s,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((A +* (P ";" D)),s,I)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((A +* (P ";" D)),s,I)) . (IC ) is set
(A +* (P ";" D)) /. (IC (Comput ((A +* (P ";" D)),s,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr ((A +* (P ";" D)),(Comput ((A +* (P ";" D)),s,I)))),(Comput ((A +* (P ";" D)),s,I))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((A +* (P ";" D)),(Comput ((A +* (P ";" D)),s,I))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((A +* (P ";" D)),(Comput ((A +* (P ";" D)),s,I))))) . (Comput ((A +* (P ";" D)),s,I)) is set
dom A is non empty set
A . (IC (Comput (A,s,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P . (IC (Comput (A,s,I))) is set
dom (A +* (P ";" D)) is non empty set
(P ";" D) . (IC (Comput (A,s,I))) is set
(A +* (P ";" D)) . (IC (Comput (A,s,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (A,s,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((A +* (P ";" D)),s,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed V144() set
P +* D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
Directed D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() halt-free V61( SCM+FSA ) V144() set
card D is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Directed (D,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() halt-free V144() set
goto (card D) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) V100(3, SCM+FSA ) V102(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K495((card D)) is Element of the InstructionsF of K489()
D +~ ((halt SCM+FSA),(goto (card D))) is Relation-like Function-like set
LifeSpan ((P +* D),s) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(LifeSpan ((P +* D),s)) + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput (P,s,((LifeSpan ((P +* D),s)) + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (P,s,((LifeSpan ((P +* D),s)) + 1))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (P,s,((LifeSpan ((P +* D),s)) + 1))) . (IC ) is set
Comput ((P +* D),s,(LifeSpan ((P +* D),s))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((P +* D),s,(LifeSpan ((P +* D),s)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* D),s,(LifeSpan ((P +* D),s)))) . (IC ) is set
dom D is non empty V33() set
D ";" D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
stop D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty V20() Function-like constant V33() V51() non halt-free V60( SCM+FSA ) V61( SCM+FSA ) V103(3, SCM+FSA ) V144() set
K179((halt SCM+FSA)) is set
K169(D,(Stop SCM+FSA)) is Relation-like V13() Function-like set
CutLastLoc (stop D) is Relation-like Function-like set
Directed (CutLastLoc (stop D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
Reloc (D,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
IncAddr (D,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Shift ((IncAddr (D,(card D))),(card D)) is Relation-like Function-like set
(Directed (CutLastLoc (stop D))) +* (Reloc (D,(card D))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
P +* (D ";" D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
D +* (D ";" D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V144() set
P +* (D +* (D ";" D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
(P +* D) +* (D ";" D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
P1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
P +* (Directed D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
s2 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((P +* (D ";" D)),s,s2) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* (Directed D)),s,s2) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
s2 + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput ((P +* (D ";" D)),s,(s2 + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* (Directed D)),s,(s2 + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Following ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,s2))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,s2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((P +* (Directed D)),s,s2)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* (Directed D)),s,s2)) . (IC ) is set
(P +* (Directed D)) /. (IC (Comput ((P +* (Directed D)),s,s2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,s2)))),(Comput ((P +* (Directed D)),s,s2))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)) is set
K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V30( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) Element of K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))))
K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) is Relation-like set
K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))))) is set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,s2))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,s2))))) . (Comput ((P +* (Directed D)),s,s2)) is set
Following ((P +* (D ";" D)),(Comput ((P +* (D ";" D)),s,s2))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr ((P +* (D ";" D)),(Comput ((P +* (D ";" D)),s,s2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((P +* (D ";" D)),s,s2)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* (D ";" D)),s,s2)) . (IC ) is set
(P +* (D ";" D)) /. (IC (Comput ((P +* (D ";" D)),s,s2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr ((P +* (D ";" D)),(Comput ((P +* (D ";" D)),s,s2)))),(Comput ((P +* (D ";" D)),s,s2))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* (D ";" D)),(Comput ((P +* (D ";" D)),s,s2))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* (D ";" D)),(Comput ((P +* (D ";" D)),s,s2))))) . (Comput ((P +* (D ";" D)),s,s2)) is set
Comput ((P +* D),s,s2) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
dom (Directed D) is non empty V33() set
dom (P +* (Directed D)) is non empty set
(P +* (Directed D)) . (IC (Comput ((P +* (Directed D)),s,s2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (P +* (D ";" D)) is non empty set
(Directed D) . (IC (Comput ((P +* (Directed D)),s,s2))) is set
dom (D ";" D) is non empty V33() set
(P +* (D ";" D)) . (IC (Comput ((P +* (D ";" D)),s,s2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput ((P +* (D ";" D)),s,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* (Directed D)),s,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* (D ";" D)),s,P1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* (Directed D)),s,P1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* D),s,P1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* (Directed D)),s,(LifeSpan ((P +* D),s))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
dom (P +* D) is non empty set
D . (IC (Comput ((P +* D),s,(LifeSpan ((P +* D),s))))) is set
(P +* D) . (IC (Comput ((P +* D),s,(LifeSpan ((P +* D),s))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr ((P +* D),(Comput ((P +* D),s,(LifeSpan ((P +* D),s))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(P +* D) /. (IC (Comput ((P +* D),s,(LifeSpan ((P +* D),s))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((P +* (Directed D)),s,(LifeSpan ((P +* D),s)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* (Directed D)),s,(LifeSpan ((P +* D),s)))) . (IC ) is set
dom (Directed D) is non empty V33() set
(P +* (Directed D)) . (IC (Comput ((P +* D),s,(LifeSpan ((P +* D),s))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Directed D) . (IC (Comput ((P +* D),s,(LifeSpan ((P +* D),s))))) is set
dom (P +* (Directed D)) is non empty set
Comput ((P +* (Directed D)),s,((LifeSpan ((P +* D),s)) + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Following ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,(LifeSpan ((P +* D),s))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,(LifeSpan ((P +* D),s))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(P +* (Directed D)) /. (IC (Comput ((P +* (Directed D)),s,(LifeSpan ((P +* D),s))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,(LifeSpan ((P +* D),s)))))),(Comput ((P +* (Directed D)),s,(LifeSpan ((P +* D),s))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)) is set
K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V30( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) Element of K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))))
K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) is Relation-like set
K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))))) is set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,(LifeSpan ((P +* D),s))))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,(LifeSpan ((P +* D),s))))))) . (Comput ((P +* (Directed D)),s,(LifeSpan ((P +* D),s)))) is set
Exec ((goto (card D)),(Comput ((P +* (Directed D)),s,(LifeSpan ((P +* D),s))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(goto (card D))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(goto (card D))) . (Comput ((P +* (Directed D)),s,(LifeSpan ((P +* D),s)))) is set
s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed V144() set
P +* D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
Directed D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() halt-free V61( SCM+FSA ) V144() set
card D is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Directed (D,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() halt-free V144() set
goto (card D) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) V100(3, SCM+FSA ) V102(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K495((card D)) is Element of the InstructionsF of K489()
D +~ ((halt SCM+FSA),(goto (card D))) is Relation-like Function-like set
LifeSpan ((P +* D),s) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (P,s,(LifeSpan ((P +* D),s))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
DataPart (Comput (P,s,(LifeSpan ((P +* D),s)))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (P,s,(LifeSpan ((P +* D),s)))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(LifeSpan ((P +* D),s)) + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput (P,s,((LifeSpan ((P +* D),s)) + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
DataPart (Comput (P,s,((LifeSpan ((P +* D),s)) + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (P,s,((LifeSpan ((P +* D),s)) + 1))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Comput ((P +* D),s,(LifeSpan ((P +* D),s))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((P +* D),s,(LifeSpan ((P +* D),s)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* D),s,(LifeSpan ((P +* D),s)))) . (IC ) is set
dom D is non empty V33() set
J is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
D ";" D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
stop D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty V20() Function-like constant V33() V51() non halt-free V60( SCM+FSA ) V61( SCM+FSA ) V103(3, SCM+FSA ) V144() set
K179((halt SCM+FSA)) is set
K169(D,(Stop SCM+FSA)) is Relation-like V13() Function-like set
CutLastLoc (stop D) is Relation-like Function-like set
Directed (CutLastLoc (stop D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
Reloc (D,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
IncAddr (D,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Shift ((IncAddr (D,(card D))),(card D)) is Relation-like Function-like set
(Directed (CutLastLoc (stop D))) +* (Reloc (D,(card D))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
(P +* D) +* (D ";" D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
s1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (((P +* D) +* (D ";" D)),s,s1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput (P,s,s1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
s1 + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput (((P +* D) +* (D ";" D)),s,(s1 + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput (P,s,(s1 + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
dom (D ";" D) is non empty V33() set
Following (P,(Comput (P,s,s1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (P,(Comput (P,s,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (P,s,s1)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (P,s,s1)) . (IC ) is set
P /. (IC (Comput (P,s,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P,(Comput (P,s,s1)))),(Comput (P,s,s1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)) is set
K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V30( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) Element of K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))))
K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) is Relation-like set
K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))))) is set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P,(Comput (P,s,s1))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P,(Comput (P,s,s1))))) . (Comput (P,s,s1)) is set
Following (((P +* D) +* (D ";" D)),(Comput (((P +* D) +* (D ";" D)),s,s1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (((P +* D) +* (D ";" D)),(Comput (((P +* D) +* (D ";" D)),s,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (((P +* D) +* (D ";" D)),s,s1)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (((P +* D) +* (D ";" D)),s,s1)) . (IC ) is set
((P +* D) +* (D ";" D)) /. (IC (Comput (((P +* D) +* (D ";" D)),s,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (((P +* D) +* (D ";" D)),(Comput (((P +* D) +* (D ";" D)),s,s1)))),(Comput (((P +* D) +* (D ";" D)),s,s1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (((P +* D) +* (D ";" D)),(Comput (((P +* D) +* (D ";" D)),s,s1))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (((P +* D) +* (D ";" D)),(Comput (((P +* D) +* (D ";" D)),s,s1))))) . (Comput (((P +* D) +* (D ";" D)),s,s1)) is set
Comput ((P +* D),s,s1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
dom (Directed D) is non empty V33() set
dom P is non empty set
P . (IC (Comput (P,s,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Directed D) . (IC (Comput (P,s,s1))) is set
dom ((P +* D) +* (D ";" D)) is non empty set
((P +* D) +* (D ";" D)) . (IC (Comput (((P +* D) +* (D ";" D)),s,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(D ";" D) . (IC (Comput (((P +* D) +* (D ";" D)),s,s1))) is set
(Directed D) . (IC (Comput (((P +* D) +* (D ";" D)),s,s1))) is set
Comput (((P +* D) +* (D ";" D)),s,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput (P,s,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput (((P +* D) +* (D ";" D)),s,J) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput (P,s,J) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* D),s,J) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
dom (P +* D) is non empty set
D . (IC (Comput ((P +* D),s,(LifeSpan ((P +* D),s))))) is set
(P +* D) . (IC (Comput ((P +* D),s,(LifeSpan ((P +* D),s))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr ((P +* D),(Comput ((P +* D),s,(LifeSpan ((P +* D),s))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(P +* D) /. (IC (Comput ((P +* D),s,(LifeSpan ((P +* D),s))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (P,s,(LifeSpan ((P +* D),s)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (P,s,(LifeSpan ((P +* D),s)))) . (IC ) is set
dom (Directed D) is non empty V33() set
P . (IC (Comput ((P +* D),s,(LifeSpan ((P +* D),s))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Directed D) . (IC (Comput ((P +* D),s,(LifeSpan ((P +* D),s))))) is set
dom P is non empty set
Following (P,(Comput (P,s,(LifeSpan ((P +* D),s))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (P,(Comput (P,s,(LifeSpan ((P +* D),s))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P /. (IC (Comput (P,s,(LifeSpan ((P +* D),s))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P,(Comput (P,s,(LifeSpan ((P +* D),s)))))),(Comput (P,s,(LifeSpan ((P +* D),s))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)) is set
K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V30( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) Element of K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))))
K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) is Relation-like set
K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))))) is set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P,(Comput (P,s,(LifeSpan ((P +* D),s))))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P,(Comput (P,s,(LifeSpan ((P +* D),s))))))) . (Comput (P,s,(LifeSpan ((P +* D),s)))) is set
Exec ((goto (card D)),(Comput (P,s,(LifeSpan ((P +* D),s))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(goto (card D))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(goto (card D))) . (Comput (P,s,(LifeSpan ((P +* D),s)))) is set
J is V94() Element of the carrier of SCM+FSA
(Comput (P,s,((LifeSpan ((P +* D),s)) + 1))) . J is ext-real V27() integer V110() set
(Comput (P,s,(LifeSpan ((P +* D),s)))) . J is ext-real V27() integer V110() set
s1 is FinSeq-Location
(Comput (P,s,((LifeSpan ((P +* D),s)) + 1))) . s1 is Relation-like NAT -defined INT -valued Function-like V33() V41() V42() V144() M7( INT )
(Comput (P,s,(LifeSpan ((P +* D),s)))) . s1 is Relation-like NAT -defined INT -valued Function-like V33() V41() V42() V144() M7( INT )
s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
LifeSpan (P,s) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() set
Directed D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() halt-free V61( SCM+FSA ) V144() set
card D is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Directed (D,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() halt-free V144() set
goto (card D) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) V100(3, SCM+FSA ) V102(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K495((card D)) is Element of the InstructionsF of K489()
D +~ ((halt SCM+FSA),(goto (card D))) is Relation-like Function-like set
P +* (Directed D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
J is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
D ";" D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
stop D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty V20() Function-like constant V33() V51() non halt-free V60( SCM+FSA ) V61( SCM+FSA ) V103(3, SCM+FSA ) V144() set
K179((halt SCM+FSA)) is set
K169(D,(Stop SCM+FSA)) is Relation-like V13() Function-like set
CutLastLoc (stop D) is Relation-like Function-like set
Directed (CutLastLoc (stop D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
Reloc (D,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
IncAddr (D,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Shift ((IncAddr (D,(card D))),(card D)) is Relation-like Function-like set
(Directed (CutLastLoc (stop D))) +* (Reloc (D,(card D))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
P +* (D ";" D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
I is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
s1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((P +* (D ";" D)),I,s1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* (Directed D)),s,s1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
s1 + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput ((P +* (D ";" D)),I,(s1 + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* (Directed D)),s,(s1 + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
dom D is non empty V33() set
dom (D ";" D) is non empty V33() set
Following ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,s1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((P +* (Directed D)),s,s1)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* (Directed D)),s,s1)) . (IC ) is set
(P +* (Directed D)) /. (IC (Comput ((P +* (Directed D)),s,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,s1)))),(Comput ((P +* (Directed D)),s,s1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)) is set
K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V30( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) Element of K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))))
K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) is Relation-like set
K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))))) is set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,s1))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,s1))))) . (Comput ((P +* (Directed D)),s,s1)) is set
Following ((P +* (D ";" D)),(Comput ((P +* (D ";" D)),I,s1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr ((P +* (D ";" D)),(Comput ((P +* (D ";" D)),I,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((P +* (D ";" D)),I,s1)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* (D ";" D)),I,s1)) . (IC ) is set
(P +* (D ";" D)) /. (IC (Comput ((P +* (D ";" D)),I,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr ((P +* (D ";" D)),(Comput ((P +* (D ";" D)),I,s1)))),(Comput ((P +* (D ";" D)),I,s1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* (D ";" D)),(Comput ((P +* (D ";" D)),I,s1))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* (D ";" D)),(Comput ((P +* (D ";" D)),I,s1))))) . (Comput ((P +* (D ";" D)),I,s1)) is set
Comput (P,s,s1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
dom (Directed D) is non empty V33() set
dom (P +* (Directed D)) is non empty set
(P +* (Directed D)) . (IC (Comput ((P +* (Directed D)),s,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Directed D) . (IC (Comput ((P +* (Directed D)),s,s1))) is set
dom (P +* (D ";" D)) is non empty set
(P +* (D ";" D)) . (IC (Comput ((P +* (D ";" D)),I,s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(D ";" D) . (IC (Comput ((P +* (D ";" D)),I,s1))) is set
(Directed D) . (IC (Comput ((P +* (D ";" D)),I,s1))) is set
Comput ((P +* (D ";" D)),I,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* (Directed D)),s,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* (D ";" D)),I,J) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* (Directed D)),s,J) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput (P,s,J) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
J is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (P,s,J) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (P,s,J)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (P,s,J)) . (IC ) is set
dom D is non empty V33() set
dom (Directed D) is non empty V33() set
Comput (P,I,J) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (P,I,J)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (P,I,J)) . (IC ) is set
(Directed D) . (IC (Comput (P,s,J))) is set
rng (Directed D) is non empty V33() set
dom (P +* (Directed D)) is non empty set
Comput ((P +* (Directed D)),s,J) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((P +* (Directed D)),s,J)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* (Directed D)),s,J)) . (IC ) is set
CurInstr ((P +* (Directed D)),(Comput ((P +* (Directed D)),s,J))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(P +* (Directed D)) /. (IC (Comput ((P +* (Directed D)),s,J))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(P +* (Directed D)) . (IC (Comput (P,s,J))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed V144() set
P +* D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
LifeSpan ((P +* D),s) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
D ";" A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
stop D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty V20() Function-like constant V33() V51() non halt-free V60( SCM+FSA ) V61( SCM+FSA ) V103(3, SCM+FSA ) V144() set
K179((halt SCM+FSA)) is set
K169(D,(Stop SCM+FSA)) is Relation-like V13() Function-like set
CutLastLoc (stop D) is Relation-like Function-like set
Directed (CutLastLoc (stop D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
card D is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Reloc (A,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
IncAddr (A,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Shift ((IncAddr (A,(card D))),(card D)) is Relation-like Function-like set
(Directed (CutLastLoc (stop D))) +* (Reloc (A,(card D))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
P +* (D ";" A) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
dom (D ";" A) is non empty V33() set
Directed D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() halt-free V61( SCM+FSA ) V144() set
Directed (D,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() halt-free V144() set
goto (card D) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) V100(3, SCM+FSA ) V102(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K495((card D)) is Element of the InstructionsF of K489()
D +~ ((halt SCM+FSA),(goto (card D))) is Relation-like Function-like set
dom (Directed D) is non empty V33() set
dom (Reloc (A,(card D))) is V33() set
(dom (Directed D)) \/ (dom (Reloc (A,(card D)))) is non empty V33() set
dom D is non empty V33() set
(dom D) \/ (dom (Reloc (A,(card D)))) is non empty V33() set
I is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((P +* D),s,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* (D ";" A)),s,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
I + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput ((P +* D),s,(I + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* (D ";" A)),s,(I + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Following ((P +* D),(Comput ((P +* D),s,I))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr ((P +* D),(Comput ((P +* D),s,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((P +* D),s,I)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* D),s,I)) . (IC ) is set
(P +* D) /. (IC (Comput ((P +* D),s,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr ((P +* D),(Comput ((P +* D),s,I)))),(Comput ((P +* D),s,I))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)) is set
K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V30( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) Element of K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))))
K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) is Relation-like set
K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))))) is set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* D),(Comput ((P +* D),s,I))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* D),(Comput ((P +* D),s,I))))) . (Comput ((P +* D),s,I)) is set
Following ((P +* (D ";" A)),(Comput ((P +* (D ";" A)),s,I))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr ((P +* (D ";" A)),(Comput ((P +* (D ";" A)),s,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((P +* (D ";" A)),s,I)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* (D ";" A)),s,I)) . (IC ) is set
(P +* (D ";" A)) /. (IC (Comput ((P +* (D ";" A)),s,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr ((P +* (D ";" A)),(Comput ((P +* (D ";" A)),s,I)))),(Comput ((P +* (D ";" A)),s,I))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* (D ";" A)),(Comput ((P +* (D ";" A)),s,I))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((P +* (D ";" A)),(Comput ((P +* (D ";" A)),s,I))))) . (Comput ((P +* (D ";" A)),s,I)) is set
dom (P +* D) is non empty set
(P +* D) . (IC (Comput ((P +* D),s,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D . (IC (Comput ((P +* D),s,I))) is set
dom (P +* (D ";" A)) is non empty set
(D ";" A) . (IC (Comput ((P +* D),s,I))) is set
(P +* (D ";" A)) . (IC (Comput ((P +* (D ";" A)),s,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput ((P +* D),s,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((P +* (D ";" A)),s,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() () set
s +* D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
card D is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() set
D ";" A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
stop D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty V20() Function-like constant V33() V51() non halt-free V60( SCM+FSA ) V61( SCM+FSA ) V103(3, SCM+FSA ) V144() set
K179((halt SCM+FSA)) is set
K169(D,(Stop SCM+FSA)) is Relation-like V13() Function-like set
CutLastLoc (stop D) is Relation-like Function-like set
Directed (CutLastLoc (stop D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
Reloc (A,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
IncAddr (A,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Shift ((IncAddr (A,(card D))),(card D)) is Relation-like Function-like set
(Directed (CutLastLoc (stop D))) +* (Reloc (A,(card D))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
(s +* D) +* A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
I is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
LifeSpan ((s +* D),I) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(LifeSpan ((s +* D),I)) + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput (s,I,((LifeSpan ((s +* D),I)) + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (s,I,((LifeSpan ((s +* D),I)) + 1))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))) . (IC ) is set
DataPart (Comput (s,I,((LifeSpan ((s +* D),I)) + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Comput ((s +* D),I,(LifeSpan ((s +* D),I))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
DataPart ((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))) . (intloc 0) is ext-real V27() integer V110() set
LifeSpan (s,I) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Result ((s +* D),I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Result ((s +* D),I)) +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
LifeSpan (((s +* D) +* A),((Result ((s +* D),I)) +* (Initialize ((intloc 0) .--> 1)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
((LifeSpan ((s +* D),I)) + 1) + (LifeSpan (((s +* D) +* A),((Result ((s +* D),I)) +* (Initialize ((intloc 0) .--> 1))))) is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Result (s,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Result (s,I)) . (intloc 0) is ext-real V27() integer V110() set
LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Directed D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() halt-free V61( SCM+FSA ) V144() set
Directed (D,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() halt-free V144() set
goto (card D) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) V100(3, SCM+FSA ) V102(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K495((card D)) is Element of the InstructionsF of K489()
D +~ ((halt SCM+FSA),(goto (card D))) is Relation-like Function-like set
dom (Directed D) is non empty V33() set
dom D is non empty V33() set
s +* (Directed D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
s +* (D ";" A) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
DataPart (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible V33() data-only V144() set
(Initialize ((intloc 0) .--> 1)) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible V33() V144() set
dom (DataPart (Initialize ((intloc 0) .--> 1))) is V33() set
s2 is set
(DataPart (Initialize ((intloc 0) .--> 1))) . s2 is set
I . s2 is set
(Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) . s2 is set
DataPart (Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(DataPart (Comput ((s +* D),I,(LifeSpan ((s +* D),I))))) . s2 is set
(DataPart (Initialize ((intloc 0) .--> 1))) . s2 is set
DataPart (Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(DataPart (Comput ((s +* D),I,(LifeSpan ((s +* D),I))))) . s2 is set
DataPart (Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart (Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
((LifeSpan ((s +* D),I)) + 1) + (LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))))) is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
(dom (Initialize ((intloc 0) .--> 1))) /\ (NonZero SCM+FSA) is V33() Element of K43( the carrier of SCM+FSA)
the carrier of SCM+FSA /\ (NonZero SCM+FSA) is Element of K43( the carrier of SCM+FSA)
dom (Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) is non empty set
(dom (Comput ((s +* D),I,(LifeSpan ((s +* D),I))))) /\ (NonZero SCM+FSA) is Element of K43( the carrier of SCM+FSA)
dom (DataPart (Comput ((s +* D),I,(LifeSpan ((s +* D),I))))) is set
(DataPart (Comput ((s +* D),I,(LifeSpan ((s +* D),I))))) +* (DataPart (Initialize ((intloc 0) .--> 1))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
I +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
Comput (s,I,(LifeSpan ((s +* D),I))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
DataPart (Comput (s,I,(LifeSpan ((s +* D),I)))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (s,I,(LifeSpan ((s +* D),I)))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(DataPart ((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1)))) . (intloc 0) is set
((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))) . (intloc 0) is ext-real V27() integer V110() set
Comput (s,I,(((LifeSpan ((s +* D),I)) + 1) + (LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput (s,(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1)))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1)))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (((s +* D) +* A),(Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1)))))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))))))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))))))) . (IC ) is set
((s +* D) +* A) /. (IC (Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1)))))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (((s +* D) +* A),(Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))))))))),(card D)) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (s,(Comput (s,(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1)))))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (s,(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))))))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (s,(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))))))) . (IC ) is set
s /. (IC (Comput (s,(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1)))))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P2 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (s,I,P2) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (s,(Comput (s,I,P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (s,I,P2)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (s,I,P2)) . (IC ) is set
s /. (IC (Comput (s,I,P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((halt SCM+FSA),(card D)) is ins-loc-free V90(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s3 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
((LifeSpan ((s +* D),I)) + 1) + s3 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput (s,I,(((LifeSpan ((s +* D),I)) + 1) + s3)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (s,(Comput (s,I,(((LifeSpan ((s +* D),I)) + 1) + s3)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (s,I,(((LifeSpan ((s +* D),I)) + 1) + s3))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (s,I,(((LifeSpan ((s +* D),I)) + 1) + s3))) . (IC ) is set
s /. (IC (Comput (s,I,(((LifeSpan ((s +* D),I)) + 1) + s3)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
InsCode (halt SCM+FSA) is ext-real non negative V9() V10() V11() V15() V27() integer V99(3, SCM+FSA ) V110() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K34( the InstructionsF of SCM+FSA) is set
Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),s3) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (((s +* D) +* A),(Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),s3))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),s3)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),s3)) . (IC ) is set
((s +* D) +* A) /. (IC (Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),s3))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (((s +* D) +* A),(Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),s3)))),(card D)) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (s,(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))),s3) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (s,(Comput (s,(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))),s3))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (s,(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))),s3)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (s,(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))),s3)) . (IC ) is set
s /. (IC (Comput (s,(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))),s3))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
InsCode (CurInstr (((s +* D) +* A),(Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),s3)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of InsCodes the InstructionsF of SCM+FSA
s3 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(s +* D) +* (Directed D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
Comput (s,I,s3) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (s,(Comput (s,I,s3))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (s,I,s3)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (s,I,s3)) . (IC ) is set
s /. (IC (Comput (s,I,s3))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
P3 is ext-real non negative V9() V10() V11() V15() V27() integer V110() set
((LifeSpan ((s +* D),I)) + 1) + P3 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput (s,I,s3) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (s,(Comput (s,I,s3))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (s,I,s3)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (s,I,s3)) . (IC ) is set
s /. (IC (Comput (s,I,s3))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s3 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (s,I,s3) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (s,(Comput (s,I,s3))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (s,I,s3)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (s,I,s3)) . (IC ) is set
s /. (IC (Comput (s,I,s3))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
DataPart (Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))))))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))))))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart (Comput (s,(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))))))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (s,(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))))))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(Comput (s,I,P2)) . (intloc 0) is ext-real V27() integer V110() set
(Comput (s,(Comput (s,I,((LifeSpan ((s +* D),I)) + 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))))))) . (intloc 0) is ext-real V27() integer V110() set
(Comput (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((s +* D) +* A),((Comput ((s +* D),I,(LifeSpan ((s +* D),I)))) +* (Initialize ((intloc 0) .--> 1))))))) . (intloc 0) is ext-real V27() integer V110() set
s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() set
s ";" P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
stop s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Stop SCM+FSA is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty V20() Function-like constant V33() V51() non halt-free V60( SCM+FSA ) V61( SCM+FSA ) V103(3, SCM+FSA ) V144() set
K179((halt SCM+FSA)) is set
K169(s,(Stop SCM+FSA)) is Relation-like V13() Function-like set
CutLastLoc (stop s) is Relation-like Function-like set
Directed (CutLastLoc (stop s)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
card s is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Reloc (P,(card s)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
IncAddr (P,(card s)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Shift ((IncAddr (P,(card s))),(card s)) is Relation-like Function-like set
(Directed (CutLastLoc (stop s))) +* (Reloc (P,(card s))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
A is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
I +* s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
LifeSpan ((I +* s),A) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((I +* s),A,(LifeSpan ((I +* s),A))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A)))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(Comput ((I +* s),A,(LifeSpan ((I +* s),A)))) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
(I +* s) +* P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
LifeSpan (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A)))))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
DataPart (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible V33() data-only V144() set
(Start-At (0,SCM+FSA)) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible V33() V144() set
s3 is set
dom (DataPart (Start-At (0,SCM+FSA))) is V33() set
dom (Start-At (0,SCM+FSA)) is non empty V33() set
(dom (Start-At (0,SCM+FSA))) /\ (NonZero SCM+FSA) is V33() Element of K43( the carrier of SCM+FSA)
P2 is Relation-like Function-like set
P2 . s3 is set
DataPart (Comput ((I +* s),A,(LifeSpan ((I +* s),A)))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput ((I +* s),A,(LifeSpan ((I +* s),A)))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(DataPart (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))) . s3 is set
dom (Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))) is non empty set
the carrier of SCM+FSA /\ (NonZero SCM+FSA) is Element of K43( the carrier of SCM+FSA)
dom (Comput ((I +* s),A,(LifeSpan ((I +* s),A)))) is non empty set
(dom (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))) /\ (NonZero SCM+FSA) is Element of K43( the carrier of SCM+FSA)
dom (DataPart (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))) is set
(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(DataPart (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))) +* P2 is Relation-like Function-like set
DataPart (Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(LifeSpan ((I +* s),A)) + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
((LifeSpan ((I +* s),A)) + 1) + (LifeSpan (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))))) is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
s3 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (I,A,s3) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (I,A,s3)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (I,A,s3)) . (IC ) is set
dom I is non empty set
CurInstr (I,(Comput (I,A,s3))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
I /. (IC (Comput (I,A,s3))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (I,A,((LifeSpan ((I +* s),A)) + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Directed s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() halt-free V61( SCM+FSA ) V144() set
Directed (s,(card s)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() halt-free V144() set
goto (card s) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) V100(3, SCM+FSA ) V102(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K495((card s)) is Element of the InstructionsF of K489()
s +~ ((halt SCM+FSA),(goto (card s))) is Relation-like Function-like set
IC (Comput (I,A,((LifeSpan ((I +* s),A)) + 1))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (I,A,((LifeSpan ((I +* s),A)) + 1))) . (IC ) is set
I +* (s ";" P) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
Comput (I,A,(LifeSpan ((I +* s),A))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
DataPart (Comput (I,A,(LifeSpan ((I +* s),A)))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (I,A,(LifeSpan ((I +* s),A)))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Comput (I,A,(((LifeSpan ((I +* s),A)) + 1) + (LifeSpan (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput (I,(Comput (I,A,((LifeSpan ((I +* s),A)) + 1))),(LifeSpan (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A)))))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
DataPart (Comput (I,A,((LifeSpan ((I +* s),A)) + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (I,A,((LifeSpan ((I +* s),A)) + 1))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Comput (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))),(LifeSpan (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A)))))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (((I +* s) +* P),(Comput (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))),(LifeSpan (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A)))))))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))),(LifeSpan (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))))))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))),(LifeSpan (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))))))) . (IC ) is set
((I +* s) +* P) /. (IC (Comput (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))),(LifeSpan (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A)))))))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (((I +* s) +* P),(Comput (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))),(LifeSpan (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))))))))),(card s)) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (I,(Comput (I,(Comput (I,A,((LifeSpan ((I +* s),A)) + 1))),(LifeSpan (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A)))))))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (I,(Comput (I,A,((LifeSpan ((I +* s),A)) + 1))),(LifeSpan (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))))))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (I,(Comput (I,A,((LifeSpan ((I +* s),A)) + 1))),(LifeSpan (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A))))))))) . (IC ) is set
I /. (IC (Comput (I,(Comput (I,A,((LifeSpan ((I +* s),A)) + 1))),(LifeSpan (((I +* s) +* P),(Initialize (Comput ((I +* s),A,(LifeSpan ((I +* s),A)))))))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((halt SCM+FSA),(card s)) is ins-loc-free V90(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
P is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed V144() () set
s +* D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
D ";" A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
stop D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
K169(D,(Stop SCM+FSA)) is Relation-like V13() Function-like set
CutLastLoc (stop D) is Relation-like Function-like set
Directed (CutLastLoc (stop D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
card D is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Reloc (A,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
IncAddr (A,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Shift ((IncAddr (A,(card D))),(card D)) is Relation-like Function-like set
(Directed (CutLastLoc (stop D))) +* (Reloc (A,(card D))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
s +* (D ";" A) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
dom (D ";" A) is non empty V33() set
Directed D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() halt-free V61( SCM+FSA ) V144() set
Directed (D,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() halt-free V144() set
goto (card D) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) V100(3, SCM+FSA ) V102(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K495((card D)) is Element of the InstructionsF of K489()
D +~ ((halt SCM+FSA),(goto (card D))) is Relation-like Function-like set
dom (Directed D) is non empty V33() set
dom (Reloc (A,(card D))) is V33() set
(dom (Directed D)) \/ (dom (Reloc (A,(card D)))) is non empty V33() set
dom D is non empty V33() set
(dom D) \/ (dom (Reloc (A,(card D)))) is non empty V33() set
I is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((s +* D),P,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((s +* (D ";" A)),P,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
I + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput ((s +* D),P,(I + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((s +* (D ";" A)),P,(I + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Following ((s +* D),(Comput ((s +* D),P,I))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr ((s +* D),(Comput ((s +* D),P,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((s +* D),P,I)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((s +* D),P,I)) . (IC ) is set
(s +* D) /. (IC (Comput ((s +* D),P,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr ((s +* D),(Comput ((s +* D),P,I)))),(Comput ((s +* D),P,I))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)) is set
K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V30( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) Element of K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))))
K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) is Relation-like set
K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))))) is set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((s +* D),(Comput ((s +* D),P,I))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((s +* D),(Comput ((s +* D),P,I))))) . (Comput ((s +* D),P,I)) is set
Following ((s +* (D ";" A)),(Comput ((s +* (D ";" A)),P,I))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr ((s +* (D ";" A)),(Comput ((s +* (D ";" A)),P,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((s +* (D ";" A)),P,I)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((s +* (D ";" A)),P,I)) . (IC ) is set
(s +* (D ";" A)) /. (IC (Comput ((s +* (D ";" A)),P,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr ((s +* (D ";" A)),(Comput ((s +* (D ";" A)),P,I)))),(Comput ((s +* (D ";" A)),P,I))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((s +* (D ";" A)),(Comput ((s +* (D ";" A)),P,I))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((s +* (D ";" A)),(Comput ((s +* (D ";" A)),P,I))))) . (Comput ((s +* (D ";" A)),P,I)) is set
dom (s +* D) is non empty set
(s +* D) . (IC (Comput ((s +* D),P,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (s +* (D ";" A)) is non empty set
(s +* (D ";" A)) . (IC (Comput ((s +* (D ";" A)),P,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D . (IC (Comput ((s +* D),P,I))) is set
(D ";" A) . (IC (Comput ((s +* D),P,I))) is set
Comput ((s +* D),P,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Comput ((s +* (D ";" A)),P,0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
P is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed V144() () set
s +* D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
Result ((s +* D),P) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Initialize (Result ((s +* D),P)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(Result ((s +* D),P)) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
card D is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
LifeSpan ((s +* D),P) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(LifeSpan ((s +* D),P)) + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed V144() set
D ";" A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
stop D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
K169(D,(Stop SCM+FSA)) is Relation-like V13() Function-like set
CutLastLoc (stop D) is Relation-like Function-like set
Directed (CutLastLoc (stop D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
Reloc (A,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
IncAddr (A,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Shift ((IncAddr (A,(card D))),(card D)) is Relation-like Function-like set
(Directed (CutLastLoc (stop D))) +* (Reloc (A,(card D))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
(s +* D) +* A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
s +* (D ";" A) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
P1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IncIC ((Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1)),(card D)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1)) . (IC ) is set
(IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) + (card D) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Start-At (((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) + (card D)),SCM+FSA) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible V33() (IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) + (card D) -started V144() set
(IC ) .--> ((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) + (card D)) is Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued non empty V20() Function-like one-to-one constant V33() V144() set
{(IC )} --> ((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) + (card D)) is Relation-like {(IC )} -defined NAT -valued non empty Function-like constant total V30({(IC )},{((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) + (card D))}) V33() V144() Element of K43(K44({(IC )},{((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) + (card D))}))
{((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) + (card D))} is non empty V33() set
K44({(IC )},{((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) + (card D))}) is Relation-like V33() set
K43(K44({(IC )},{((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) + (card D))})) is V33() V37() set
(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1)) +* (Start-At (((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) + (card D)),SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total (IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) + (card D) -started set
((LifeSpan ((s +* D),P)) + 1) + P1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + P1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
P1 + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IncIC ((Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1))),(card D)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1))) . (IC ) is set
(IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1)))) + (card D) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Start-At (((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1)))) + (card D)),SCM+FSA) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible V33() (IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1)))) + (card D) -started V144() set
(IC ) .--> ((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1)))) + (card D)) is Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued non empty V20() Function-like one-to-one constant V33() V144() set
{(IC )} --> ((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1)))) + (card D)) is Relation-like {(IC )} -defined NAT -valued non empty Function-like constant total V30({(IC )},{((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1)))) + (card D))}) V33() V144() Element of K43(K44({(IC )},{((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1)))) + (card D))}))
{((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1)))) + (card D))} is non empty V33() set
K44({(IC )},{((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1)))) + (card D))}) is Relation-like V33() set
K43(K44({(IC )},{((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1)))) + (card D))})) is V33() V37() set
(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1))) +* (Start-At (((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1)))) + (card D)),SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total (IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1)))) + (card D) -started set
((LifeSpan ((s +* D),P)) + 1) + (P1 + 1) is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + (P1 + 1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
CurInstr (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
((s +* D) +* A) /. (IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1)))),(card D)) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr ((s +* (D ";" A)),(Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + P1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + P1))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + P1))) . (IC ) is set
(s +* (D ";" A)) /. (IC (Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + P1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (s +* (D ";" A)) is non empty set
IC (IncIC ((Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1)),(card D))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(IncIC ((Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1)),(card D))) . (IC ) is set
(s +* (D ";" A)) . (IC (IncIC ((Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1)),(card D)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(s +* (D ";" A)) . ((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) + (card D)) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom A is non empty V33() set
dom (IncAddr (A,(card D))) is non empty V33() set
(Shift ((IncAddr (A,(card D))),(card D))) . ((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) + (card D)) is set
x is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(IncAddr (A,(card D))) . x is set
A /. x is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((A /. x),(card D)) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom (Shift ((IncAddr (A,(card D))),(card D))) is set
{ (b1 + (card D)) where b1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT : b1 in dom (IncAddr (A,(card D))) } is set
x + (card D) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
A . x is set
((s +* D) +* A) . (IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((((s +* D) +* A) . (IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1)))),(card D)) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Reloc (A,(card D))) . ((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) + (card D)) is set
Exec ((CurInstr ((s +* (D ";" A)),(Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + P1))))),(Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + P1)))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)) is set
K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V30( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) Element of K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))))
K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))) is Relation-like set
K43(K44( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))))) is set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((s +* (D ";" A)),(Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + P1)))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((s +* (D ";" A)),(Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + P1)))))) . (Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + P1))) is set
Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Exec ((CurInstr (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1)))),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))))) is Element of K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)))
K99( the InstructionsF of SCM+FSA,K97(K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA)),K221(( the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))))) . (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1)) is set
IncIC ((Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1)))),(card D)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1)))) . (IC ) is set
(IC (Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))))) + (card D) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Start-At (((IC (Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))))) + (card D)),SCM+FSA) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible V33() (IC (Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))))) + (card D) -started V144() set
(IC ) .--> ((IC (Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))))) + (card D)) is Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued non empty V20() Function-like one-to-one constant V33() V144() set
{(IC )} --> ((IC (Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))))) + (card D)) is Relation-like {(IC )} -defined NAT -valued non empty Function-like constant total V30({(IC )},{((IC (Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))))) + (card D))}) V33() V144() Element of K43(K44({(IC )},{((IC (Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))))) + (card D))}))
{((IC (Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))))) + (card D))} is non empty V33() set
K44({(IC )},{((IC (Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))))) + (card D))}) is Relation-like V33() set
K43(K44({(IC )},{((IC (Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))))) + (card D))})) is V33() V37() set
(Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1)))) +* (Start-At (((IC (Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))))) + (card D)),SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total (IC (Following (((s +* D) +* A),(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),P1))))) + (card D) -started set
(((LifeSpan ((s +* D),P)) + 1) + P1) + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput ((s +* (D ";" A)),P,((((LifeSpan ((s +* D),P)) + 1) + P1) + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Following ((s +* (D ";" A)),(Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + P1)))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
x is V94() Element of the carrier of SCM+FSA
(IncIC ((Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1))),(card D))) . x is ext-real V27() integer V110() set
(Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + (P1 + 1)))) . x is ext-real V27() integer V110() set
x is FinSeq-Location
(IncIC ((Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1))),(card D))) . x is Relation-like NAT -defined INT -valued Function-like V33() V41() V42() V144() M7( INT )
(Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + (P1 + 1)))) . x is Relation-like NAT -defined INT -valued Function-like V33() V41() V42() V144() M7( INT )
IC (IncIC ((Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1))),(card D))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(IncIC ((Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(P1 + 1))),(card D))) . (IC ) is set
IC (Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + (P1 + 1)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + (P1 + 1)))) . (IC ) is set
Directed D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() halt-free V61( SCM+FSA ) V144() set
Directed (D,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() halt-free V144() set
goto (card D) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) V100(3, SCM+FSA ) V102(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K495((card D)) is Element of the InstructionsF of K489()
D +~ ((halt SCM+FSA),(goto (card D))) is Relation-like Function-like set
((LifeSpan ((s +* D),P)) + 1) + 0 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + 0)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IncIC (((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(card D)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC ((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))) . (IC ) is set
(IC ((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA)))) + (card D) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Start-At (((IC ((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA)))) + (card D)),SCM+FSA) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible V33() (IC ((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA)))) + (card D) -started V144() set
(IC ) .--> ((IC ((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA)))) + (card D)) is Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued non empty V20() Function-like one-to-one constant V33() V144() set
{(IC )} --> ((IC ((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA)))) + (card D)) is Relation-like {(IC )} -defined NAT -valued non empty Function-like constant total V30({(IC )},{((IC ((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA)))) + (card D))}) V33() V144() Element of K43(K44({(IC )},{((IC ((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA)))) + (card D))}))
{((IC ((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA)))) + (card D))} is non empty V33() set
K44({(IC )},{((IC ((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA)))) + (card D))}) is Relation-like V33() set
K43(K44({(IC )},{((IC ((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA)))) + (card D))})) is V33() V37() set
((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))) +* (Start-At (((IC ((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA)))) + (card D)),SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total (IC ((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA)))) + (card D) -started set
IC (IncIC (((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(card D))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(IncIC (((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(card D))) . (IC ) is set
0 + (card D) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
IC (Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + 0))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + 0))) . (IC ) is set
Comput (s,P,(LifeSpan ((s +* D),P))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
DataPart (Comput (s,P,(LifeSpan ((s +* D),P)))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (s,P,(LifeSpan ((s +* D),P)))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Comput (s,P,((LifeSpan ((s +* D),P)) + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
DataPart (Comput (s,P,((LifeSpan ((s +* D),P)) + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (s,P,((LifeSpan ((s +* D),P)) + 1))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
s3 is V94() Element of the carrier of SCM+FSA
dom (Start-At (0,SCM+FSA)) is non empty V33() set
dom (Start-At (((IC ((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA)))) + (card D)),SCM+FSA)) is non empty V33() set
(IncIC (((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(card D))) . s3 is ext-real V27() integer V110() set
((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))) . s3 is ext-real V27() integer V110() set
(Result ((s +* D),P)) . s3 is ext-real V27() integer V110() set
Comput ((s +* D),P,(LifeSpan ((s +* D),P))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Comput ((s +* D),P,(LifeSpan ((s +* D),P)))) . s3 is ext-real V27() integer V110() set
Comput ((s +* (D ";" A)),P,(LifeSpan ((s +* D),P))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Comput ((s +* (D ";" A)),P,(LifeSpan ((s +* D),P)))) . s3 is ext-real V27() integer V110() set
(Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + 0))) . s3 is ext-real V27() integer V110() set
s3 is FinSeq-Location
(IncIC (((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),(card D))) . s3 is Relation-like NAT -defined INT -valued Function-like V33() V41() V42() V144() M7( INT )
((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))) . s3 is Relation-like NAT -defined INT -valued Function-like V33() V41() V42() V144() M7( INT )
(Result ((s +* D),P)) . s3 is Relation-like NAT -defined INT -valued Function-like V33() V41() V42() V144() M7( INT )
(Comput ((s +* D),P,(LifeSpan ((s +* D),P)))) . s3 is Relation-like NAT -defined INT -valued Function-like V33() V41() V42() V144() M7( INT )
(Comput ((s +* (D ";" A)),P,(LifeSpan ((s +* D),P)))) . s3 is Relation-like NAT -defined INT -valued Function-like V33() V41() V42() V144() M7( INT )
(Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + 0))) . s3 is Relation-like NAT -defined INT -valued Function-like V33() V41() V42() V144() M7( INT )
Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IncIC ((Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0)),(card D)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0)) . (IC ) is set
(IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0))) + (card D) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Start-At (((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0))) + (card D)),SCM+FSA) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible V33() (IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0))) + (card D) -started V144() set
(IC ) .--> ((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0))) + (card D)) is Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued non empty V20() Function-like one-to-one constant V33() V144() set
{(IC )} --> ((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0))) + (card D)) is Relation-like {(IC )} -defined NAT -valued non empty Function-like constant total V30({(IC )},{((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0))) + (card D))}) V33() V144() Element of K43(K44({(IC )},{((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0))) + (card D))}))
{((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0))) + (card D))} is non empty V33() set
K44({(IC )},{((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0))) + (card D))}) is Relation-like V33() set
K43(K44({(IC )},{((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0))) + (card D))})) is V33() V37() set
(Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0)) +* (Start-At (((IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0))) + (card D)),SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total (IC (Comput (((s +* D) +* A),((Result ((s +* D),P)) +* (Start-At (0,SCM+FSA))),0))) + (card D) -started set
P1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IncIC ((Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1)),(card D)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1)) . (IC ) is set
(IC (Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1))) + (card D) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Start-At (((IC (Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1))) + (card D)),SCM+FSA) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible V33() (IC (Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1))) + (card D) -started V144() set
(IC ) .--> ((IC (Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1))) + (card D)) is Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued non empty V20() Function-like one-to-one constant V33() V144() set
{(IC )} --> ((IC (Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1))) + (card D)) is Relation-like {(IC )} -defined NAT -valued non empty Function-like constant total V30({(IC )},{((IC (Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1))) + (card D))}) V33() V144() Element of K43(K44({(IC )},{((IC (Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1))) + (card D))}))
{((IC (Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1))) + (card D))} is non empty V33() set
K44({(IC )},{((IC (Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1))) + (card D))}) is Relation-like V33() set
K43(K44({(IC )},{((IC (Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1))) + (card D))})) is V33() V37() set
(Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1)) +* (Start-At (((IC (Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1))) + (card D)),SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total (IC (Comput (((s +* D) +* A),(Initialize (Result ((s +* D),P))),P1))) + (card D) -started set
((LifeSpan ((s +* D),P)) + 1) + P1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput ((s +* (D ";" A)),P,(((LifeSpan ((s +* D),P)) + 1) + P1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed V144() () set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed V144() () set
s ";" P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
stop s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
K169(s,(Stop SCM+FSA)) is Relation-like V13() Function-like set
CutLastLoc (stop s) is Relation-like Function-like set
Directed (CutLastLoc (stop s)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
card s is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Reloc (P,(card s)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
IncAddr (P,(card s)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Shift ((IncAddr (P,(card s))),(card s)) is Relation-like Function-like set
(Directed (CutLastLoc (stop s))) +* (Reloc (P,(card s))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
D is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
D . (intloc 0) is ext-real V27() integer V110() set
A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
A +* s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
A +* (s ";" P) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
I is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (A,D,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Comput (A,D,I)) . (intloc 0) is ext-real V27() integer V110() set
LifeSpan ((A +* s),D) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((A +* s),D,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Comput ((A +* s),D,I)) . (intloc 0) is ext-real V27() integer V110() set
LifeSpan ((A +* s),D) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
s1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(LifeSpan ((A +* s),D)) + s1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
P1 is ext-real non negative V9() V10() V11() V15() V27() integer V110() set
1 + P1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
dom (Start-At (0,SCM+FSA)) is non empty V33() set
(A +* s) +* P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
Result ((A +* s),D) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Initialize (Result ((A +* s),D)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(Result ((A +* s),D)) +* (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
s2 is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2)) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2)) . (IC ) is set
(IC (Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2))) + (card s) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Start-At (((IC (Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2))) + (card s)),SCM+FSA) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible V33() (IC (Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2))) + (card s) -started V144() set
(IC ) .--> ((IC (Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2))) + (card s)) is Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued non empty V20() Function-like one-to-one constant V33() V144() set
{(IC )} --> ((IC (Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2))) + (card s)) is Relation-like {(IC )} -defined NAT -valued non empty Function-like constant total V30({(IC )},{((IC (Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2))) + (card s))}) V33() V144() Element of K43(K44({(IC )},{((IC (Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2))) + (card s))}))
{((IC (Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2))) + (card s))} is non empty V33() set
K44({(IC )},{((IC (Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2))) + (card s))}) is Relation-like V33() set
K43(K44({(IC )},{((IC (Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2))) + (card s))})) is V33() V37() set
dom (Start-At (((IC (Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2))) + (card s)),SCM+FSA)) is non empty V33() set
IncIC ((Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2)),(card s)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2)) +* (Start-At (((IC (Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2))) + (card s)),SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total (IC (Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2))) + (card s) -started set
(LifeSpan ((A +* s),D)) + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
((LifeSpan ((A +* s),D)) + 1) + s2 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput ((A +* (s ";" P)),D,(((LifeSpan ((A +* s),D)) + 1) + s2)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Comput (((A +* s) +* P),(Initialize (Result ((A +* s),D))),s2)) . (intloc 0) is ext-real V27() integer V110() set
(Initialize (Result ((A +* s),D))) . (intloc 0) is ext-real V27() integer V110() set
(Result ((A +* s),D)) . (intloc 0) is ext-real V27() integer V110() set
Comput ((A +* s),D,(LifeSpan ((A +* s),D))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Comput ((A +* s),D,(LifeSpan ((A +* s),D)))) . (intloc 0) is ext-real V27() integer V110() set
LifeSpan ((A +* s),D) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
I is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput (A,D,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Comput (A,D,I)) . (intloc 0) is ext-real V27() integer V110() set
Comput ((A +* s),D,I) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Comput ((A +* s),D,I)) . (intloc 0) is ext-real V27() integer V110() set
s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() () set
P +* D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
LifeSpan ((P +* D),(s +* (Initialize ((intloc 0) .--> 1)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(LifeSpan ((P +* D),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Result ((P +* D),(s +* (Initialize ((intloc 0) .--> 1)))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Result ((P +* D),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() set
D ";" A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() set
stop D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
K169(D,(Stop SCM+FSA)) is Relation-like V13() Function-like set
CutLastLoc (stop D) is Relation-like Function-like set
Directed (CutLastLoc (stop D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
card D is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Reloc (A,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
IncAddr (A,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Shift ((IncAddr (A,(card D))),(card D)) is Relation-like Function-like set
(Directed (CutLastLoc (stop D))) +* (Reloc (A,(card D))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
P +* (D ";" A) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
LifeSpan ((P +* (D ";" A)),(s +* (Initialize ((intloc 0) .--> 1)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(P +* D) +* A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
LifeSpan (((P +* D) +* A),((Result ((P +* D),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
((LifeSpan ((P +* D),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* D) +* A),((Result ((P +* D),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))))) is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
(P +* (D ";" A)) +* D is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
LifeSpan (((P +* (D ";" A)) +* D),(s +* (Initialize ((intloc 0) .--> 1)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(LifeSpan (((P +* (D ";" A)) +* D),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
((P +* (D ";" A)) +* D) +* A is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
Result (((P +* (D ";" A)) +* D),(s +* (Initialize ((intloc 0) .--> 1)))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Result (((P +* (D ";" A)) +* D),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
LifeSpan ((((P +* (D ";" A)) +* D) +* A),((Result (((P +* (D ";" A)) +* D),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
((LifeSpan (((P +* (D ";" A)) +* D),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan ((((P +* (D ";" A)) +* D) +* A),((Result (((P +* (D ";" A)) +* D),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))))) is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() () set
(I,s,P) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
P +* I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
Initialized s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
Result ((P +* I),(Initialized s)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
card I is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
J is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() set
I ";" J is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() paraclosed parahalting V144() set
stop I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
K169(I,(Stop SCM+FSA)) is Relation-like V13() Function-like set
CutLastLoc (stop I) is Relation-like Function-like set
Directed (CutLastLoc (stop I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
Reloc (J,(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
IncAddr (J,(card I)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V51() V144() set
Shift ((IncAddr (J,(card I))),(card I)) is Relation-like Function-like set
(Directed (CutLastLoc (stop I))) +* (Reloc (J,(card I))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V33() V144() set
((I ";" J),s,P) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
P +* (I ";" J) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
Result ((P +* (I ";" J)),(Initialized s)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(J,(I,s,P),P) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
P +* J is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
Initialized (I,s,P) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total 0 -started set
(I,s,P) +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
Result ((P +* J),(Initialized (I,s,P))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IncIC ((J,(I,s,P),P),(card I)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (J,(I,s,P),P) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(J,(I,s,P),P) . (IC ) is set
(IC (J,(I,s,P),P)) + (card I) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Start-At (((IC (J,(I,s,P),P)) + (card I)),SCM+FSA) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible V33() (IC (J,(I,s,P),P)) + (card I) -started V144() set
(IC ) .--> ((IC (J,(I,s,P),P)) + (card I)) is Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued non empty V20() Function-like one-to-one constant V33() V144() set
{(IC )} --> ((IC (J,(I,s,P),P)) + (card I)) is Relation-like {(IC )} -defined NAT -valued non empty Function-like constant total V30({(IC )},{((IC (J,(I,s,P),P)) + (card I))}) V33() V144() Element of K43(K44({(IC )},{((IC (J,(I,s,P),P)) + (card I))}))
{((IC (J,(I,s,P),P)) + (card I))} is non empty V33() set
K44({(IC )},{((IC (J,(I,s,P),P)) + (card I))}) is Relation-like V33() set
K43(K44({(IC )},{((IC (J,(I,s,P),P)) + (card I))})) is V33() V37() set
(J,(I,s,P),P) +* (Start-At (((IC (J,(I,s,P),P)) + (card I)),SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total (IC (J,(I,s,P),P)) + (card I) -started set
LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
(P +* I) +* J is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(P +* (I ";" J)) +* I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
LifeSpan (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
(Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
((P +* (I ";" J)) +* I) +* (I ";" J) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
I +* (I ";" J) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V144() set
(P +* (I ";" J)) +* (I +* (I ";" J)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
(I ";" J) +* (I +* (I ";" J)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V144() set
P +* ((I ";" J) +* (I +* (I ";" J))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
(I ";" J) +* (I ";" J) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like V33() V144() set
P +* ((I ";" J) +* (I ";" J)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
(P +* I) +* (I ";" J) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
P +* (I +* (I ";" J)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
Comput (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
DataPart (Comput (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Comput ((P +* ((I ";" J) +* (I ";" J))),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
DataPart (Comput ((P +* ((I ";" J) +* (I ";" J))),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput ((P +* ((I ";" J) +* (I ";" J))),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(Comput (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible the_Values_of SCM+FSA -compatible total 0 -started set
DataPart ((Comput (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
((Comput (((P +* (I ";" J)) +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart (Initialize ((intloc 0) .--> 1)) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible V33() data-only V144() set
(Initialize ((intloc 0) .--> 1)) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible V33() V144() set
(DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))))))) +* (DataPart (Initialize ((intloc 0) .--> 1))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart ((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) . (IC ) is set
DataPart (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Comput ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
DataPart (Comput ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
DataPart (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
IC (Comput ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* (I ";" J)),(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) . (IC ) is set
IC (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) . (IC ) is set
(IC (Comput (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))),(LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))) + (card I) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Result ((P +* J),((I,s,P) +* (Initialize ((intloc 0) .--> 1)))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
Result (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1)))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))) is ext-real positive non negative V9() V10() V11() V15() non empty V27() integer V44() V110() Element of NAT
Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
DataPart ((I ";" J),s,P) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
((I ";" J),s,P) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
DataPart (J,(I,s,P),P) is Relation-like the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible data-only set
(J,(I,s,P),P) | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible set
IC ((I ";" J),s,P) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
((I ";" J),s,P) . (IC ) is set
IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))))))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))))))) . (IC ) is set
IC (Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Comput ((P +* (I ";" J)),(s +* (Initialize ((intloc 0) .--> 1))),(((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))))) . (IC ) is set
IC (Result (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Result (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1))))) . (IC ) is set
(IC (Result (((P +* I) +* J),((Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) +* (Initialize ((intloc 0) .--> 1)))))) + (card I) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Result (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC (Result (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))))) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
(Result (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1))))) . (IC ) is set
(IC (Result (((P +* I) +* J),((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))) + (card I) is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
l is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
Start-At (l,SCM+FSA) is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible V33() l -started V144() set
(IC ) .--> l is Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued non empty V20() Function-like one-to-one constant V33() V144() set
{(IC )} --> l is Relation-like {(IC )} -defined NAT -valued non empty Function-like constant total V30({(IC )},{l}) V33() V144() Element of K43(K44({(IC )},{l}))
{l} is non empty V33() set
K44({(IC )},{l}) is Relation-like V33() set
K43(K44({(IC )},{l})) is V33() V37() set
dom (Start-At (l,SCM+FSA)) is non empty V33() set
x is set
dom ((I ";" J),s,P) is non empty set
((I ";" J),s,P) . x is set
(J,(I,s,P),P) . x is set
((J,(I,s,P),P) +* (Start-At (((IC (J,(I,s,P),P)) + (card I)),SCM+FSA))) . x is set
((I ";" J),s,P) . x is set
(J,(I,s,P),P) . x is set
((J,(I,s,P),P) +* (Start-At (((IC (J,(I,s,P),P)) + (card I)),SCM+FSA))) . x is set
((I ";" J),s,P) . x is set
(Start-At (l,SCM+FSA)) . (IC ) is set
((J,(I,s,P),P) +* (Start-At (((IC (J,(I,s,P),P)) + (card I)),SCM+FSA))) . x is set
dom ((J,(I,s,P),P) +* (Start-At (((IC (J,(I,s,P),P)) + (card I)),SCM+FSA))) is non empty set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set
s is Relation-like the carrier of SCM+FSA -defined non empty Function-like the_Values_of SCM+FSA -compatible total set
IC s is ext-real non negative V9() V10() V11() V15() V27() integer V110() Element of NAT
s . (IC ) is set
goto (IC s) is non ins-loc-free V57( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) V100(3, SCM+FSA ) V102(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K495((IC s)) is Element of the InstructionsF of K489()
P +* ((IC s),(goto (IC s))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued non empty Function-like total set