:: SCM_HALT semantic presentation

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

{ b

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