REAL is non empty V2() V32() V79() set
NAT is non empty V2() epsilon-transitive epsilon-connected ordinal V32() countable denumerable V79() Element of K6(REAL)
K6(REAL) is non empty V79() cup-closed diff-closed preBoolean set
SCM+FSA is V58() with_non-empty_values IC-Ins-separated strict V105(3) with_explicit_jumps IC-relocable V161(3) AMI-Struct over 3
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V78() ext-real positive non negative Element of NAT
the U1 of SCM+FSA is non empty set
COMPLEX is non empty V2() V32() V79() set
NAT is non empty V2() epsilon-transitive epsilon-connected ordinal V32() countable denumerable V79() set
K6(NAT) is non empty V79() cup-closed diff-closed preBoolean set
K6(NAT) is non empty V79() cup-closed diff-closed preBoolean set
9 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V78() ext-real positive non negative Element of NAT
Segm 9 is countable Element of K6(NAT)
Int-Locations is non empty set
K236() is set
K6(K236()) is cup-closed diff-closed preBoolean set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V78() ext-real positive non negative Element of NAT
K7(K236(),2) is Relation-like set
K6(K7(K236(),2)) is cup-closed diff-closed preBoolean set
K238() is Relation-like K236() -defined 2 -valued Function-like total V29(K236(),2) Element of K6(K7(K236(),2))
K239() is non empty Relation-like 2 -defined Function-like total set
K238() (#) K239() is Relation-like K236() -defined Function-like total set
product (K238() (#) K239()) is functional with_common_domain product-like set
K230() is non empty set
K127((product (K238() (#) K239())),(product (K238() (#) K239()))) is non empty functional set
K7(K230(),K127((product (K238() (#) K239())),(product (K238() (#) K239())))) is Relation-like set
K6(K7(K230(),K127((product (K238() (#) K239())),(product (K238() (#) K239()))))) is cup-closed diff-closed preBoolean set
K6( the U1 of SCM+FSA) is non empty V79() cup-closed diff-closed preBoolean set
the InstructionsF of SCM+FSA is non empty Relation-like standard-ins V87() J/A-independent V90() set
INT is non empty V2() V32() V79() set
the_Values_of 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 non empty Relation-like the U1 of SCM+FSA -defined 3 -valued Function-like total V29( the U1 of SCM+FSA,3) Element of K6(K7( the U1 of SCM+FSA,3))
K7( the U1 of SCM+FSA,3) is Relation-like set
K6(K7( the U1 of SCM+FSA,3)) is cup-closed diff-closed preBoolean set
the ValuesF of SCM+FSA is non empty Relation-like 3 -defined Function-like total set
the Object-Kind of SCM+FSA (#) the ValuesF of SCM+FSA is non empty Relation-like the U1 of SCM+FSA -defined Function-like total set
Int-Locations is non empty Element of K6( the U1 of SCM+FSA)
K6(Int-Locations) is non empty V79() cup-closed diff-closed preBoolean set
K7(NAT,K6(NAT)) is Relation-like set
K6(K7(NAT,K6(NAT))) is cup-closed diff-closed preBoolean set
FinPartSt SCM+FSA is non empty functional Element of K6((sproduct (the_Values_of SCM+FSA)))
sproduct (the_Values_of SCM+FSA) is non empty functional set
K6((sproduct (the_Values_of SCM+FSA))) is non empty V79() cup-closed diff-closed preBoolean set
{ b1 where b1 is Relation-like the U1 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible Element of sproduct (the_Values_of SCM+FSA) : b1 is V32() } is set
K7((FinPartSt SCM+FSA),(FinPartSt SCM+FSA)) is Relation-like set
K6(K7((FinPartSt SCM+FSA),(FinPartSt SCM+FSA))) is cup-closed diff-closed preBoolean set
product (the_Values_of SCM+FSA) is non empty functional with_common_domain product-like set
K7(NAT,(product (the_Values_of SCM+FSA))) is Relation-like set
K6(K7(NAT,(product (the_Values_of SCM+FSA)))) is cup-closed diff-closed preBoolean set
RAT is non empty V2() V32() V79() set
K548() is V58() with_non-empty_values IC-Ins-separated strict strict V105(2) AMI-Struct over 2
the InstructionsF of K548() is non empty Relation-like standard-ins V87() J/A-independent V90() set
the U1 of K548() is non empty set
the_Values_of K548() is non empty Relation-like non-empty non empty-yielding the U1 of K548() -defined Function-like total set
the Object-Kind of K548() is non empty Relation-like the U1 of K548() -defined 2 -valued Function-like total V29( the U1 of K548(),2) Element of K6(K7( the U1 of K548(),2))
K7( the U1 of K548(),2) is Relation-like set
K6(K7( the U1 of K548(),2)) is cup-closed diff-closed preBoolean set
the ValuesF of K548() is non empty Relation-like 2 -defined Function-like total set
the Object-Kind of K548() (#) the ValuesF of K548() is non empty Relation-like the U1 of K548() -defined Function-like total set
Fin Int-Locations is non empty cup-closed diff-closed preBoolean set
FinSeq-Locations is non empty V2() V32() V79() Element of K6( the U1 of SCM+FSA)
Fin FinSeq-Locations is non empty cup-closed diff-closed preBoolean set
K6(FinSeq-Locations) is non empty V79() cup-closed diff-closed preBoolean set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V78() ext-real positive non negative Element of NAT
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V36() V40() V41() V42() Function-yielding V52() Cardinal-yielding countable V85() ext-real non positive non negative set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() V12() integer Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V32() V33() V36() V40() V41() V42() Function-yielding V52() Cardinal-yielding countable V85() ext-real non positive non negative Element of NAT
Fusc 0 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Fusc 1 is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
IC is V65( SCM+FSA ) Element of the U1 of SCM+FSA
halt SCM+FSA is ins-loc-free V104(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V160(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
intloc 0 is V77() read-only Element of the U1 of SCM+FSA
UsedIntLoc (halt SCM+FSA) is V32() countable Element of Fin Int-Locations
K7( the InstructionsF of SCM+FSA,(Fin Int-Locations)) is Relation-like set
K6(K7( the InstructionsF of SCM+FSA,(Fin Int-Locations))) is cup-closed diff-closed preBoolean set
K7( the InstructionsF of SCM+FSA,(Fin FinSeq-Locations)) is Relation-like set
K6(K7( the InstructionsF of SCM+FSA,(Fin FinSeq-Locations))) is cup-closed diff-closed preBoolean set
Stop SCM+FSA is non empty V2() T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like constant V32() countable V85() non halt-free V94( SCM+FSA ) V95( SCM+FSA ) keeping_0 good V163(3, SCM+FSA ) paraclosed parahalting set
K292((halt SCM+FSA)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() 1 -element countable V85() set
0 .--> (halt SCM+FSA) is V2() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V32() countable set
{0} is non empty functional V32() V36() with_common_domain countable set
{0} --> (halt SCM+FSA) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {(halt SCM+FSA)} -valued Function-like constant total V29({0},{(halt SCM+FSA)}) V32() countable Element of K6(K7({0},{(halt SCM+FSA)}))
{(halt SCM+FSA)} is non empty V32() countable set
K7({0},{(halt SCM+FSA)}) is Relation-like V32() countable set
K6(K7({0},{(halt SCM+FSA)})) is V32() V36() countable cup-closed diff-closed preBoolean set
Goto 0 is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() halt-free V95( SCM+FSA ) good set
6 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V78() ext-real positive non negative Element of NAT
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V78() ext-real positive non negative Element of NAT
goto 0 is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
goto 2 is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
5 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V78() ext-real positive non negative Element of NAT
goto 3 is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
Start-At (0,SCM+FSA) is non empty Relation-like the U1 of SCM+FSA -defined Function-like the_Values_of SCM+FSA -compatible V32() countable 0 -started set
(IC ) .--> 0 is V2() Relation-like the U1 of SCM+FSA -defined {(IC )} -defined NAT -valued Function-like one-to-one constant V32() Function-yielding V52() countable set
{(IC )} is non empty V32() countable set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued {0} -valued Function-like constant total V29({(IC )},{0}) V32() Function-yielding V52() countable Element of K6(K7({(IC )},{0}))
K7({(IC )},{0}) is Relation-like V32() countable set
K6(K7({(IC )},{0})) is V32() V36() countable cup-closed diff-closed preBoolean set
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V78() ext-real positive non negative Element of NAT
D is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
SAt is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D .--> SAt is V2() Relation-like NAT -defined {D} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V32() countable set
{D} is non empty V32() countable set
{D} --> SAt is non empty Relation-like {D} -defined the InstructionsF of SCM+FSA -valued {SAt} -valued Function-like constant total V29({D},{SAt}) V32() countable Element of K6(K7({D},{SAt}))
{SAt} is non empty V32() countable set
K7({D},{SAt}) is Relation-like V32() countable set
K6(K7({D},{SAt})) is V32() V36() countable cup-closed diff-closed preBoolean set
UsedIntLoc (D .--> SAt) is V32() countable Element of K6(Int-Locations)
UsedIntLoc SAt is V32() countable Element of Fin Int-Locations
s is non empty Relation-like the InstructionsF of SCM+FSA -defined Fin Int-Locations -valued Function-like total V29( the InstructionsF of SCM+FSA, Fin Int-Locations) Element of K6(K7( the InstructionsF of SCM+FSA,(Fin Int-Locations)))
(D .--> SAt) (#) s is Relation-like NAT -defined Fin Int-Locations -valued Function-like V32() countable set
Union ((D .--> SAt) (#) s) is set
dom s is non empty set
{D} --> SAt is non empty Relation-like {D} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V29({D}, the InstructionsF of SCM+FSA) V32() countable Element of K6(K7({D}, the InstructionsF of SCM+FSA))
K7({D}, the InstructionsF of SCM+FSA) is Relation-like set
K6(K7({D}, the InstructionsF of SCM+FSA)) is cup-closed diff-closed preBoolean set
s * ({D} --> SAt) is non empty Relation-like {D} -defined Fin Int-Locations -valued Function-like total V29({D}, Fin Int-Locations) V32() countable Element of K6(K7({D},(Fin Int-Locations)))
K7({D},(Fin Int-Locations)) is Relation-like set
K6(K7({D},(Fin Int-Locations))) is cup-closed diff-closed preBoolean set
rng (s * ({D} --> SAt)) is non empty V32() countable set
union (rng (s * ({D} --> SAt))) is set
s . SAt is V32() countable Element of Fin Int-Locations
{D} --> (s . SAt) is non empty Relation-like {D} -defined Fin Int-Locations -valued Function-like constant total V29({D}, Fin Int-Locations) V32() countable Element of K6(K7({D},(Fin Int-Locations)))
{(s . SAt)} is non empty V32() V36() countable set
K7({D},{(s . SAt)}) is Relation-like V32() countable set
rng ({D} --> (s . SAt)) is non empty V2() V32() countable set
union (rng ({D} --> (s . SAt))) is set
union {(s . SAt)} is V32() countable set
{(UsedIntLoc SAt)} is non empty V32() V36() countable set
union {(UsedIntLoc SAt)} is V32() countable set
D is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
SAt is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
D .--> SAt is V2() Relation-like NAT -defined {D} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V32() countable set
{D} is non empty V32() countable set
{D} --> SAt is non empty Relation-like {D} -defined the InstructionsF of SCM+FSA -valued {SAt} -valued Function-like constant total V29({D},{SAt}) V32() countable Element of K6(K7({D},{SAt}))
{SAt} is non empty V32() countable set
K7({D},{SAt}) is Relation-like V32() countable set
K6(K7({D},{SAt})) is V32() V36() countable cup-closed diff-closed preBoolean set
UsedInt*Loc (D .--> SAt) is V32() countable Element of K6(FinSeq-Locations)
UsedInt*Loc SAt is V32() countable Element of Fin FinSeq-Locations
s is non empty Relation-like the InstructionsF of SCM+FSA -defined Fin FinSeq-Locations -valued Function-like total V29( the InstructionsF of SCM+FSA, Fin FinSeq-Locations) Element of K6(K7( the InstructionsF of SCM+FSA,(Fin FinSeq-Locations)))
(D .--> SAt) (#) s is Relation-like NAT -defined Fin FinSeq-Locations -valued Function-like V32() countable set
Union ((D .--> SAt) (#) s) is set
dom s is non empty set
{D} --> SAt is non empty Relation-like {D} -defined the InstructionsF of SCM+FSA -valued Function-like constant total V29({D}, the InstructionsF of SCM+FSA) V32() countable Element of K6(K7({D}, the InstructionsF of SCM+FSA))
K7({D}, the InstructionsF of SCM+FSA) is Relation-like set
K6(K7({D}, the InstructionsF of SCM+FSA)) is cup-closed diff-closed preBoolean set
s * ({D} --> SAt) is non empty Relation-like {D} -defined Fin FinSeq-Locations -valued Function-like total V29({D}, Fin FinSeq-Locations) V32() countable Element of K6(K7({D},(Fin FinSeq-Locations)))
K7({D},(Fin FinSeq-Locations)) is Relation-like set
K6(K7({D},(Fin FinSeq-Locations))) is cup-closed diff-closed preBoolean set
rng (s * ({D} --> SAt)) is non empty V32() countable set
union (rng (s * ({D} --> SAt))) is set
s . SAt is V32() countable Element of Fin FinSeq-Locations
{D} --> (s . SAt) is non empty Relation-like {D} -defined Fin FinSeq-Locations -valued Function-like constant total V29({D}, Fin FinSeq-Locations) V32() countable Element of K6(K7({D},(Fin FinSeq-Locations)))
{(s . SAt)} is non empty V32() V36() countable set
K7({D},{(s . SAt)}) is Relation-like V32() countable set
rng ({D} --> (s . SAt)) is non empty V2() V32() countable set
union (rng ({D} --> (s . SAt))) is set
union {(s . SAt)} is V32() countable set
{(UsedInt*Loc SAt)} is non empty V32() V36() countable set
union {(UsedInt*Loc SAt)} is V32() countable set
UsedIntLoc (Stop SCM+FSA) is V32() countable Element of K6(Int-Locations)
UsedInt*Loc (Stop SCM+FSA) is V32() countable Element of K6(FinSeq-Locations)
UsedInt*Loc (halt SCM+FSA) is V32() countable Element of Fin FinSeq-Locations
D is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Goto D is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() halt-free V95( SCM+FSA ) good set
UsedIntLoc (Goto D) is V32() countable Element of K6(Int-Locations)
goto D is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
0 .--> (goto D) is V2() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V32() countable set
{0} --> (goto D) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {(goto D)} -valued Function-like constant total V29({0},{(goto D)}) V32() countable Element of K6(K7({0},{(goto D)}))
{(goto D)} is non empty V32() countable set
K7({0},{(goto D)}) is Relation-like V32() countable set
K6(K7({0},{(goto D)})) is V32() V36() countable cup-closed diff-closed preBoolean set
UsedIntLoc (goto D) is V32() countable Element of Fin Int-Locations
D is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
Goto D is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() halt-free V95( SCM+FSA ) good set
UsedInt*Loc (Goto D) is V32() countable Element of K6(FinSeq-Locations)
goto D is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
0 .--> (goto D) is V2() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V32() countable set
{0} --> (goto D) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {(goto D)} -valued Function-like constant total V29({0},{(goto D)}) V32() countable Element of K6(K7({0},{(goto D)}))
{(goto D)} is non empty V32() countable set
K7({0},{(goto D)}) is Relation-like V32() countable set
K6(K7({0},{(goto D)})) is V32() V36() countable cup-closed diff-closed preBoolean set
UsedInt*Loc (goto D) is V32() countable Element of Fin FinSeq-Locations
Int-Locations \/ FinSeq-Locations is non empty Element of K6( the U1 of SCM+FSA)
p is V77() Element of the U1 of SCM+FSA
{p} is non empty V32() countable Element of K6(Int-Locations)
s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
UsedIntLoc s is V32() countable Element of K6(Int-Locations)
{p} \/ (UsedIntLoc s) is non empty V32() countable Element of K6(Int-Locations)
N is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
if=0 (p,s,N) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() non halt-free set
UsedIntLoc (if=0 (p,s,N)) is V32() countable Element of K6(Int-Locations)
UsedIntLoc N is V32() countable Element of K6(Int-Locations)
({p} \/ (UsedIntLoc s)) \/ (UsedIntLoc N) is non empty V32() countable Element of K6(Int-Locations)
card N is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom N is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable V78() ext-real positive non negative V140() set
(card N) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V78() ext-real positive non negative Element of NAT
p =0_goto ((card N) + 3) is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
card s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom s is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable V78() ext-real positive non negative V140() set
(card s) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V78() ext-real positive non negative Element of NAT
Goto ((card s) + 1) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() halt-free V95( SCM+FSA ) good set
(p =0_goto ((card N) + 3)) ";" N is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Macro (p =0_goto ((card N) + 3)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() good set
K320(SCM+FSA,(p =0_goto ((card N) + 3))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like V32() 1 -element countable V85() set
0 .--> (p =0_goto ((card N) + 3)) is V2() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V32() countable set
{0} --> (p =0_goto ((card N) + 3)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {(p =0_goto ((card N) + 3))} -valued Function-like constant total V29({0},{(p =0_goto ((card N) + 3))}) V32() countable Element of K6(K7({0},{(p =0_goto ((card N) + 3))}))
{(p =0_goto ((card N) + 3))} is non empty V32() countable set
K7({0},{(p =0_goto ((card N) + 3))}) is Relation-like V32() countable set
K6(K7({0},{(p =0_goto ((card N) + 3))})) is V32() V36() countable cup-closed diff-closed preBoolean set
stop K320(SCM+FSA,(p =0_goto ((card N) + 3))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
K282(K320(SCM+FSA,(p =0_goto ((card N) + 3))),(Stop SCM+FSA)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
(Macro (p =0_goto ((card N) + 3))) ";" N is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
stop (Macro (p =0_goto ((card N) + 3))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
K282((Macro (p =0_goto ((card N) + 3))),(Stop SCM+FSA)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
CutLastLoc (stop (Macro (p =0_goto ((card N) + 3)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Directed (CutLastLoc (stop (Macro (p =0_goto ((card N) + 3))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
card (CutLastLoc (stop (Macro (p =0_goto ((card N) + 3))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (CutLastLoc (stop (Macro (p =0_goto ((card N) + 3))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable ext-real non negative V140() set
Directed ((CutLastLoc (stop (Macro (p =0_goto ((card N) + 3))))),(card (CutLastLoc (stop (Macro (p =0_goto ((card N) + 3))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
goto (card (CutLastLoc (stop (Macro (p =0_goto ((card N) + 3)))))) is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(CutLastLoc (stop (Macro (p =0_goto ((card N) + 3))))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro (p =0_goto ((card N) + 3)))))))) is Relation-like Function-like set
card (Macro (p =0_goto ((card N) + 3))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (Macro (p =0_goto ((card N) + 3))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable V78() ext-real positive non negative V140() set
Reloc (N,(card (Macro (p =0_goto ((card N) + 3))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
IncAddr (N,(card (Macro (p =0_goto ((card N) + 3))))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Shift ((IncAddr (N,(card (Macro (p =0_goto ((card N) + 3)))))),(card (Macro (p =0_goto ((card N) + 3))))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
(Directed (CutLastLoc (stop (Macro (p =0_goto ((card N) + 3)))))) +* (Reloc (N,(card (Macro (p =0_goto ((card N) + 3)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
stop ((p =0_goto ((card N) + 3)) ";" N) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
K282(((p =0_goto ((card N) + 3)) ";" N),(Stop SCM+FSA)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
CutLastLoc (stop ((p =0_goto ((card N) + 3)) ";" N)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Directed (CutLastLoc (stop ((p =0_goto ((card N) + 3)) ";" N))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
card (CutLastLoc (stop ((p =0_goto ((card N) + 3)) ";" N))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (CutLastLoc (stop ((p =0_goto ((card N) + 3)) ";" N))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable ext-real non negative V140() set
Directed ((CutLastLoc (stop ((p =0_goto ((card N) + 3)) ";" N))),(card (CutLastLoc (stop ((p =0_goto ((card N) + 3)) ";" N))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
goto (card (CutLastLoc (stop ((p =0_goto ((card N) + 3)) ";" N)))) is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(CutLastLoc (stop ((p =0_goto ((card N) + 3)) ";" N))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop ((p =0_goto ((card N) + 3)) ";" N)))))) is Relation-like Function-like set
card ((p =0_goto ((card N) + 3)) ";" N) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((p =0_goto ((card N) + 3)) ";" N) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable V78() ext-real positive non negative V140() set
Reloc ((Goto ((card s) + 1)),(card ((p =0_goto ((card N) + 3)) ";" N))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
IncAddr ((Goto ((card s) + 1)),(card ((p =0_goto ((card N) + 3)) ";" N))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Shift ((IncAddr ((Goto ((card s) + 1)),(card ((p =0_goto ((card N) + 3)) ";" N)))),(card ((p =0_goto ((card N) + 3)) ";" N))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
(Directed (CutLastLoc (stop ((p =0_goto ((card N) + 3)) ";" N)))) +* (Reloc ((Goto ((card s) + 1)),(card ((p =0_goto ((card N) + 3)) ";" N)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
(((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
stop (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
K282((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))),(Stop SCM+FSA)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
CutLastLoc (stop (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Directed (CutLastLoc (stop (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
card (CutLastLoc (stop (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (CutLastLoc (stop (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable ext-real non negative V140() set
Directed ((CutLastLoc (stop (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))))),(card (CutLastLoc (stop (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
goto (card (CutLastLoc (stop (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1)))))) is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(CutLastLoc (stop (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1)))))))) is Relation-like Function-like set
card (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable V78() ext-real positive non negative V140() set
Reloc (s,(card (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
IncAddr (s,(card (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Shift ((IncAddr (s,(card (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1)))))),(card (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
(Directed (CutLastLoc (stop (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1)))))) +* (Reloc (s,(card (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s) ";" (Stop SCM+FSA) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() non halt-free set
stop ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
K282(((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s),(Stop SCM+FSA)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
CutLastLoc (stop ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Directed (CutLastLoc (stop ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
card (CutLastLoc (stop ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (CutLastLoc (stop ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable ext-real non negative V140() set
Directed ((CutLastLoc (stop ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s))),(card (CutLastLoc (stop ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
goto (card (CutLastLoc (stop ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s)))) is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(CutLastLoc (stop ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s)))))) is Relation-like Function-like set
card ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable V78() ext-real positive non negative V140() set
Reloc ((Stop SCM+FSA),(card ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable non halt-free set
IncAddr ((Stop SCM+FSA),(card ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Shift ((IncAddr ((Stop SCM+FSA),(card ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s)))),(card ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
(Directed (CutLastLoc (stop ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s)))) +* (Reloc ((Stop SCM+FSA),(card ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like V32() countable non halt-free set
UsedIntLoc (((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s) ";" (Stop SCM+FSA)) is V32() countable Element of K6(Int-Locations)
UsedIntLoc ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s) is V32() countable Element of K6(Int-Locations)
(UsedIntLoc ((((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) ";" s)) \/ {} is V32() countable set
UsedIntLoc (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1))) is V32() countable Element of K6(Int-Locations)
(UsedIntLoc (((p =0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1)))) \/ (UsedIntLoc s) is V32() countable Element of K6(Int-Locations)
UsedIntLoc ((p =0_goto ((card N) + 3)) ";" N) is V32() countable Element of K6(Int-Locations)
UsedIntLoc (Goto ((card s) + 1)) is V32() countable Element of K6(Int-Locations)
(UsedIntLoc ((p =0_goto ((card N) + 3)) ";" N)) \/ (UsedIntLoc (Goto ((card s) + 1))) is V32() countable Element of K6(Int-Locations)
((UsedIntLoc ((p =0_goto ((card N) + 3)) ";" N)) \/ (UsedIntLoc (Goto ((card s) + 1)))) \/ (UsedIntLoc s) is V32() countable Element of K6(Int-Locations)
(UsedIntLoc ((p =0_goto ((card N) + 3)) ";" N)) \/ {} is V32() countable set
((UsedIntLoc ((p =0_goto ((card N) + 3)) ";" N)) \/ {}) \/ (UsedIntLoc s) is V32() countable set
UsedIntLoc (p =0_goto ((card N) + 3)) is V32() countable Element of Fin Int-Locations
(UsedIntLoc (p =0_goto ((card N) + 3))) \/ (UsedIntLoc N) is V32() countable set
((UsedIntLoc (p =0_goto ((card N) + 3))) \/ (UsedIntLoc N)) \/ (UsedIntLoc s) is V32() countable set
{p} \/ (UsedIntLoc N) is non empty V32() countable Element of K6(Int-Locations)
({p} \/ (UsedIntLoc N)) \/ (UsedIntLoc s) is non empty V32() countable Element of K6(Int-Locations)
p is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
UsedInt*Loc p is V32() countable Element of K6(FinSeq-Locations)
s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
UsedInt*Loc s is V32() countable Element of K6(FinSeq-Locations)
(UsedInt*Loc p) \/ (UsedInt*Loc s) is V32() countable Element of K6(FinSeq-Locations)
result is V77() Element of the U1 of SCM+FSA
if=0 (result,p,s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() non halt-free set
UsedInt*Loc (if=0 (result,p,s)) is V32() countable Element of K6(FinSeq-Locations)
card s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom s is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable V78() ext-real positive non negative V140() set
(card s) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V78() ext-real positive non negative Element of NAT
result =0_goto ((card s) + 3) is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
card p is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom p is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable V78() ext-real positive non negative V140() set
(card p) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V78() ext-real positive non negative Element of NAT
Goto ((card p) + 1) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() halt-free V95( SCM+FSA ) good set
(result =0_goto ((card s) + 3)) ";" s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Macro (result =0_goto ((card s) + 3)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() good set
K320(SCM+FSA,(result =0_goto ((card s) + 3))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like V32() 1 -element countable V85() set
0 .--> (result =0_goto ((card s) + 3)) is V2() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V32() countable set
{0} --> (result =0_goto ((card s) + 3)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {(result =0_goto ((card s) + 3))} -valued Function-like constant total V29({0},{(result =0_goto ((card s) + 3))}) V32() countable Element of K6(K7({0},{(result =0_goto ((card s) + 3))}))
{(result =0_goto ((card s) + 3))} is non empty V32() countable set
K7({0},{(result =0_goto ((card s) + 3))}) is Relation-like V32() countable set
K6(K7({0},{(result =0_goto ((card s) + 3))})) is V32() V36() countable cup-closed diff-closed preBoolean set
stop K320(SCM+FSA,(result =0_goto ((card s) + 3))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
K282(K320(SCM+FSA,(result =0_goto ((card s) + 3))),(Stop SCM+FSA)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
(Macro (result =0_goto ((card s) + 3))) ";" s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
stop (Macro (result =0_goto ((card s) + 3))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
K282((Macro (result =0_goto ((card s) + 3))),(Stop SCM+FSA)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
CutLastLoc (stop (Macro (result =0_goto ((card s) + 3)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Directed (CutLastLoc (stop (Macro (result =0_goto ((card s) + 3))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
card (CutLastLoc (stop (Macro (result =0_goto ((card s) + 3))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (CutLastLoc (stop (Macro (result =0_goto ((card s) + 3))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable ext-real non negative V140() set
Directed ((CutLastLoc (stop (Macro (result =0_goto ((card s) + 3))))),(card (CutLastLoc (stop (Macro (result =0_goto ((card s) + 3))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
goto (card (CutLastLoc (stop (Macro (result =0_goto ((card s) + 3)))))) is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(CutLastLoc (stop (Macro (result =0_goto ((card s) + 3))))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro (result =0_goto ((card s) + 3)))))))) is Relation-like Function-like set
card (Macro (result =0_goto ((card s) + 3))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (Macro (result =0_goto ((card s) + 3))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable V78() ext-real positive non negative V140() set
Reloc (s,(card (Macro (result =0_goto ((card s) + 3))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
IncAddr (s,(card (Macro (result =0_goto ((card s) + 3))))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Shift ((IncAddr (s,(card (Macro (result =0_goto ((card s) + 3)))))),(card (Macro (result =0_goto ((card s) + 3))))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
(Directed (CutLastLoc (stop (Macro (result =0_goto ((card s) + 3)))))) +* (Reloc (s,(card (Macro (result =0_goto ((card s) + 3)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
stop ((result =0_goto ((card s) + 3)) ";" s) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
K282(((result =0_goto ((card s) + 3)) ";" s),(Stop SCM+FSA)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
CutLastLoc (stop ((result =0_goto ((card s) + 3)) ";" s)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Directed (CutLastLoc (stop ((result =0_goto ((card s) + 3)) ";" s))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
card (CutLastLoc (stop ((result =0_goto ((card s) + 3)) ";" s))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (CutLastLoc (stop ((result =0_goto ((card s) + 3)) ";" s))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable ext-real non negative V140() set
Directed ((CutLastLoc (stop ((result =0_goto ((card s) + 3)) ";" s))),(card (CutLastLoc (stop ((result =0_goto ((card s) + 3)) ";" s))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
goto (card (CutLastLoc (stop ((result =0_goto ((card s) + 3)) ";" s)))) is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(CutLastLoc (stop ((result =0_goto ((card s) + 3)) ";" s))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop ((result =0_goto ((card s) + 3)) ";" s)))))) is Relation-like Function-like set
card ((result =0_goto ((card s) + 3)) ";" s) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((result =0_goto ((card s) + 3)) ";" s) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable V78() ext-real positive non negative V140() set
Reloc ((Goto ((card p) + 1)),(card ((result =0_goto ((card s) + 3)) ";" s))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
IncAddr ((Goto ((card p) + 1)),(card ((result =0_goto ((card s) + 3)) ";" s))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Shift ((IncAddr ((Goto ((card p) + 1)),(card ((result =0_goto ((card s) + 3)) ";" s)))),(card ((result =0_goto ((card s) + 3)) ";" s))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
(Directed (CutLastLoc (stop ((result =0_goto ((card s) + 3)) ";" s)))) +* (Reloc ((Goto ((card p) + 1)),(card ((result =0_goto ((card s) + 3)) ";" s)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
(((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
stop (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
K282((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))),(Stop SCM+FSA)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
CutLastLoc (stop (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Directed (CutLastLoc (stop (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
card (CutLastLoc (stop (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (CutLastLoc (stop (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable ext-real non negative V140() set
Directed ((CutLastLoc (stop (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))))),(card (CutLastLoc (stop (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
goto (card (CutLastLoc (stop (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1)))))) is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(CutLastLoc (stop (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1)))))))) is Relation-like Function-like set
card (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable V78() ext-real positive non negative V140() set
Reloc (p,(card (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
IncAddr (p,(card (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Shift ((IncAddr (p,(card (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1)))))),(card (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
(Directed (CutLastLoc (stop (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1)))))) +* (Reloc (p,(card (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p) ";" (Stop SCM+FSA) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() non halt-free set
stop ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
K282(((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p),(Stop SCM+FSA)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
CutLastLoc (stop ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Directed (CutLastLoc (stop ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
card (CutLastLoc (stop ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (CutLastLoc (stop ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable ext-real non negative V140() set
Directed ((CutLastLoc (stop ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p))),(card (CutLastLoc (stop ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
goto (card (CutLastLoc (stop ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p)))) is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(CutLastLoc (stop ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p)))))) is Relation-like Function-like set
card ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable V78() ext-real positive non negative V140() set
Reloc ((Stop SCM+FSA),(card ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable non halt-free set
IncAddr ((Stop SCM+FSA),(card ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Shift ((IncAddr ((Stop SCM+FSA),(card ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p)))),(card ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
(Directed (CutLastLoc (stop ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p)))) +* (Reloc ((Stop SCM+FSA),(card ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like V32() countable non halt-free set
UsedInt*Loc (((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p) ";" (Stop SCM+FSA)) is V32() countable Element of K6(FinSeq-Locations)
UsedInt*Loc ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p) is V32() countable Element of K6(FinSeq-Locations)
(UsedInt*Loc ((((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) ";" p)) \/ {} is V32() countable set
UsedInt*Loc (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1))) is V32() countable Element of K6(FinSeq-Locations)
(UsedInt*Loc (((result =0_goto ((card s) + 3)) ";" s) ";" (Goto ((card p) + 1)))) \/ (UsedInt*Loc p) is V32() countable Element of K6(FinSeq-Locations)
UsedInt*Loc ((result =0_goto ((card s) + 3)) ";" s) is V32() countable Element of K6(FinSeq-Locations)
UsedInt*Loc (Goto ((card p) + 1)) is V32() countable Element of K6(FinSeq-Locations)
(UsedInt*Loc ((result =0_goto ((card s) + 3)) ";" s)) \/ (UsedInt*Loc (Goto ((card p) + 1))) is V32() countable Element of K6(FinSeq-Locations)
((UsedInt*Loc ((result =0_goto ((card s) + 3)) ";" s)) \/ (UsedInt*Loc (Goto ((card p) + 1)))) \/ (UsedInt*Loc p) is V32() countable Element of K6(FinSeq-Locations)
(UsedInt*Loc ((result =0_goto ((card s) + 3)) ";" s)) \/ {} is V32() countable set
((UsedInt*Loc ((result =0_goto ((card s) + 3)) ";" s)) \/ {}) \/ (UsedInt*Loc p) is V32() countable set
UsedInt*Loc (result =0_goto ((card s) + 3)) is V32() countable Element of Fin FinSeq-Locations
(UsedInt*Loc (result =0_goto ((card s) + 3))) \/ (UsedInt*Loc s) is V32() countable set
((UsedInt*Loc (result =0_goto ((card s) + 3))) \/ (UsedInt*Loc s)) \/ (UsedInt*Loc p) is V32() countable set
{} \/ (UsedInt*Loc s) is V32() countable set
({} \/ (UsedInt*Loc s)) \/ (UsedInt*Loc p) is V32() countable set
p is V77() Element of the U1 of SCM+FSA
{p} is non empty V32() countable Element of K6(Int-Locations)
s is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
UsedIntLoc s is V32() countable Element of K6(Int-Locations)
{p} \/ (UsedIntLoc s) is non empty V32() countable Element of K6(Int-Locations)
N is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
if>0 (p,s,N) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() non halt-free set
UsedIntLoc (if>0 (p,s,N)) is V32() countable Element of K6(Int-Locations)
UsedIntLoc N is V32() countable Element of K6(Int-Locations)
({p} \/ (UsedIntLoc s)) \/ (UsedIntLoc N) is non empty V32() countable Element of K6(Int-Locations)
card N is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom N is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable V78() ext-real positive non negative V140() set
(card N) + 3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V78() ext-real positive non negative Element of NAT
p >0_goto ((card N) + 3) is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
card s is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom s is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable V78() ext-real positive non negative V140() set
(card s) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V78() ext-real positive non negative Element of NAT
Goto ((card s) + 1) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() halt-free V95( SCM+FSA ) good set
(p >0_goto ((card N) + 3)) ";" N is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Macro (p >0_goto ((card N) + 3)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() good set
K320(SCM+FSA,(p >0_goto ((card N) + 3))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like V32() 1 -element countable V85() set
0 .--> (p >0_goto ((card N) + 3)) is V2() Relation-like NAT -defined {0} -defined the InstructionsF of SCM+FSA -valued Function-like one-to-one constant V32() countable set
{0} --> (p >0_goto ((card N) + 3)) is non empty Relation-like {0} -defined the InstructionsF of SCM+FSA -valued {(p >0_goto ((card N) + 3))} -valued Function-like constant total V29({0},{(p >0_goto ((card N) + 3))}) V32() countable Element of K6(K7({0},{(p >0_goto ((card N) + 3))}))
{(p >0_goto ((card N) + 3))} is non empty V32() countable set
K7({0},{(p >0_goto ((card N) + 3))}) is Relation-like V32() countable set
K6(K7({0},{(p >0_goto ((card N) + 3))})) is V32() V36() countable cup-closed diff-closed preBoolean set
stop K320(SCM+FSA,(p >0_goto ((card N) + 3))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
K282(K320(SCM+FSA,(p >0_goto ((card N) + 3))),(Stop SCM+FSA)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
(Macro (p >0_goto ((card N) + 3))) ";" N is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
stop (Macro (p >0_goto ((card N) + 3))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
K282((Macro (p >0_goto ((card N) + 3))),(Stop SCM+FSA)) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
CutLastLoc (stop (Macro (p >0_goto ((card N) + 3)))) is T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Directed (CutLastLoc (stop (Macro (p >0_goto ((card N) + 3))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
card (CutLastLoc (stop (Macro (p >0_goto ((card N) + 3))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (CutLastLoc (stop (Macro (p >0_goto ((card N) + 3))))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable ext-real non negative V140() set
Directed ((CutLastLoc (stop (Macro (p >0_goto ((card N) + 3))))),(card (CutLastLoc (stop (Macro (p >0_goto ((card N) + 3))))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable halt-free set
goto (card (CutLastLoc (stop (Macro (p >0_goto ((card N) + 3)))))) is non ins-loc-free V91( the InstructionsF of SCM+FSA) V104(3, SCM+FSA ) good with_explicit_jumps IC-relocable V160(3, SCM+FSA ) V162(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(CutLastLoc (stop (Macro (p >0_goto ((card N) + 3))))) +~ ((halt SCM+FSA),(goto (card (CutLastLoc (stop (Macro (p >0_goto ((card N) + 3)))))))) is Relation-like Function-like set
card (Macro (p >0_goto ((card N) + 3))) is epsilon-transitive epsilon-connected ordinal natural V11() V12() integer ext-real non negative Element of NAT
dom (Macro (p >0_goto ((card N) + 3))) is non empty epsilon-transitive epsilon-connected ordinal natural V11() V12() integer V32() countable V78() ext-real positive non negative V140() set
Reloc (N,(card (Macro (p >0_goto ((card N) + 3))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
IncAddr (N,(card (Macro (p >0_goto ((card N) + 3))))) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
Shift ((IncAddr (N,(card (Macro (p >0_goto ((card N) + 3)))))),(card (Macro (p >0_goto ((card N) + 3))))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
(Directed (CutLastLoc (stop (Macro (p >0_goto ((card N) + 3)))))) +* (Reloc (N,(card (Macro (p >0_goto ((card N) + 3)))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable set
((p >0_goto ((card N) + 3)) ";" N) ";" (Goto ((card s) + 1)) is non empty T-Sequence-like Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V32() countable V85() set
stop