:: SCMFSA9A semantic presentation

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

{ b

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