:: 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₁ where b₁ is Element of K166(K274(3,SCM+FSA)) : b₁ is V28() } is set
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₁ + I) where b₁ is ext-real epsilon-transitive epsilon-connected ordinal natural V27() V63() V107() V108() V119() V120() V121() V122() V123() V124() Element of NAT : b₁ in dom (IncAddr (P,I)) } is set
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</