:: SCMFSA8A semantic presentation

REAL is non empty V5() V28() V66() V119() V120() V121() V125() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V119() V120() V121() V122() V123() V124() V125() Element of K32(REAL)

K32(REAL) is set

SCM+FSA is non empty V84(3) IC-Ins-separated strict V92(3) with_explicit_jumps IC-relocable V144(3) V154(3) AMI-Struct over 3

3 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V63() V65() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

the U1 of SCM+FSA is non empty set

NAT is non empty epsilon-transitive epsilon-connected ordinal V119() V120() V121() V122() V123() V124() V125() set

K32(NAT) is set

K32(NAT) is set

9 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V63() V65() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Segm 9 is V119() V120() V121() V122() V123() V124() Element of K32(NAT)

Int-Locations is non empty set

K186() is set

K32(K186()) is set

2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V63() V65() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

K33(K186(),2) is Relation-like set

K32(K33(K186(),2)) is set

K188() is Relation-like Function-like V40(K186(),2) Element of K32(K33(K186(),2))

K189() is non empty Relation-like 2 -defined Function-like total set

K188() (#) K189() is Relation-like Function-like set

K162((K188() (#) K189())) is set

K180() is non empty set

K141(K162((K188() (#) K189())),K162((K188() (#) K189()))) is set

K33(K180(),K141(K162((K188() (#) K189())),K162((K188() (#) K189())))) is Relation-like set

K32(K33(K180(),K141(K162((K188() (#) K189())),K162((K188() (#) K189()))))) is set

K32( the U1 of SCM+FSA) is set

the InstructionsF of SCM+FSA is non empty Relation-like standard-ins V74() J/A-independent V77() set

INT is non empty V5() V28() V66() V119() V120() V121() V122() V123() V125() set

Int-Locations is non empty Element of K32( the U1 of SCM+FSA)

K324(Int-Locations) is V98() set

K32(Int-Locations) is set

FinSeq-Locations is non empty V5() V28() V66() Element of K32( the U1 of SCM+FSA)

K324(FinSeq-Locations) is V98() set

K32(FinSeq-Locations) is set

K274(3,SCM+FSA) is non empty Relation-like non-empty non empty-yielding the U1 of SCM+FSA -defined Function-like total set

the Object-Kind of SCM+FSA is Relation-like Function-like V40( the U1 of SCM+FSA,3) Element of K32(K33( the U1 of SCM+FSA,3))

K33( the U1 of SCM+FSA,3) is Relation-like set

K32(K33( the U1 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

COMPLEX is non empty V5() V28() V66() V119() V125() set

RAT is non empty V5() V28() V66() V119() V120() V121() V122() V125() set

K33(NAT,K32(NAT)) is Relation-like set

K32(K33(NAT,K32(NAT))) is set

FinPartSt SCM+FSA is non empty Element of K32(K166(K274(3,SCM+FSA)))

K166(K274(3,SCM+FSA)) is set

K32(K166(K274(3,SCM+FSA))) is set

{ b

K33((FinPartSt SCM+FSA),(FinPartSt SCM+FSA)) is Relation-like set

K32(K33((FinPartSt SCM+FSA),(FinPartSt SCM+FSA))) is set

1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V63() V65() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V28() V29() V32() V36() V37() V38() initial V119() V120() V121() V122() V123() V124() V125() Function-yielding V150() set

0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V27() V28() V29() V32() V36() V37() V38() V63() initial V107() V108() V119() V120() V121() V122() V123() V124() V125() Function-yielding V150() Element of NAT

12 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V63() V65() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

4 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V63() V65() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

5 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V63() V65() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

6 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V63() V65() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

7 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V63() V65() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

8 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V63() V65() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

10 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V63() V65() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

11 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V27() V63() V65() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

IC is V51( SCM+FSA ) Element of the U1 of SCM+FSA

the U2 of SCM+FSA is Element of the U1 of SCM+FSA

halt SCM+FSA is ins-loc-free V91(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V143(3, SCM+FSA ) 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

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

intloc 0 is V64() V160() Element of the U1 of SCM+FSA

Data-Locations is Element of K32( the U1 of SCM+FSA)

[#] SCM+FSA is non empty non proper Element of K32( the U1 of SCM+FSA)

{(IC )} is non empty V28() set

([#] SCM+FSA) \ {(IC )} is Element of K32( the U1 of SCM+FSA)

Start-At (0,SCM+FSA) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible V28() 0 -started set

(IC ) .--> 0 is V5() Relation-like the U1 of SCM+FSA -defined {(IC )} -defined NAT -valued Function-like one-to-one constant V28() Function-yielding V150() set

{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued Function-like constant V28() total V40({(IC )},{0}) Function-yielding V150() Element of K32(K33({(IC )},{0}))

{0} is non empty functional V28() V32() V119() V120() V121() V122() V123() V124() set

K33({(IC )},{0}) is Relation-like V28() set

K32(K33({(IC )},{0})) is V28() V32() set

(intloc 0) .--> 1 is V5() Relation-like the U1 of SCM+FSA -defined {(intloc 0)} -defined {(intloc 0)} -defined NAT -valued Function-like one-to-one constant K274(3,SCM+FSA) -compatible V28() data-only set

{(intloc 0)} is non empty V28() set

{(intloc 0)} --> 1 is non empty Relation-like non-empty non empty-yielding {(intloc 0)} -defined NAT -valued Function-like constant V28() total V40({(intloc 0)},{1}) Element of K32(K33({(intloc 0)},{1}))

{1} is non empty V28() V65() V66() V119() V120() V121() V122() V123() V124() set

K33({(intloc 0)},{1}) is Relation-like V28() set

K32(K33({(intloc 0)},{1})) is V28() V32() set

J is set

P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

dom P is V28() V119() V120() V121() V122() V123() V124() set

P . J is set

I is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Directed (P,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() halt-free set

goto I is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

P +~ ((halt SCM+FSA),(goto I)) is Relation-like Function-like set

(Directed (P,I)) . J is set

P is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

I is V64() Element of the U1 of SCM+FSA

J is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

IncAddr (P,J) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

InsCode P is ext-real epsilon-transitive epsilon-connected ordinal natural Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K23( the InstructionsF of SCM+FSA) is set

InsCode P is ext-real epsilon-transitive epsilon-connected ordinal natural Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K23( the InstructionsF of SCM+FSA) is set

s is V64() Element of the U1 of SCM+FSA

s1 is V64() Element of the U1 of SCM+FSA

s := s1 is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable sequential Element of the InstructionsF of SCM+FSA

InsCode P is ext-real epsilon-transitive epsilon-connected ordinal natural Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K23( the InstructionsF of SCM+FSA) is set

s is V64() Element of the U1 of SCM+FSA

s1 is V64() Element of the U1 of SCM+FSA

AddTo (s,s1) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable sequential Element of the InstructionsF of SCM+FSA

InsCode P is ext-real epsilon-transitive epsilon-connected ordinal natural Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K23( the InstructionsF of SCM+FSA) is set

s is V64() Element of the U1 of SCM+FSA

s1 is V64() Element of the U1 of SCM+FSA

SubFrom (s,s1) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable sequential Element of the InstructionsF of SCM+FSA

InsCode P is ext-real epsilon-transitive epsilon-connected ordinal natural Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K23( the InstructionsF of SCM+FSA) is set

s is V64() Element of the U1 of SCM+FSA

s1 is V64() Element of the U1 of SCM+FSA

MultBy (s,s1) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable sequential Element of the InstructionsF of SCM+FSA

InsCode P is ext-real epsilon-transitive epsilon-connected ordinal natural Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K23( the InstructionsF of SCM+FSA) is set

s is V64() Element of the U1 of SCM+FSA

s1 is V64() Element of the U1 of SCM+FSA

Divide (s,s1) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable sequential Element of the InstructionsF of SCM+FSA

InsCode P is ext-real epsilon-transitive epsilon-connected ordinal natural Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K23( the InstructionsF of SCM+FSA) is set

s is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

goto s is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

s + J is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

goto (s + J) is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

InsCode P is ext-real epsilon-transitive epsilon-connected ordinal natural Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K23( the InstructionsF of SCM+FSA) is set

s is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

s1 is V64() Element of the U1 of SCM+FSA

s1 =0_goto s is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

s + J is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

s1 =0_goto (s + J) is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

InsCode P is ext-real epsilon-transitive epsilon-connected ordinal natural Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K23( the InstructionsF of SCM+FSA) is set

s is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

s1 is V64() Element of the U1 of SCM+FSA

s1 >0_goto s is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

s + J is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

s1 >0_goto (s + J) is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

InsCode P is ext-real epsilon-transitive epsilon-connected ordinal natural Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K23( the InstructionsF of SCM+FSA) is set

s1 is V64() Element of the U1 of SCM+FSA

s is V64() Element of the U1 of SCM+FSA

P2 is FinSeq-Location

s1 := (P2,s) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V143(3, SCM+FSA ) sequential Element of the InstructionsF of SCM+FSA

InsCode P is ext-real epsilon-transitive epsilon-connected ordinal natural Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K23( the InstructionsF of SCM+FSA) is set

s1 is V64() Element of the U1 of SCM+FSA

s is V64() Element of the U1 of SCM+FSA

P2 is FinSeq-Location

(P2,s) := s1 is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V143(3, SCM+FSA ) sequential Element of the InstructionsF of SCM+FSA

InsCode P is ext-real epsilon-transitive epsilon-connected ordinal natural Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K23( the InstructionsF of SCM+FSA) is set

s is V64() Element of the U1 of SCM+FSA

s1 is FinSeq-Location

s :=len s1 is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V143(3, SCM+FSA ) sequential Element of the InstructionsF of SCM+FSA

InsCode P is ext-real epsilon-transitive epsilon-connected ordinal natural Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K23( the InstructionsF of SCM+FSA) is set

s is V64() Element of the U1 of SCM+FSA

s1 is FinSeq-Location

s1 :=<0,...,0> s is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V143(3, SCM+FSA ) sequential Element of the InstructionsF of SCM+FSA

InsCode P is ext-real epsilon-transitive epsilon-connected ordinal natural Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

K23( the InstructionsF of SCM+FSA) is set

P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

I is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Reloc (P,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

IncAddr (P,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

Shift ((IncAddr (P,I)),I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

J is V64() Element of the U1 of SCM+FSA

dom (IncAddr (P,I)) is V28() V119() V120() V121() V122() V123() V124() set

dom P is V28() V119() V120() V121() V122() V123() V124() set

dom (Shift ((IncAddr (P,I)),I)) is V28() V119() V120() V121() V122() V123() V124() set

{ (b

s is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

rng (Reloc (P,I)) is V28() set

s1 is set

(Shift ((IncAddr (P,I)),I)) . s1 is set

P2 is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

P2 + I is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

P . P2 is set

rng P is V28() set

P2 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(IncAddr (P,I)) . P2 is set

P /. P2 is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IncAddr ((P /. P2),I) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IncAddr (P2,I) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() good set

I is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Reloc (P,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

IncAddr (P,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

Shift ((IncAddr (P,I)),I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

P +* I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

J is V64() Element of the U1 of SCM+FSA

rng (P +* I) is V28() set

rng P is V28() set

rng I is V28() set

(rng P) \/ (rng I) is V28() set

s is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() good set

I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() good set

P +* I is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

I is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Directed (P,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() halt-free set

goto I is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

P +~ ((halt SCM+FSA),(goto I)) is Relation-like Function-like set

J is V64() Element of the U1 of SCM+FSA

dom (Directed (P,I)) is V28() V119() V120() V121() V122() V123() V124() set

dom P is V28() V119() V120() V121() V122() V123() V124() set

s is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

rng (Directed (P,I)) is V28() set

s1 is set

(Directed (P,I)) . s1 is set

P . s1 is set

rng P is V28() set

P . s1 is set

P . s1 is set

P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() good set

I is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Directed (P,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() halt-free set

goto I is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

P +~ ((halt SCM+FSA),(goto I)) is Relation-like Function-like set

P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial good set

Directed P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial halt-free V82( SCM+FSA ) set

card P is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom P is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() set

Directed (P,(card P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() halt-free good set

goto (card P) is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

P +~ ((halt SCM+FSA),(goto (card P))) is Relation-like Function-like set

P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

I is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Directed (P,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() halt-free set

goto I is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

P +~ ((halt SCM+FSA),(goto I)) is Relation-like Function-like set

s is ext-real epsilon-transitive epsilon-connected ordinal natural set

dom (Directed (P,I)) is V28() V119() V120() V121() V122() V123() V124() set

dom P is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() Element of K32(NAT)

J is ext-real epsilon-transitive epsilon-connected ordinal natural set

P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial good set

I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial good set

P ";" I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

stop P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

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 T-Sequence-like V28() initial non halt-free V81( SCM+FSA ) V82( SCM+FSA ) good V146(3, SCM+FSA ) parahalting set

<%(halt SCM+FSA)%> is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() 1 -element initial set

K232(P,(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

CutLastLoc (stop P) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

Directed (CutLastLoc (stop P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() halt-free set

card (CutLastLoc (stop P)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom (CutLastLoc (stop P)) is ext-real epsilon-transitive epsilon-connected ordinal natural V28() V119() V120() V121() V122() V123() V124() set

Directed ((CutLastLoc (stop P)),(card (CutLastLoc (stop P)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() halt-free set

goto (card (CutLastLoc (stop P))) is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

(CutLastLoc (stop P)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop P))))) is Relation-like Function-like set

card P is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom P is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() set

Reloc (I,(card P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

IncAddr (I,(card P)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

Shift ((IncAddr (I,(card P))),(card P)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

(Directed (CutLastLoc (stop P))) +* (Reloc (I,(card P))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

P is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

goto P is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

0 .--> (goto P) is V5() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V28() set

{0} --> (goto P) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V28() total V40({0},{(goto P)}) Element of K32(K33({0},{(goto P)}))

{(goto P)} is non empty V28() set

K33({0},{(goto P)}) is Relation-like V28() set

K32(K33({0},{(goto P)})) is V28() V32() set

dom (0 .--> (goto P)) is V5() V28() V119() V120() V121() V122() V123() V124() set

(0 .--> (goto P)) . 0 is set

card (0 .--> (goto P)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

rng (0 .--> (goto P)) is V5() V28() set

<%(goto P)%> is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() 1 -element initial set

card <%(goto P)%> is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom <%(goto P)%> is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() set

P is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

goto P is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

0 .--> (goto P) is V5() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V28() set

{0} --> (goto P) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V28() total V40({0},{(goto P)}) Element of K32(K33({0},{(goto P)}))

{(goto P)} is non empty V28() set

K33({0},{(goto P)}) is Relation-like V28() set

K32(K33({0},{(goto P)})) is V28() V32() set

<%(goto P)%> is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() 1 -element initial set

I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

rng (0 .--> (goto P)) is V5() V28() set

s is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

P is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(P) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

goto P is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

0 .--> (goto P) is V5() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V28() set

{0} --> (goto P) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V28() total V40({0},{(goto P)}) Element of K32(K33({0},{(goto P)}))

{(goto P)} is non empty V28() set

K33({0},{(goto P)}) is Relation-like V28() set

K32(K33({0},{(goto P)})) is V28() V32() set

<%(goto P)%> is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() 1 -element initial set

I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

rng I is non empty V28() set

rng (0 .--> (goto P)) is V5() V28() set

s is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

(0) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial halt-free V82( SCM+FSA ) good set

goto 0 is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

0 .--> (goto 0) is V5() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V28() set

{0} --> (goto 0) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V28() total V40({0},{(goto 0)}) Element of K32(K33({0},{(goto 0)}))

{(goto 0)} is non empty V28() set

K33({0},{(goto 0)}) is Relation-like V28() set

K32(K33({0},{(goto 0)})) is V28() V32() set

(intloc 0) := (intloc 0) is ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable sequential Element of the InstructionsF of SCM+FSA

P is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set

J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

I +* J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set

Initialize P is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set

P +* (Start-At (0,SCM+FSA)) is non empty Relation-like the U1 of SCM+FSA -defined the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set

card J is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom J is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() set

dom J is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() Element of K32(NAT)

s is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Comput ((I +* J),(Initialize P),s) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

IC (Comput ((I +* J),(Initialize P),s)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* J),(Initialize P),s)) . (IC ) is set

s1 is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Comput ((I +* J),(Initialize P),s1) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

IC (Comput ((I +* J),(Initialize P),s1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* J),(Initialize P),s1)) . (IC ) is set

s1 is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Comput ((I +* J),(Initialize P),s1) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

IC (Comput ((I +* J),(Initialize P),s1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* J),(Initialize P),s1)) . (IC ) is set

P2 is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Comput ((I +* J),(Initialize P),P2) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

IC (Comput ((I +* J),(Initialize P),P2)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* J),(Initialize P),P2)) . (IC ) is set

s is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

card s is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom s is ext-real epsilon-transitive epsilon-connected ordinal natural V28() V119() V120() V121() V122() V123() V124() set

dom s is ext-real epsilon-transitive epsilon-connected ordinal natural V28() V119() V120() V121() V122() V123() V124() Element of K32(NAT)

P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

dom P is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() Element of K32(NAT)

I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

P ";" I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

stop P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

K232(P,(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

CutLastLoc (stop P) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

Directed (CutLastLoc (stop P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() halt-free set

card (CutLastLoc (stop P)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom (CutLastLoc (stop P)) is ext-real epsilon-transitive epsilon-connected ordinal natural V28() V119() V120() V121() V122() V123() V124() set

Directed ((CutLastLoc (stop P)),(card (CutLastLoc (stop P)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() halt-free set

goto (card (CutLastLoc (stop P))) is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

(CutLastLoc (stop P)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop P))))) is Relation-like Function-like set

card P is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom P is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() set

Reloc (I,(card P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

IncAddr (I,(card P)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

Shift ((IncAddr (I,(card P))),(card P)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

(Directed (CutLastLoc (stop P))) +* (Reloc (I,(card P))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

Directed P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial halt-free V82( SCM+FSA ) set

Directed (P,(card P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial halt-free set

goto (card P) is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

P +~ ((halt SCM+FSA),(goto (card P))) is Relation-like Function-like set

J is set

(P ";" I) . J is set

(Directed P) . J is set

dom (Directed P) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() Element of K32(NAT)

P is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(P) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial halt-free V82( SCM+FSA ) good set

goto P is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

0 .--> (goto P) is V5() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V28() set

{0} --> (goto P) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued Function-like constant V28() total V40({0},{(goto P)}) Element of K32(K33({0},{(goto P)}))

{(goto P)} is non empty V28() set

K33({0},{(goto P)}) is Relation-like V28() set

K32(K33({0},{(goto P)})) is V28() V32() set

card (P) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom (P) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() set

I is set

P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

dom P is V28() V119() V120() V121() V122() V123() V124() set

P . I is set

Directed P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() halt-free set

card P is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Directed (P,(card P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() halt-free set

goto (card P) is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

P +~ ((halt SCM+FSA),(goto (card P))) is Relation-like Function-like set

(Directed P) . I is set

P is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

Initialize P is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set

P +* (Start-At (0,SCM+FSA)) is non empty Relation-like the U1 of SCM+FSA -defined the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set

I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set

J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

(P,I,J) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

I +* J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set

dom J is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() Element of K32(NAT)

Comput ((I +* J),(Initialize P),(P,I,J)) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

IC (Comput ((I +* J),(Initialize P),(P,I,J))) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* J),(Initialize P),(P,I,J))) . (IC ) is set

card J is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom J is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() set

s1 is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Comput ((I +* J),(Initialize P),s1) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

IC (Comput ((I +* J),(Initialize P),s1)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* J),(Initialize P),s1)) . (IC ) is set

CurInstr ((I +* J),(Comput ((I +* J),(Initialize P),s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(I +* J) /. (IC (Comput ((I +* J),(Initialize P),s1))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

P is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

Initialize P is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set

P +* (Start-At (0,SCM+FSA)) is non empty Relation-like the U1 of SCM+FSA -defined the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set

I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set

J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

(P,I,J) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

I +* J 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 T-Sequence-like V28() initial set

J ";" s is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

stop J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

K232(J,(Stop SCM+FSA)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

CutLastLoc (stop J) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

Directed (CutLastLoc (stop J)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() halt-free set

card (CutLastLoc (stop J)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom (CutLastLoc (stop J)) is ext-real epsilon-transitive epsilon-connected ordinal natural V28() V119() V120() V121() V122() V123() V124() set

Directed ((CutLastLoc (stop J)),(card (CutLastLoc (stop J)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() halt-free set

goto (card (CutLastLoc (stop J))) is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

(CutLastLoc (stop J)) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop J))))) is Relation-like Function-like set

card J is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom J is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() set

Reloc (s,(card J)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

IncAddr (s,(card J)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

Shift ((IncAddr (s,(card J))),(card J)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

(Directed (CutLastLoc (stop J))) +* (Reloc (s,(card J))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

I +* (J ";" s) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set

dom (I +* J) is non empty V119() V120() V121() V122() V123() V124() set

dom (I +* (J ";" s)) is non empty V119() V120() V121() V122() V123() V124() set

P2 is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Comput ((I +* J),(Initialize P),P2) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

Comput ((I +* (J ";" s)),(Initialize P),P2) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

P2 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Comput ((I +* J),(Initialize P),(P2 + 1)) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

Comput ((I +* (J ";" s)),(Initialize P),(P2 + 1)) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

Following ((I +* (J ";" s)),(Comput ((I +* (J ";" s)),(Initialize P),P2))) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

CurInstr ((I +* (J ";" s)),(Comput ((I +* (J ";" s)),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IC (Comput ((I +* (J ";" s)),(Initialize P),P2)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* (J ";" s)),(Initialize P),P2)) . (IC ) is set

(I +* (J ";" s)) /. (IC (Comput ((I +* (J ";" s)),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

Exec ((CurInstr ((I +* (J ";" s)),(Comput ((I +* (J ";" s)),(Initialize P),P2)))),(Comput ((I +* (J ";" s)),(Initialize P),P2))) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)) is set

K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) is set

the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))))

K33( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) is Relation-like set

K32(K33( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))))) is set

K143( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((I +* (J ";" s)),(Comput ((I +* (J ";" s)),(Initialize P),P2))))) is Element of K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))

K143( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((I +* (J ";" s)),(Comput ((I +* (J ";" s)),(Initialize P),P2))))) . (Comput ((I +* (J ";" s)),(Initialize P),P2)) is set

Following ((I +* J),(Comput ((I +* J),(Initialize P),P2))) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

CurInstr ((I +* J),(Comput ((I +* J),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IC (Comput ((I +* J),(Initialize P),P2)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* J),(Initialize P),P2)) . (IC ) is set

(I +* J) /. (IC (Comput ((I +* J),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

Exec ((CurInstr ((I +* J),(Comput ((I +* J),(Initialize P),P2)))),(Comput ((I +* J),(Initialize P),P2))) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

K143( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((I +* J),(Comput ((I +* J),(Initialize P),P2))))) is Element of K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))

K143( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((I +* J),(Comput ((I +* J),(Initialize P),P2))))) . (Comput ((I +* J),(Initialize P),P2)) is set

dom J is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() Element of K32(NAT)

dom (J ";" s) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() Element of K32(NAT)

P2 + 0 is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(I +* J) . (IC (Comput ((I +* J),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

J . (IC (Comput ((I +* J),(Initialize P),P2))) is set

(J ";" s) . (IC (Comput ((I +* J),(Initialize P),P2))) is set

(I +* (J ";" s)) . (IC (Comput ((I +* J),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(I +* (J ";" s)) . (IC (Comput ((I +* (J ";" s)),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

Comput ((I +* J),(Initialize P),0) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

Comput ((I +* (J ";" s)),(Initialize P),0) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() set

card P is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

I is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Directed (P,I) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V28() halt-free set

goto I is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

P +~ ((halt SCM+FSA),(goto I)) is Relation-like Function-like set

card (Directed (P,I)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom (Directed (P,I)) is V28() V119() V120() V121() V122() V123() V124() set

card (dom (Directed (P,I))) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom P is V28() V119() V120() V121() V122() V123() V124() set

card (dom P) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

Directed P is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial halt-free V82( SCM+FSA ) set

card P is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom P is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() set

Directed (P,(card P)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial halt-free set

goto (card P) is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

P +~ ((halt SCM+FSA),(goto (card P))) is Relation-like Function-like set

card (Directed P) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom (Directed P) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() set

P is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

Initialize P is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set

P +* (Start-At (0,SCM+FSA)) is non empty Relation-like the U1 of SCM+FSA -defined the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set

I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set

J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

I +* J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set

LifeSpan ((I +* J),(Initialize P)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Directed J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial halt-free V82( SCM+FSA ) set

card J is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom J is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() set

Directed (J,(card J)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial halt-free set

goto (card J) is non ins-loc-free V78( the InstructionsF of SCM+FSA) V91(3, SCM+FSA ) with_explicit_jumps IC-relocable V143(3, SCM+FSA ) non sequential Element of the InstructionsF of SCM+FSA

J +~ ((halt SCM+FSA),(goto (card J))) is Relation-like Function-like set

I +* (Directed J) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set

dom (I +* (Directed J)) is non empty V119() V120() V121() V122() V123() V124() set

dom (I +* J) is non empty V119() V120() V121() V122() V123() V124() set

dom (Directed J) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() Element of K32(NAT)

dom J is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() Element of K32(NAT)

P2 is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Comput ((I +* J),(Initialize P),P2) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

IC (Comput ((I +* J),(Initialize P),P2)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* J),(Initialize P),P2)) . (IC ) is set

Comput ((I +* (Directed J)),(Initialize P),P2) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

IC (Comput ((I +* (Directed J)),(Initialize P),P2)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* (Directed J)),(Initialize P),P2)) . (IC ) is set

(I +* (Directed J)) /. (IC (Comput ((I +* (Directed J)),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(I +* (Directed J)) . (IC (Comput ((I +* (Directed J)),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

CurInstr ((I +* (Directed J)),(Comput ((I +* (Directed J)),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(I +* (Directed J)) . (IC (Comput ((I +* J),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(Directed J) . (IC (Comput ((I +* J),(Initialize P),P2))) is set

rng (Directed J) is non empty V28() set

P2 is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Comput ((I +* J),(Initialize P),P2) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

Comput ((I +* (Directed J)),(Initialize P),P2) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

P2 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Comput ((I +* (Directed J)),(Initialize P),(P2 + 1)) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

Following ((I +* (Directed J)),(Comput ((I +* (Directed J)),(Initialize P),P2))) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

CurInstr ((I +* (Directed J)),(Comput ((I +* (Directed J)),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IC (Comput ((I +* (Directed J)),(Initialize P),P2)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* (Directed J)),(Initialize P),P2)) . (IC ) is set

(I +* (Directed J)) /. (IC (Comput ((I +* (Directed J)),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

Exec ((CurInstr ((I +* (Directed J)),(Comput ((I +* (Directed J)),(Initialize P),P2)))),(Comput ((I +* (Directed J)),(Initialize P),P2))) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)) is set

K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))) is set

the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))))

K33( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))) is Relation-like set

K32(K33( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))))) is set

K143( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((I +* (Directed J)),(Comput ((I +* (Directed J)),(Initialize P),P2))))) is Element of K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))

K143( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((I +* (Directed J)),(Comput ((I +* (Directed J)),(Initialize P),P2))))) . (Comput ((I +* (Directed J)),(Initialize P),P2)) is set

IC (Comput ((I +* J),(Initialize P),P2)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* J),(Initialize P),P2)) . (IC ) is set

CurInstr ((I +* J),(Comput ((I +* J),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(I +* J) /. (IC (Comput ((I +* J),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(I +* J) . (IC (Comput ((I +* J),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

J . (IC (Comput ((I +* J),(Initialize P),P2))) is set

P2 + 0 is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(I +* (Directed J)) . (IC (Comput ((I +* (Directed J)),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

(Directed J) . (IC (Comput ((I +* J),(Initialize P),P2))) is set

(I +* (Directed J)) . (IC (Comput ((I +* J),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

Comput ((I +* J),(Initialize P),(P2 + 1)) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

Following ((I +* J),(Comput ((I +* J),(Initialize P),P2))) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

Exec ((CurInstr ((I +* J),(Comput ((I +* J),(Initialize P),P2)))),(Comput ((I +* J),(Initialize P),P2))) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

K143( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((I +* J),(Comput ((I +* J),(Initialize P),P2))))) is Element of K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)))

K143( the InstructionsF of SCM+FSA,K141(K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA)),K162(( the Object-Kind of SCM+FSA (#) the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr ((I +* J),(Comput ((I +* J),(Initialize P),P2))))) . (Comput ((I +* J),(Initialize P),P2)) is set

CurInstr ((I +* (Directed J)),(Comput ((I +* (Directed J)),(Initialize P),(P2 + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IC (Comput ((I +* (Directed J)),(Initialize P),(P2 + 1))) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* (Directed J)),(Initialize P),(P2 + 1))) . (IC ) is set

(I +* (Directed J)) /. (IC (Comput ((I +* (Directed J)),(Initialize P),(P2 + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

P2 is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Comput ((I +* J),(Initialize P),P2) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

Comput ((I +* (Directed J)),(Initialize P),P2) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

CurInstr ((I +* (Directed J)),(Comput ((I +* (Directed J)),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IC (Comput ((I +* (Directed J)),(Initialize P),P2)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* (Directed J)),(Initialize P),P2)) . (IC ) is set

(I +* (Directed J)) /. (IC (Comput ((I +* (Directed J)),(Initialize P),P2))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

P2 + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

Comput ((I +* J),(Initialize P),(P2 + 1)) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

Comput ((I +* (Directed J)),(Initialize P),(P2 + 1)) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

CurInstr ((I +* (Directed J)),(Comput ((I +* (Directed J)),(Initialize P),(P2 + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IC (Comput ((I +* (Directed J)),(Initialize P),(P2 + 1))) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* (Directed J)),(Initialize P),(P2 + 1))) . (IC ) is set

(I +* (Directed J)) /. (IC (Comput ((I +* (Directed J)),(Initialize P),(P2 + 1)))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

Comput ((I +* J),(Initialize P),0) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

Comput ((I +* (Directed J)),(Initialize P),0) is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

CurInstr ((I +* (Directed J)),(Comput ((I +* (Directed J)),(Initialize P),0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

IC (Comput ((I +* (Directed J)),(Initialize P),0)) is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

(Comput ((I +* (Directed J)),(Initialize P),0)) . (IC ) is set

(I +* (Directed J)) /. (IC (Comput ((I +* (Directed J)),(Initialize P),0))) is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA

P is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total set

Initialize P is non empty Relation-like the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible total 0 -started set

P +* (Start-At (0,SCM+FSA)) is non empty Relation-like the U1 of SCM+FSA -defined the U1 of SCM+FSA -defined Function-like K274(3,SCM+FSA) -compatible K274(3,SCM+FSA) -compatible total 0 -started set

I is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set

J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial set

Directed J is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like T-Sequence-like V28() initial halt-free V82( SCM+FSA ) set

card J is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT

dom J is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V28() V65() V119() V120() V121() V122() V123() V124() set

Directed (J,(card J)) is Relation-like</