REAL is non empty V30() set
NAT is non empty V21() V22() V23() Element of K24(REAL)
K24(REAL) is set
SCM+FSA is non empty V81(3) IC-Ins-separated strict V89(3) V108(3) with_explicit_jumps IC-relocable V143(3) AMI-Struct over 3
3 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
K577() is set
K589(NAT,K577()) is Element of K577()
K570() is non empty set
K580() is Relation-like Function-like V18(K577(),3) Element of K24(K25(K577(),3))
K25(K577(),3) is Relation-like set
K24(K25(K577(),3)) is set
K581() is non empty Relation-like 3 -defined Function-like total set
K588() is Relation-like Function-like V18(K570(),K74(K138((K580() (#) K581())),K138((K580() (#) K581())))) Element of K24(K25(K570(),K74(K138((K580() (#) K581())),K138((K580() (#) K581())))))
K580() (#) K581() is Relation-like Function-like set
K138((K580() (#) K581())) is set
K74(K138((K580() (#) K581())),K138((K580() (#) K581()))) is set
K25(K570(),K74(K138((K580() (#) K581())),K138((K580() (#) K581())))) is Relation-like set
K24(K25(K570(),K74(K138((K580() (#) K581())),K138((K580() (#) K581()))))) is set
AMI-Struct(# K577(),K589(NAT,K577()),K570(),K580(),K581(),K588() #) is strict AMI-Struct over 3
the carrier of SCM+FSA is non empty set
K354() is non empty V81(2) IC-Ins-separated strict V89(2) AMI-Struct over 2
2 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
the carrier of K354() is non empty set
K244(2,K354()) is non empty Relation-like non-empty non empty-yielding the carrier of K354() -defined Function-like total set
the Object-Kind of K354() is Relation-like Function-like V18( the carrier of K354(),2) Element of K24(K25( the carrier of K354(),2))
K25( the carrier of K354(),2) is Relation-like set
K24(K25( the carrier of K354(),2)) is set
the U7 of K354() is non empty Relation-like 2 -defined Function-like total set
the Object-Kind of K354() (#) the U7 of K354() is Relation-like Function-like set
NAT is non empty V21() V22() V23() set
K24(NAT) is set
K24(NAT) is set
9 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
Segm 9 is Element of K24(NAT)
Int-Locations is non empty set
K156() is set
K24(K156()) is set
K25(K156(),2) is Relation-like set
K24(K25(K156(),2)) is set
K158() is Relation-like Function-like V18(K156(),2) Element of K24(K25(K156(),2))
K159() is non empty Relation-like 2 -defined Function-like total set
K158() (#) K159() is Relation-like Function-like set
K138((K158() (#) K159())) is set
K150() is non empty set
K74(K138((K158() (#) K159())),K138((K158() (#) K159()))) is set
K25(K150(),K74(K138((K158() (#) K159())),K138((K158() (#) K159())))) is Relation-like set
K24(K25(K150(),K74(K138((K158() (#) K159())),K138((K158() (#) K159()))))) is set
K24( the carrier of SCM+FSA) is set
the InstructionsF of SCM+FSA is non empty Relation-like standard-ins V71() J/A-independent V74() set
INT is non empty V30() set
the InstructionsF of K354() is non empty Relation-like standard-ins V71() J/A-independent V74() set
K244(3,SCM+FSA) is non empty Relation-like non-empty non empty-yielding the carrier of SCM+FSA -defined Function-like total set
the Object-Kind of SCM+FSA is Relation-like Function-like V18( the carrier of SCM+FSA,3) Element of K24(K25( the carrier of SCM+FSA,3))
K25( the carrier of SCM+FSA,3) is Relation-like set
K24(K25( the carrier of SCM+FSA,3)) is set
the U7 of SCM+FSA is non empty Relation-like 3 -defined Function-like total set
the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA is Relation-like Function-like set
Int-Locations is non empty Element of K24( the carrier of SCM+FSA)
K378(Int-Locations) is V102() set
K24(Int-Locations) is set
FinSeq-Locations is V30() Element of K24( the carrier of SCM+FSA)
K579() is Element of K24(K577())
K24(K577()) is set
K378(FinSeq-Locations) is V102() set
K24(FinSeq-Locations) is set
COMPLEX is non empty V30() set
RAT is non empty V30() set
K25(NAT,K24(NAT)) is Relation-like set
K24(K25(NAT,K24(NAT))) is set
FinPartSt SCM+FSA is non empty Element of K24(K142(K244(3,SCM+FSA)))
K142(K244(3,SCM+FSA)) is set
K24(K142(K244(3,SCM+FSA))) is set
{ b1 where b1 is Element of K142(K244(3,SCM+FSA)) : b1 is V30() } is set
K25((FinPartSt SCM+FSA),(FinPartSt SCM+FSA)) is Relation-like set
K24(K25((FinPartSt SCM+FSA),(FinPartSt SCM+FSA))) is set
K138(K244(3,SCM+FSA)) is set
K25(NAT,K138(K244(3,SCM+FSA))) is Relation-like set
K24(K25(NAT,K138(K244(3,SCM+FSA)))) is set
K569() is set
1 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() V38() V39() V40() ext-real non positive non negative V96() Function-yielding V98() V161() V162() V163() set
the empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() V38() V39() V40() ext-real non positive non negative V96() Function-yielding V98() V161() V162() V163() set is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() V38() V39() V40() ext-real non positive non negative V96() Function-yielding V98() V161() V162() V163() set
0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V21() V22() V23() V25() V26() V27() V28() V29() V30() V38() V39() V40() ext-real non positive non negative V96() Function-yielding V98() V161() V162() V163() Element of NAT
Start-At (0,SCM+FSA) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible V30() 0 -started V162() set
IC is V49( SCM+FSA ) Element of the carrier of SCM+FSA
(IC ) .--> 0 is non empty V5() Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued Function-like one-to-one constant Function-yielding V98() set
{(IC )} is non empty set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued Function-like constant total V18({(IC )},{0}) Function-yielding V98() Element of K24(K25({(IC )},{0}))
{0} is non empty functional set
K25({(IC )},{0}) is Relation-like set
K24(K25({(IC )},{0})) is set
halt SCM+FSA is ins-loc-free V88(3, SCM+FSA ) parahalting keeping_0 V107(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
K7(0,{},{}) is set
6 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
7 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
NonZero SCM+FSA is Element of K24( the carrier of SCM+FSA)
Int-Locations \/ FinSeq-Locations is non empty Element of K24( the carrier of SCM+FSA)
intloc 0 is V61() read-only Element of the carrier of SCM+FSA
K363(0) is V61() Element of the carrier of K354()
Stop SCM+FSA is non empty V5() Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like constant V30() V69() non halt-free V78( SCM+FSA ) V79( SCM+FSA ) keeping_0 V110(3, SCM+FSA ) paraclosed parahalting good V162() set
K212((halt SCM+FSA)) is set
4 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
(intloc 0) .--> 1 is non empty V5() Relation-like the carrier of SCM+FSA -defined {(intloc 0)} -defined {(intloc 0)} -defined NAT -valued Function-like one-to-one constant K244(3,SCM+FSA) -compatible data-only set
{(intloc 0)} is non empty set
{(intloc 0)} --> 1 is non empty Relation-like non-empty non empty-yielding {(intloc 0)} -defined NAT -valued Function-like constant total V18({(intloc 0)},{1}) Element of K24(K25({(intloc 0)},{1}))
{1} is non empty V62() V63() set
K25({(intloc 0)},{1}) is Relation-like set
K24(K25({(intloc 0)},{1})) is set
Initialize ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible 0 -started set
((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible K244(3,SCM+FSA) -compatible 0 -started set
8 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
{0,6,7,8} is set
goto 2 is non ins-loc-free V75( the InstructionsF of SCM+FSA) V88(3, SCM+FSA ) good V107(3, SCM+FSA ) V109(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K360(2) is Element of the InstructionsF of K354()
Goto 2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() halt-free V79( SCM+FSA ) good V162() set
5 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
K296(NAT,0,1) is non empty Element of K24(NAT)
K157() is non empty Element of K24(K156())
dom (Initialize ((intloc 0) .--> 1)) is set
K296( the carrier of SCM+FSA,(intloc 0),(IC )) is non empty Element of K24( the carrier of SCM+FSA)
(Initialize ((intloc 0) .--> 1)) . (intloc 0) is set
(intloc 0) .--> 1 is non empty V5() Relation-like the carrier of SCM+FSA -defined {(intloc 0)} -defined {(intloc 0)} -defined NAT -valued Function-like one-to-one constant K244(3,SCM+FSA) -compatible V30() data-only V162() set
Initialize ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible V30() 0 -started V162() set
((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible K244(3,SCM+FSA) -compatible 0 -started set
IC (Initialize ((intloc 0) .--> 1)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Initialize ((intloc 0) .--> 1)) . (IC ) is set
dom (Initialize ((intloc 0) .--> 1)) is set
dom ((intloc 0) .--> 1) is non empty V5() set
dom (Start-At (0,SCM+FSA)) is non empty set
(dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) is non empty set
{(intloc 0)} is non empty Element of K24(Int-Locations)
{(intloc 0)} \/ (dom (Start-At (0,SCM+FSA))) is non empty set
{(intloc 0)} \/ {(IC )} is non empty set
Macro (halt SCM+FSA) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like V30() V69() keeping_0 paraclosed parahalting V162() set
K240(SCM+FSA,(halt SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V162() set
stop K240(SCM+FSA,(halt SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V162() set
A is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Comput (D,A,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (D,A,0)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (D,A,0)) . (IC ) is set
dom D is non empty set
CurInstr (D,(Comput (D,A,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D /. (IC (Comput (D,A,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 set
{0,1} is non empty set
IC A is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
A . (IC ) is set
D /. (IC A) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D . (IC A) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (D,A) 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
A is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() set
D is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
dom A is non empty set
i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
D is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (i,D,D) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (i,D,D)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (i,D,D)) . (IC ) is set
A is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() set
D is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
A is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() set
D is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
dom A is non empty set
i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
D is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (i,D,D) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (i,D,D)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (i,D,D)) . (IC ) is set
s is V21() V22() V23() V27() V28() V29() ext-real non negative V96() set
Comput (i,D,s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (i,D,s)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (i,D,s)) . (IC ) is set
I is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
b is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (i,D,b) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (i,D,b)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (i,D,b)) . (IC ) is set
Comput (i,D,I) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (i,D,I)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (i,D,I)) . (IC ) is set
goto (IC (Comput (i,D,I))) is non ins-loc-free V75( the InstructionsF of SCM+FSA) V88(3, SCM+FSA ) good V107(3, SCM+FSA ) V109(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K360((IC (Comput (i,D,I)))) is Element of the InstructionsF of K354()
i +* ((IC (Comput (i,D,I))),(goto (IC (Comput (i,D,I))))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Comput ((i +* ((IC (Comput (i,D,I))),(goto (IC (Comput (i,D,I)))))),D,I) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
A is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() set
FirstNotUsed A is V61() non read-only Element of the carrier of SCM+FSA
i is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
dom A is non empty set
D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (D,i,s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (D,i,s)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (D,i,s)) . (IC ) is set
I is V21() V22() V23() V27() V28() V29() ext-real non negative V96() set
Comput (D,i,I) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (D,i,I)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (D,i,I)) . (IC ) is set
b is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (D,i,b) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (D,i,b)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (D,i,b)) . (IC ) is set
(intloc 0) := (FirstNotUsed A) is ins-loc-free V75( the InstructionsF of SCM+FSA) V88(3, SCM+FSA ) parahalting V109(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
i . (intloc 0) is V28() V29() ext-real V96() set
(i . (intloc 0)) + 1 is V28() V29() ext-real V96() set
i +* ((FirstNotUsed A),((i . (intloc 0)) + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
s0 is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,b) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
P is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
dom P is non empty set
s0 . (FirstNotUsed A) is V28() V29() ext-real V96() set
P . (intloc 0) is V28() V29() ext-real V96() set
(P . (intloc 0)) + 1 is V28() V29() ext-real V96() set
UsedIntLoc A is V30() Element of K24(Int-Locations)
UsedInt*Loc A is V30() Element of K24(FinSeq-Locations)
s0 | (UsedInt*Loc A) is Relation-like the carrier of SCM+FSA -defined UsedInt*Loc A -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible set
P | (UsedInt*Loc A) is Relation-like the carrier of SCM+FSA -defined UsedInt*Loc A -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible set
s0 | (UsedIntLoc A) is Relation-like the carrier of SCM+FSA -defined UsedIntLoc A -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible set
P | (UsedIntLoc A) is Relation-like the carrier of SCM+FSA -defined UsedIntLoc A -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible set
p2 is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (D,P,p2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (D,P,p2)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (D,P,p2)) . (IC ) is set
IC (Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,b)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,b)) . (IC ) is set
b + 1 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
p2 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,p2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
(Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,p2)) . (intloc 0) is V28() V29() ext-real V96() set
dom D is non empty set
(D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))) . (IC (Comput (D,i,b))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Following ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),(Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,b))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
CurInstr ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),(Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,b))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))) /. (IC (Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,b))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),(Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,b)))),(Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,b))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)) is set
K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V18( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) Element of K24(K25( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))))
K25( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) is Relation-like set
K24(K25( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))))) is set
K76( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),(Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,b))))) is Element of K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
K76( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),(Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,b))))) . (Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,b)) is set
Exec (((intloc 0) := (FirstNotUsed A)),(Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,b))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
K76( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,((intloc 0) := (FirstNotUsed A))) is Element of K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
K76( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,((intloc 0) := (FirstNotUsed A))) . (Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,b)) is set
k is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,k) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,k)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,k)) . (IC ) is set
(Comput ((D +* ((IC (Comput (D,i,b))),((intloc 0) := (FirstNotUsed A)))),s0,b)) . (FirstNotUsed A) is V28() V29() ext-real V96() set
1 + 1 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
A is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() set
D is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
D is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (i,D,D) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
(Comput (i,D,D)) . (intloc 0) is V28() V29() ext-real V96() set
D . (intloc 0) is V28() V29() ext-real V96() set
A is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() () () set
UsedIntLoc i is V30() Element of K24(Int-Locations)
IExec (i,D,A) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
D is V61() non read-only Element of the carrier of SCM+FSA
(IExec (i,D,A)) . D is V28() V29() ext-real V96() set
A . D is V28() V29() ext-real V96() set
D +* i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialized A is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total 0 -started set
A +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible K244(3,SCM+FSA) -compatible total 0 -started set
Result ((D +* i),(Initialized A)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
(Result ((D +* i),(Initialized A))) . D is V28() V29() ext-real V96() set
A +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible K244(3,SCM+FSA) -compatible total 0 -started set
CurInstr ((D +* i),(Result ((D +* i),(Initialized A)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Result ((D +* i),(Initialized A))) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Result ((D +* i),(Initialized A))) . (IC ) is set
(D +* i) /. (IC (Result ((D +* i),(Initialized A)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput ((D +* i),(A +* (Initialize ((intloc 0) .--> 1))),s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
dom i is non empty set
I is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput ((D +* i),(Initialized A),I) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput ((D +* i),(Initialized A),I)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput ((D +* i),(Initialized A),I)) . (IC ) is set
(Initialized A) . D is V28() V29() ext-real V96() set
A is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() () () set
UsedInt*Loc i is V30() Element of K24(FinSeq-Locations)
IExec (i,D,A) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
D is FinSeq-Location
(IExec (i,D,A)) . D is Relation-like NAT -defined INT -valued Function-like V30() V38() V39() V162() M7( INT )
A . D is Relation-like NAT -defined INT -valued Function-like V30() V38() V39() V162() M7( INT )
D +* i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialized A is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total 0 -started set
A +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible K244(3,SCM+FSA) -compatible total 0 -started set
Result ((D +* i),(Initialized A)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
(Result ((D +* i),(Initialized A))) . D is Relation-like NAT -defined INT -valued Function-like V30() V38() V39() V162() M7( INT )
CurInstr ((D +* i),(Result ((D +* i),(Initialized A)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Result ((D +* i),(Initialized A))) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Result ((D +* i),(Initialized A))) . (IC ) is set
(D +* i) /. (IC (Result ((D +* i),(Initialized A)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput ((D +* i),(Initialized A),s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
dom i is non empty set
I is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput ((D +* i),(Initialized A),I) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput ((D +* i),(Initialized A),I)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput ((D +* i),(Initialized A),I)) . (IC ) is set
(Initialized A) . D is Relation-like NAT -defined INT -valued Function-like V30() V38() V39() V162() M7( INT )
A is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() set
A is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
DataPart A is Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible data-only set
A | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible set
D is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC D is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
D . (IC ) is set
DataPart D is Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible data-only set
D | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible set
i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() () () set
I is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Reloc (s,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V162() set
IncAddr (s,I) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() set
Shift ((IncAddr (s,I)),I) is Relation-like Function-like set
Comput (i,A,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
DataPart (Comput (i,A,0)) is Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible data-only set
(Comput (i,A,0)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible set
Comput (D,D,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
DataPart (Comput (D,D,0)) is Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible data-only set
(Comput (D,D,0)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible set
b is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (i,A,b) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (i,A,b)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (i,A,b)) . (IC ) is set
(IC (Comput (i,A,b))) + I is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (D,D,b) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (D,D,b)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (D,D,b)) . (IC ) is set
CurInstr (i,(Comput (i,A,b))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i /. (IC (Comput (i,A,b))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (i,(Comput (i,A,b)))),I) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (D,(Comput (D,D,b))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D /. (IC (Comput (D,D,b))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
DataPart (Comput (i,A,b)) is Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible data-only set
(Comput (i,A,b)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible set
DataPart (Comput (D,D,b)) is Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible data-only set
(Comput (D,D,b)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible set
b + 1 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
Comput (i,A,(b + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (i,A,(b + 1))) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (i,A,(b + 1))) . (IC ) is set
(IC (Comput (i,A,(b + 1)))) + I is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (D,D,(b + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (D,D,(b + 1))) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (D,D,(b + 1))) . (IC ) is set
CurInstr (i,(Comput (i,A,(b + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i /. (IC (Comput (i,A,(b + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (i,(Comput (i,A,(b + 1))))),I) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (D,(Comput (D,D,(b + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D /. (IC (Comput (D,D,(b + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
DataPart (Comput (i,A,(b + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible data-only set
(Comput (i,A,(b + 1))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible set
DataPart (Comput (D,D,(b + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible data-only set
(Comput (D,D,(b + 1))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible set
Following (i,(Comput (i,A,b))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
Exec ((CurInstr (i,(Comput (i,A,b)))),(Comput (i,A,b))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)) is set
K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V18( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) Element of K24(K25( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))))
K25( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) is Relation-like set
K24(K25( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))))) is set
K76( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i,(Comput (i,A,b))))) is Element of K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
K76( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i,(Comput (i,A,b))))) . (Comput (i,A,b)) is set
Following (D,(Comput (D,D,b))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
Exec ((CurInstr (D,(Comput (D,D,b)))),(Comput (D,D,b))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
K76( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (D,(Comput (D,D,b))))) is Element of K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
K76( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (D,(Comput (D,D,b))))) . (Comput (D,D,b)) is set
dom s is non empty set
dom (Reloc (s,I)) is set
a is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
IT is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i . (IC (Comput (i,A,(b + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s . a is set
a + I is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Reloc (s,I)) . (a + I) is set
(Reloc (s,I)) . (IC (Comput (D,D,(b + 1)))) is set
D . (IC (Comput (D,D,(b + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom s is non empty set
IC A is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
A . (IC ) is set
i . (IC A) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i . (IC (Initialize ((intloc 0) .--> 1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s . 0 is set
b is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (i,A,b) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (i,A,b)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (i,A,b)) . (IC ) is set
(IC (Comput (i,A,b))) + I is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (D,D,b) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (D,D,b)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (D,D,b)) . (IC ) is set
CurInstr (i,(Comput (i,A,b))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i /. (IC (Comput (i,A,b))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (i,(Comput (i,A,b)))),I) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (D,(Comput (D,D,b))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D /. (IC (Comput (D,D,b))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
DataPart (Comput (i,A,b)) is Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible data-only set
(Comput (i,A,b)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible set
DataPart (Comput (D,D,b)) is Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible data-only set
(Comput (D,D,b)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible set
0 + I is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
dom (Reloc (s,I)) is set
IC (Comput (i,A,0)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (i,A,0)) . (IC ) is set
D /. (IC D) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D . (IC D) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i /. (IC A) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (i,(Comput (i,A,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i /. (IC (Comput (i,A,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (i,(Comput (i,A,0)))),I) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (i,A) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (i,A)),I) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Reloc (s,I)) . (0 + I) is set
CurInstr (D,D) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (D,(Comput (D,D,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (D,D,0)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (D,D,0)) . (IC ) is set
D /. (IC (Comput (D,D,0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(IC (Comput (i,A,0))) + I is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
A is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
D is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() () () set
I is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (i,A,I) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
Comput (D,D,I) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
CurInstr (i,(Comput (i,A,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (i,A,I)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (i,A,I)) . (IC ) is set
i /. (IC (Comput (i,A,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
CurInstr (D,(Comput (D,D,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (D,D,I)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (D,D,I)) . (IC ) is set
D /. (IC (Comput (D,D,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
dom s is non empty set
b is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (D,D,b) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (D,D,b)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (D,D,b)) . (IC ) is set
D . (IC (Comput (D,D,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
s . (IC (Comput (D,D,I))) is set
i . (IC (Comput (i,A,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
A is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
D is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
LifeSpan (i,A) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Result (i,A) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
LifeSpan (D,D) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Result (D,D) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
s is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() () () set
I is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (D,D,I) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
CurInstr (D,(Comput (D,D,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (D,D,I)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (D,D,I)) . (IC ) is set
D /. (IC (Comput (D,D,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (i,A,I) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
CurInstr (i,(Comput (i,A,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (i,A,I)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (i,A,I)) . (IC ) is set
i /. (IC (Comput (i,A,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (D,D,(LifeSpan (i,A))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
CurInstr (D,(Comput (D,D,(LifeSpan (i,A))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (D,D,(LifeSpan (i,A)))) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (D,D,(LifeSpan (i,A)))) . (IC ) is set
D /. (IC (Comput (D,D,(LifeSpan (i,A))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Comput (i,A,(LifeSpan (i,A))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
CurInstr (i,(Comput (i,A,(LifeSpan (i,A))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (i,A,(LifeSpan (i,A)))) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (i,A,(LifeSpan (i,A)))) . (IC ) is set
i /. (IC (Comput (i,A,(LifeSpan (i,A))))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
A is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() () () () set
IExec (i,D,A) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
(IExec (i,D,A)) . (intloc 0) is V28() V29() ext-real V96() set
Initialized A is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total 0 -started set
A +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible K244(3,SCM+FSA) -compatible total 0 -started set
D +* i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Result ((D +* i),(Initialized A)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
CurInstr ((D +* i),(Result ((D +* i),(Initialized A)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Result ((D +* i),(Initialized A))) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Result ((D +* i),(Initialized A))) . (IC ) is set
(D +* i) /. (IC (Result ((D +* i),(Initialized A)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(Result ((D +* i),(Initialized A))) . (intloc 0) is V28() V29() ext-real V96() set
D is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput ((D +* i),(Initialized A),D) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
the non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() paraclosed V162() () set is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() paraclosed V162() () set
A is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
LifeSpan (D,A) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() () set
D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() set
i ";" D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() set
stop i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() set
K202(i,(Stop SCM+FSA)) is Relation-like Function-like V25() 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 V30() V162() set
card i is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Reloc (D,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V162() set
IncAddr (D,(card i)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() set
Shift ((IncAddr (D,(card i))),(card i)) is Relation-like Function-like set
(Directed (CutLastLoc (stop i))) +* (Reloc (D,(card i))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like set
D +* (i ";" D) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
I is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (D,A,I) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
Comput ((D +* (i ";" D)),A,I) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
I + 1 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
Comput (D,A,(I + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
Comput ((D +* (i ";" D)),A,(I + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
dom (i ";" D) is non empty set
Directed i is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() halt-free V79( SCM+FSA ) V162() set
Directed (i,(card i)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() halt-free V162() set
goto (card i) is non ins-loc-free V75( the InstructionsF of SCM+FSA) V88(3, SCM+FSA ) good V107(3, SCM+FSA ) V109(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K360((card i)) is Element of the InstructionsF of K354()
i +~ ((halt SCM+FSA),(goto (card i))) is Relation-like Function-like set
dom (Directed i) is non empty set
dom (Reloc (D,(card i))) is set
(dom (Directed i)) \/ (dom (Reloc (D,(card i)))) is non empty set
dom i is non empty set
(dom i) \/ (dom (Reloc (D,(card i)))) is non empty set
Following (D,(Comput (D,A,I))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
CurInstr (D,(Comput (D,A,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (D,A,I)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (D,A,I)) . (IC ) is set
D /. (IC (Comput (D,A,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (D,(Comput (D,A,I)))),(Comput (D,A,I))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)) is set
K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V18( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) Element of K24(K25( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))))
K25( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) is Relation-like set
K24(K25( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))))) is set
K76( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (D,(Comput (D,A,I))))) is Element of K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
K76( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (D,(Comput (D,A,I))))) . (Comput (D,A,I)) is set
Following ((D +* (i ";" D)),(Comput ((D +* (i ";" D)),A,I))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
CurInstr ((D +* (i ";" D)),(Comput ((D +* (i ";" D)),A,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput ((D +* (i ";" D)),A,I)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput ((D +* (i ";" D)),A,I)) . (IC ) is set
(D +* (i ";" D)) /. (IC (Comput ((D +* (i ";" D)),A,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr ((D +* (i ";" D)),(Comput ((D +* (i ";" D)),A,I)))),(Comput ((D +* (i ";" D)),A,I))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
K76( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((D +* (i ";" D)),(Comput ((D +* (i ";" D)),A,I))))) is Element of K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
K76( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((D +* (i ";" D)),(Comput ((D +* (i ";" D)),A,I))))) . (Comput ((D +* (i ";" D)),A,I)) is set
D . (IC (Comput (D,A,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
i . (IC (Comput (D,A,I))) is set
(D +* (i ";" D)) . (IC (Comput ((D +* (i ";" D)),A,I))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
(i ";" D) . (IC (Comput (D,A,I))) is set
Comput (D,A,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
Comput ((D +* (i ";" D)),A,0) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
A is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() () set
D +* D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Directed D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() halt-free V79( SCM+FSA ) V162() set
card D is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Directed (D,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() halt-free V162() set
goto (card D) is non ins-loc-free V75( the InstructionsF of SCM+FSA) V88(3, SCM+FSA ) good V107(3, SCM+FSA ) V109(3, SCM+FSA ) with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K360((card D)) is Element of the InstructionsF of K354()
D +~ ((halt SCM+FSA),(goto (card D))) is Relation-like Function-like set
LifeSpan ((D +* D),A) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(LifeSpan ((D +* D),A)) + 1 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
Comput (D,A,((LifeSpan ((D +* D),A)) + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput (D,A,((LifeSpan ((D +* D),A)) + 1))) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (D,A,((LifeSpan ((D +* D),A)) + 1))) . (IC ) is set
A +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible K244(3,SCM+FSA) -compatible total 0 -started set
EP is Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible set
(A +* (Initialize ((intloc 0) .--> 1))) +* EP is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
D ";" D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() set
stop D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() set
K202(D,(Stop SCM+FSA)) is Relation-like Function-like V25() 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 V30() V162() set
Reloc (D,(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V162() set
IncAddr (D,(card D)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V30() V69() V162() 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 set
(D +* D) +* (D ";" D) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
IT is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
LifeSpan ((D +* D),IT) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput ((D +* D),IT,(LifeSpan ((D +* D),IT))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
IC (Comput ((D +* D),IT,(LifeSpan ((D +* D),IT)))) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput ((D +* D),IT,(LifeSpan ((D +* D),IT)))) . (IC ) is set
dom D is non empty set
IT +* EP is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
(D +* D) +* (Directed D) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s2 is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
p2 is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
Comput (((D +* D) +* (D ";" D)),((A +* (Initialize ((intloc 0) .--> 1))) +* EP),p2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
Comput (((D +* D) +* (Directed D)),(IT +* EP),p2) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
p2 + 1 is non empty V21() V22() V23() V27() V28() V29() V62() ext-real positive non negative V96() Element of NAT
Comput (((D +* D) +* (D ";" D)),((A +* (Initialize ((intloc 0) .--> 1))) +* EP),(p2 + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
Comput (((D +* D) +* (Directed D)),(IT +* EP),(p2 + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
Following (((D +* D) +* (Directed D)),(Comput (((D +* D) +* (Directed D)),(IT +* EP),p2))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
CurInstr (((D +* D) +* (Directed D)),(Comput (((D +* D) +* (Directed D)),(IT +* EP),p2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (((D +* D) +* (Directed D)),(IT +* EP),p2)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (((D +* D) +* (Directed D)),(IT +* EP),p2)) . (IC ) is set
((D +* D) +* (Directed D)) /. (IC (Comput (((D +* D) +* (Directed D)),(IT +* EP),p2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (((D +* D) +* (Directed D)),(Comput (((D +* D) +* (Directed D)),(IT +* EP),p2)))),(Comput (((D +* D) +* (Directed D)),(IT +* EP),p2))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)) is set
K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V18( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) Element of K24(K25( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))))
K25( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) is Relation-like set
K24(K25( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))))) is set
K76( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (((D +* D) +* (Directed D)),(Comput (((D +* D) +* (Directed D)),(IT +* EP),p2))))) is Element of K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))
K76( the InstructionsF of SCM+FSA,K74(K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K138(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (((D +* D) +* (Directed D)),(Comput (((D +* D) +* (Directed D)),(IT +* EP),p2))))) . (Comput (((D +* D) +* (Directed D)),(IT +* EP),p2)) is set
Following (((D +* D) +* (D ";" D)),(Comput (((D +* D) +* (D ";" D)),((A +* (Initialize ((intloc 0) .--> 1))) +* EP),p2))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K244(3,SCM+FSA) -compatible total set
CurInstr (((D +* D) +* (D ";" D)),(Comput (((D +* D) +* (D ";" D)),((A +* (Initialize ((intloc 0) .--> 1))) +* EP),p2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
IC (Comput (((D +* D) +* (D ";" D)),((A +* (Initialize ((intloc 0) .--> 1))) +* EP),p2)) is V21() V22() V23() V27() V28() V29() ext-real non negative V96() Element of NAT
(Comput (((D +* D) +* (D ";" D)),((A +* (Initialize ((intloc 0) .--> 1))) +* EP),p2)) . (IC ) is set
((D +* D) +* (D ";" D)) /. (IC (Comput (((D +* D) +* (D ";" D)),((A +* (Initialize ((intloc 0) .--> 1))) +* EP),p2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (((D +* D) +* (D ";" D)),(Comput (((