:: COMPOS_2 semantic presentation

REAL is set
NAT is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool REAL
bool REAL is set
omega is non empty epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set
bool omega is non finite set
bool NAT is non finite set
COMPLEX is set
RAT is set
INT is set
{} is empty Relation-like non-empty empty-yielding RAT -valued functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite cardinal {} -element V39() V41() V94() complex ext-real non negative complex-valued ext-real-valued real-valued natural-valued set
2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real positive non negative Element of NAT
1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real positive non negative Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real positive non negative Element of NAT
0 is empty Relation-like non-empty empty-yielding RAT -valued functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite cardinal {} -element V39() V41() V94() complex ext-real non negative complex-valued ext-real-valued real-valued natural-valued Element of NAT
the non empty non trivial Relation-like standard-ins V48() J/A-independent V51() set is non empty non trivial Relation-like standard-ins V48() J/A-independent V51() set
COM-Struct(# the non empty non trivial Relation-like standard-ins V48() J/A-independent V51() set #) is strict COM-Struct
S is strict COM-Struct
the InstructionsF of S is non empty Relation-like standard-ins V48() J/A-independent V51() set
S is with_non_trivial_Instructions COM-Struct
the InstructionsF of S is non empty Relation-like standard-ins V48() J/A-independent V51() set
I is set
J is set
halt S is Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
i is Element of the InstructionsF of S
S is with_non_trivial_Instructions COM-Struct
the InstructionsF of S is non empty Relation-like standard-ins V48() J/A-independent V51() set
I is No-StopCode Element of the InstructionsF of S
Macro I is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
K195(S,I) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K196(S,K195(S,I)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Stop S is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() non halt-free halt-ending unique-halt set
halt S is Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
K167((halt S)) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K157(K195(S,I),(Stop S)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc (Macro I) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
card (Macro I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom (Macro I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card (Macro I)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
2 -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
2 - 1 is V94() complex ext-real set
(Macro I) . (LastLoc (Macro I)) is set
J is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative set
(Macro I) . J is set
S is with_non_trivial_Instructions COM-Struct
the InstructionsF of S is non empty Relation-like standard-ins V48() J/A-independent V51() set
I is No-StopCode Element of the InstructionsF of S
Macro I is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
K195(S,I) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K196(S,K195(S,I)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Stop S is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() non halt-free halt-ending unique-halt set
halt S is Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
K167((halt S)) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K157(K195(S,I),(Stop S)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
J is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
(Macro I) ';' J is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc (Macro I) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc (Macro I) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
(Macro I) . (LastLoc (Macro I)) is set
(LastLoc (Macro I)) .--> ((Macro I) . (LastLoc (Macro I))) is trivial Relation-like NAT -defined {(LastLoc (Macro I))} -defined Function-like one-to-one set
{(LastLoc (Macro I))} is non empty trivial 1 -element set
{(LastLoc (Macro I))} --> ((Macro I) . (LastLoc (Macro I))) is non empty Relation-like {(LastLoc (Macro I))} -defined Function-like constant total V21({(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}) Element of bool [:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:]
{((Macro I) . (LastLoc (Macro I)))} is non empty trivial 1 -element set
[:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:] is Relation-like set
bool [:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:] is set
(Macro I) \ ((LastLoc (Macro I)) .--> ((Macro I) . (LastLoc (Macro I)))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool (Macro I)
bool (Macro I) is set
card (Macro I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom (Macro I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card (Macro I)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc (J,((card (Macro I)) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr (J,((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr (J,((card (Macro I)) -' 1))),((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc (Macro I)) +* (Reloc (J,((card (Macro I)) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
S is with_non_trivial_Instructions COM-Struct
the InstructionsF of S is non empty Relation-like standard-ins V48() J/A-independent V51() set
I is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
J is No-StopCode Element of the InstructionsF of S
Macro J is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
K195(S,J) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K196(S,K195(S,J)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Stop S is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() non halt-free halt-ending unique-halt set
halt S is Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
K167((halt S)) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K157(K195(S,J),(Stop S)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
I ';' (Macro J) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc I is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc I is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
I . (LastLoc I) is set
(LastLoc I) .--> (I . (LastLoc I)) is trivial Relation-like NAT -defined {(LastLoc I)} -defined Function-like one-to-one set
{(LastLoc I)} is non empty trivial 1 -element set
{(LastLoc I)} --> (I . (LastLoc I)) is non empty Relation-like {(LastLoc I)} -defined Function-like constant total V21({(LastLoc I)},{(I . (LastLoc I))}) Element of bool [:{(LastLoc I)},{(I . (LastLoc I))}:]
{(I . (LastLoc I))} is non empty trivial 1 -element set
[:{(LastLoc I)},{(I . (LastLoc I))}:] is Relation-like set
bool [:{(LastLoc I)},{(I . (LastLoc I))}:] is set
I \ ((LastLoc I) .--> (I . (LastLoc I))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool I
bool I is set
card I is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom I is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card I) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc ((Macro J),((card I) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr ((Macro J),((card I) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr ((Macro J),((card I) -' 1))),((card I) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc I) +* (Reloc ((Macro J),((card I) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
S is with_non_trivial_Instructions COM-Struct
the InstructionsF of S is non empty Relation-like standard-ins V48() J/A-independent V51() set
I is No-StopCode Element of the InstructionsF of S
Macro I is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
K195(S,I) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K196(S,K195(S,I)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Stop S is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() non halt-free halt-ending unique-halt set
halt S is Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
K167((halt S)) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K157(K195(S,I),(Stop S)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
J is No-StopCode Element of the InstructionsF of S
Macro J is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
K195(S,J) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K196(S,K195(S,J)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
K157(K195(S,J),(Stop S)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
(Macro I) ';' (Macro J) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc (Macro I) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc (Macro I) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
(Macro I) . (LastLoc (Macro I)) is set
(LastLoc (Macro I)) .--> ((Macro I) . (LastLoc (Macro I))) is trivial Relation-like NAT -defined {(LastLoc (Macro I))} -defined Function-like one-to-one set
{(LastLoc (Macro I))} is non empty trivial 1 -element set
{(LastLoc (Macro I))} --> ((Macro I) . (LastLoc (Macro I))) is non empty Relation-like {(LastLoc (Macro I))} -defined Function-like constant total V21({(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}) Element of bool [:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:]
{((Macro I) . (LastLoc (Macro I)))} is non empty trivial 1 -element set
[:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:] is Relation-like set
bool [:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:] is set
(Macro I) \ ((LastLoc (Macro I)) .--> ((Macro I) . (LastLoc (Macro I)))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool (Macro I)
bool (Macro I) is set
card (Macro I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom (Macro I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card (Macro I)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc ((Macro J),((card (Macro I)) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr ((Macro J),((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr ((Macro J),((card (Macro I)) -' 1))),((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc (Macro I)) +* (Reloc ((Macro J),((card (Macro I)) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
S is with_non_trivial_Instructions COM-Struct
the InstructionsF of S is non empty Relation-like standard-ins V48() J/A-independent V51() set
J is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
i is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
J ';' i is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc J is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc J is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
J . (LastLoc J) is set
(LastLoc J) .--> (J . (LastLoc J)) is trivial Relation-like NAT -defined {(LastLoc J)} -defined Function-like one-to-one set
{(LastLoc J)} is non empty trivial 1 -element set
{(LastLoc J)} --> (J . (LastLoc J)) is non empty Relation-like {(LastLoc J)} -defined Function-like constant total V21({(LastLoc J)},{(J . (LastLoc J))}) Element of bool [:{(LastLoc J)},{(J . (LastLoc J))}:]
{(J . (LastLoc J))} is non empty trivial 1 -element set
[:{(LastLoc J)},{(J . (LastLoc J))}:] is Relation-like set
bool [:{(LastLoc J)},{(J . (LastLoc J))}:] is set
J \ ((LastLoc J) .--> (J . (LastLoc J))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool J
bool J is set
card J is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom J is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card J) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc (i,((card J) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr (i,((card J) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr (i,((card J) -' 1))),((card J) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc J) +* (Reloc (i,((card J) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
I is No-StopCode Element of the InstructionsF of S
(S,(J ';' i),I) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
Macro I is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
K195(S,I) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K196(S,K195(S,I)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Stop S is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() non halt-free halt-ending unique-halt set
halt S is Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
K167((halt S)) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K157(K195(S,I),(Stop S)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
(J ';' i) ';' (Macro I) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc (J ';' i) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc (J ';' i) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
(J ';' i) . (LastLoc (J ';' i)) is set
(LastLoc (J ';' i)) .--> ((J ';' i) . (LastLoc (J ';' i))) is trivial Relation-like NAT -defined {(LastLoc (J ';' i))} -defined Function-like one-to-one set
{(LastLoc (J ';' i))} is non empty trivial 1 -element set
{(LastLoc (J ';' i))} --> ((J ';' i) . (LastLoc (J ';' i))) is non empty Relation-like {(LastLoc (J ';' i))} -defined Function-like constant total V21({(LastLoc (J ';' i))},{((J ';' i) . (LastLoc (J ';' i)))}) Element of bool [:{(LastLoc (J ';' i))},{((J ';' i) . (LastLoc (J ';' i)))}:]
{((J ';' i) . (LastLoc (J ';' i)))} is non empty trivial 1 -element set
[:{(LastLoc (J ';' i))},{((J ';' i) . (LastLoc (J ';' i)))}:] is Relation-like set
bool [:{(LastLoc (J ';' i))},{((J ';' i) . (LastLoc (J ';' i)))}:] is set
(J ';' i) \ ((LastLoc (J ';' i)) .--> ((J ';' i) . (LastLoc (J ';' i)))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool (J ';' i)
bool (J ';' i) is set
card (J ';' i) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom (J ';' i) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card (J ';' i)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc ((Macro I),((card (J ';' i)) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr ((Macro I),((card (J ';' i)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr ((Macro I),((card (J ';' i)) -' 1))),((card (J ';' i)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc (J ';' i)) +* (Reloc ((Macro I),((card (J ';' i)) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
(S,i,I) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
i ';' (Macro I) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc i is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc i is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
i . (LastLoc i) is set
(LastLoc i) .--> (i . (LastLoc i)) is trivial Relation-like NAT -defined {(LastLoc i)} -defined Function-like one-to-one set
{(LastLoc i)} is non empty trivial 1 -element set
{(LastLoc i)} --> (i . (LastLoc i)) is non empty Relation-like {(LastLoc i)} -defined Function-like constant total V21({(LastLoc i)},{(i . (LastLoc i))}) Element of bool [:{(LastLoc i)},{(i . (LastLoc i))}:]
{(i . (LastLoc i))} is non empty trivial 1 -element set
[:{(LastLoc i)},{(i . (LastLoc i))}:] is Relation-like set
bool [:{(LastLoc i)},{(i . (LastLoc i))}:] is set
i \ ((LastLoc i) .--> (i . (LastLoc i))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool i
bool i is set
card i is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom i is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card i) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc ((Macro I),((card i) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr ((Macro I),((card i) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr ((Macro I),((card i) -' 1))),((card i) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc i) +* (Reloc ((Macro I),((card i) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
J ';' (S,i,I) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
Reloc ((S,i,I),((card J) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr ((S,i,I),((card J) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr ((S,i,I),((card J) -' 1))),((card J) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc J) +* (Reloc ((S,i,I),((card J) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
S is with_non_trivial_Instructions COM-Struct
the InstructionsF of S is non empty Relation-like standard-ins V48() J/A-independent V51() set
J is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
I is No-StopCode Element of the InstructionsF of S
(S,J,I) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
Macro I is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
K195(S,I) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K196(S,K195(S,I)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Stop S is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() non halt-free halt-ending unique-halt set
halt S is Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
K167((halt S)) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K157(K195(S,I),(Stop S)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
J ';' (Macro I) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc J is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc J is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
J . (LastLoc J) is set
(LastLoc J) .--> (J . (LastLoc J)) is trivial Relation-like NAT -defined {(LastLoc J)} -defined Function-like one-to-one set
{(LastLoc J)} is non empty trivial 1 -element set
{(LastLoc J)} --> (J . (LastLoc J)) is non empty Relation-like {(LastLoc J)} -defined Function-like constant total V21({(LastLoc J)},{(J . (LastLoc J))}) Element of bool [:{(LastLoc J)},{(J . (LastLoc J))}:]
{(J . (LastLoc J))} is non empty trivial 1 -element set
[:{(LastLoc J)},{(J . (LastLoc J))}:] is Relation-like set
bool [:{(LastLoc J)},{(J . (LastLoc J))}:] is set
J \ ((LastLoc J) .--> (J . (LastLoc J))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool J
bool J is set
card J is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom J is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card J) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc ((Macro I),((card J) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr ((Macro I),((card J) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr ((Macro I),((card J) -' 1))),((card J) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc J) +* (Reloc ((Macro I),((card J) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
i is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
(S,J,I) ';' i is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc (S,J,I) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc (S,J,I) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
(S,J,I) . (LastLoc (S,J,I)) is set
(LastLoc (S,J,I)) .--> ((S,J,I) . (LastLoc (S,J,I))) is trivial Relation-like NAT -defined {(LastLoc (S,J,I))} -defined Function-like one-to-one set
{(LastLoc (S,J,I))} is non empty trivial 1 -element set
{(LastLoc (S,J,I))} --> ((S,J,I) . (LastLoc (S,J,I))) is non empty Relation-like {(LastLoc (S,J,I))} -defined Function-like constant total V21({(LastLoc (S,J,I))},{((S,J,I) . (LastLoc (S,J,I)))}) Element of bool [:{(LastLoc (S,J,I))},{((S,J,I) . (LastLoc (S,J,I)))}:]
{((S,J,I) . (LastLoc (S,J,I)))} is non empty trivial 1 -element set
[:{(LastLoc (S,J,I))},{((S,J,I) . (LastLoc (S,J,I)))}:] is Relation-like set
bool [:{(LastLoc (S,J,I))},{((S,J,I) . (LastLoc (S,J,I)))}:] is set
(S,J,I) \ ((LastLoc (S,J,I)) .--> ((S,J,I) . (LastLoc (S,J,I)))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool (S,J,I)
bool (S,J,I) is set
card (S,J,I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom (S,J,I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card (S,J,I)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc (i,((card (S,J,I)) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr (i,((card (S,J,I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr (i,((card (S,J,I)) -' 1))),((card (S,J,I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc (S,J,I)) +* (Reloc (i,((card (S,J,I)) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
(S,I,i) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
(Macro I) ';' i is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc (Macro I) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc (Macro I) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
(Macro I) . (LastLoc (Macro I)) is set
(LastLoc (Macro I)) .--> ((Macro I) . (LastLoc (Macro I))) is trivial Relation-like NAT -defined {(LastLoc (Macro I))} -defined Function-like one-to-one set
{(LastLoc (Macro I))} is non empty trivial 1 -element set
{(LastLoc (Macro I))} --> ((Macro I) . (LastLoc (Macro I))) is non empty Relation-like {(LastLoc (Macro I))} -defined Function-like constant total V21({(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}) Element of bool [:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:]
{((Macro I) . (LastLoc (Macro I)))} is non empty trivial 1 -element set
[:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:] is Relation-like set
bool [:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:] is set
(Macro I) \ ((LastLoc (Macro I)) .--> ((Macro I) . (LastLoc (Macro I)))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool (Macro I)
bool (Macro I) is set
card (Macro I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom (Macro I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card (Macro I)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc (i,((card (Macro I)) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr (i,((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr (i,((card (Macro I)) -' 1))),((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc (Macro I)) +* (Reloc (i,((card (Macro I)) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
J ';' (S,I,i) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
Reloc ((S,I,i),((card J) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr ((S,I,i),((card J) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr ((S,I,i),((card J) -' 1))),((card J) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc J) +* (Reloc ((S,I,i),((card J) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
S is with_non_trivial_Instructions COM-Struct
the InstructionsF of S is non empty Relation-like standard-ins V48() J/A-independent V51() set
i is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
I is No-StopCode Element of the InstructionsF of S
(S,i,I) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
Macro I is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
K195(S,I) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K196(S,K195(S,I)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Stop S is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() non halt-free halt-ending unique-halt set
halt S is Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
K167((halt S)) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K157(K195(S,I),(Stop S)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
i ';' (Macro I) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc i is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc i is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
i . (LastLoc i) is set
(LastLoc i) .--> (i . (LastLoc i)) is trivial Relation-like NAT -defined {(LastLoc i)} -defined Function-like one-to-one set
{(LastLoc i)} is non empty trivial 1 -element set
{(LastLoc i)} --> (i . (LastLoc i)) is non empty Relation-like {(LastLoc i)} -defined Function-like constant total V21({(LastLoc i)},{(i . (LastLoc i))}) Element of bool [:{(LastLoc i)},{(i . (LastLoc i))}:]
{(i . (LastLoc i))} is non empty trivial 1 -element set
[:{(LastLoc i)},{(i . (LastLoc i))}:] is Relation-like set
bool [:{(LastLoc i)},{(i . (LastLoc i))}:] is set
i \ ((LastLoc i) .--> (i . (LastLoc i))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool i
bool i is set
card i is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom i is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card i) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc ((Macro I),((card i) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr ((Macro I),((card i) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr ((Macro I),((card i) -' 1))),((card i) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc i) +* (Reloc ((Macro I),((card i) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
J is No-StopCode Element of the InstructionsF of S
(S,(S,i,I),J) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
Macro J is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
K195(S,J) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K196(S,K195(S,J)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
K157(K195(S,J),(Stop S)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
(S,i,I) ';' (Macro J) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc (S,i,I) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc (S,i,I) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
(S,i,I) . (LastLoc (S,i,I)) is set
(LastLoc (S,i,I)) .--> ((S,i,I) . (LastLoc (S,i,I))) is trivial Relation-like NAT -defined {(LastLoc (S,i,I))} -defined Function-like one-to-one set
{(LastLoc (S,i,I))} is non empty trivial 1 -element set
{(LastLoc (S,i,I))} --> ((S,i,I) . (LastLoc (S,i,I))) is non empty Relation-like {(LastLoc (S,i,I))} -defined Function-like constant total V21({(LastLoc (S,i,I))},{((S,i,I) . (LastLoc (S,i,I)))}) Element of bool [:{(LastLoc (S,i,I))},{((S,i,I) . (LastLoc (S,i,I)))}:]
{((S,i,I) . (LastLoc (S,i,I)))} is non empty trivial 1 -element set
[:{(LastLoc (S,i,I))},{((S,i,I) . (LastLoc (S,i,I)))}:] is Relation-like set
bool [:{(LastLoc (S,i,I))},{((S,i,I) . (LastLoc (S,i,I)))}:] is set
(S,i,I) \ ((LastLoc (S,i,I)) .--> ((S,i,I) . (LastLoc (S,i,I)))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool (S,i,I)
bool (S,i,I) is set
card (S,i,I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom (S,i,I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card (S,i,I)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc ((Macro J),((card (S,i,I)) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr ((Macro J),((card (S,i,I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr ((Macro J),((card (S,i,I)) -' 1))),((card (S,i,I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc (S,i,I)) +* (Reloc ((Macro J),((card (S,i,I)) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
(S,I,J) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
(Macro I) ';' (Macro J) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc (Macro I) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc (Macro I) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
(Macro I) . (LastLoc (Macro I)) is set
(LastLoc (Macro I)) .--> ((Macro I) . (LastLoc (Macro I))) is trivial Relation-like NAT -defined {(LastLoc (Macro I))} -defined Function-like one-to-one set
{(LastLoc (Macro I))} is non empty trivial 1 -element set
{(LastLoc (Macro I))} --> ((Macro I) . (LastLoc (Macro I))) is non empty Relation-like {(LastLoc (Macro I))} -defined Function-like constant total V21({(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}) Element of bool [:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:]
{((Macro I) . (LastLoc (Macro I)))} is non empty trivial 1 -element set
[:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:] is Relation-like set
bool [:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:] is set
(Macro I) \ ((LastLoc (Macro I)) .--> ((Macro I) . (LastLoc (Macro I)))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool (Macro I)
bool (Macro I) is set
card (Macro I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom (Macro I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card (Macro I)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc ((Macro J),((card (Macro I)) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr ((Macro J),((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr ((Macro J),((card (Macro I)) -' 1))),((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc (Macro I)) +* (Reloc ((Macro J),((card (Macro I)) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
i ';' (S,I,J) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
Reloc ((S,I,J),((card i) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr ((S,I,J),((card i) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr ((S,I,J),((card i) -' 1))),((card i) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc i) +* (Reloc ((S,I,J),((card i) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
S is with_non_trivial_Instructions COM-Struct
the InstructionsF of S is non empty Relation-like standard-ins V48() J/A-independent V51() set
I is No-StopCode Element of the InstructionsF of S
J is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
(S,I,J) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
Macro I is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
K195(S,I) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K196(S,K195(S,I)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Stop S is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() non halt-free halt-ending unique-halt set
halt S is Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
K167((halt S)) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K157(K195(S,I),(Stop S)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
(Macro I) ';' J is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc (Macro I) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc (Macro I) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
(Macro I) . (LastLoc (Macro I)) is set
(LastLoc (Macro I)) .--> ((Macro I) . (LastLoc (Macro I))) is trivial Relation-like NAT -defined {(LastLoc (Macro I))} -defined Function-like one-to-one set
{(LastLoc (Macro I))} is non empty trivial 1 -element set
{(LastLoc (Macro I))} --> ((Macro I) . (LastLoc (Macro I))) is non empty Relation-like {(LastLoc (Macro I))} -defined Function-like constant total V21({(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}) Element of bool [:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:]
{((Macro I) . (LastLoc (Macro I)))} is non empty trivial 1 -element set
[:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:] is Relation-like set
bool [:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:] is set
(Macro I) \ ((LastLoc (Macro I)) .--> ((Macro I) . (LastLoc (Macro I)))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool (Macro I)
bool (Macro I) is set
card (Macro I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom (Macro I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card (Macro I)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc (J,((card (Macro I)) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr (J,((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr (J,((card (Macro I)) -' 1))),((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc (Macro I)) +* (Reloc (J,((card (Macro I)) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
i is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
(S,I,J) ';' i is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc (S,I,J) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc (S,I,J) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
(S,I,J) . (LastLoc (S,I,J)) is set
(LastLoc (S,I,J)) .--> ((S,I,J) . (LastLoc (S,I,J))) is trivial Relation-like NAT -defined {(LastLoc (S,I,J))} -defined Function-like one-to-one set
{(LastLoc (S,I,J))} is non empty trivial 1 -element set
{(LastLoc (S,I,J))} --> ((S,I,J) . (LastLoc (S,I,J))) is non empty Relation-like {(LastLoc (S,I,J))} -defined Function-like constant total V21({(LastLoc (S,I,J))},{((S,I,J) . (LastLoc (S,I,J)))}) Element of bool [:{(LastLoc (S,I,J))},{((S,I,J) . (LastLoc (S,I,J)))}:]
{((S,I,J) . (LastLoc (S,I,J)))} is non empty trivial 1 -element set
[:{(LastLoc (S,I,J))},{((S,I,J) . (LastLoc (S,I,J)))}:] is Relation-like set
bool [:{(LastLoc (S,I,J))},{((S,I,J) . (LastLoc (S,I,J)))}:] is set
(S,I,J) \ ((LastLoc (S,I,J)) .--> ((S,I,J) . (LastLoc (S,I,J)))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool (S,I,J)
bool (S,I,J) is set
card (S,I,J) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom (S,I,J) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card (S,I,J)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc (i,((card (S,I,J)) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr (i,((card (S,I,J)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr (i,((card (S,I,J)) -' 1))),((card (S,I,J)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc (S,I,J)) +* (Reloc (i,((card (S,I,J)) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
J ';' i is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc J is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc J is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
J . (LastLoc J) is set
(LastLoc J) .--> (J . (LastLoc J)) is trivial Relation-like NAT -defined {(LastLoc J)} -defined Function-like one-to-one set
{(LastLoc J)} is non empty trivial 1 -element set
{(LastLoc J)} --> (J . (LastLoc J)) is non empty Relation-like {(LastLoc J)} -defined Function-like constant total V21({(LastLoc J)},{(J . (LastLoc J))}) Element of bool [:{(LastLoc J)},{(J . (LastLoc J))}:]
{(J . (LastLoc J))} is non empty trivial 1 -element set
[:{(LastLoc J)},{(J . (LastLoc J))}:] is Relation-like set
bool [:{(LastLoc J)},{(J . (LastLoc J))}:] is set
J \ ((LastLoc J) .--> (J . (LastLoc J))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool J
bool J is set
card J is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom J is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card J) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc (i,((card J) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr (i,((card J) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr (i,((card J) -' 1))),((card J) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc J) +* (Reloc (i,((card J) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
(S,I,(J ';' i)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
(Macro I) ';' (J ';' i) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
Reloc ((J ';' i),((card (Macro I)) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr ((J ';' i),((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr ((J ';' i),((card (Macro I)) -' 1))),((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc (Macro I)) +* (Reloc ((J ';' i),((card (Macro I)) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
S is with_non_trivial_Instructions COM-Struct
the InstructionsF of S is non empty Relation-like standard-ins V48() J/A-independent V51() set
I is No-StopCode Element of the InstructionsF of S
i is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
(S,I,i) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
Macro I is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
K195(S,I) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K196(S,K195(S,I)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Stop S is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() non halt-free halt-ending unique-halt set
halt S is Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
K167((halt S)) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K157(K195(S,I),(Stop S)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
(Macro I) ';' i is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc (Macro I) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc (Macro I) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
(Macro I) . (LastLoc (Macro I)) is set
(LastLoc (Macro I)) .--> ((Macro I) . (LastLoc (Macro I))) is trivial Relation-like NAT -defined {(LastLoc (Macro I))} -defined Function-like one-to-one set
{(LastLoc (Macro I))} is non empty trivial 1 -element set
{(LastLoc (Macro I))} --> ((Macro I) . (LastLoc (Macro I))) is non empty Relation-like {(LastLoc (Macro I))} -defined Function-like constant total V21({(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}) Element of bool [:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:]
{((Macro I) . (LastLoc (Macro I)))} is non empty trivial 1 -element set
[:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:] is Relation-like set
bool [:{(LastLoc (Macro I))},{((Macro I) . (LastLoc (Macro I)))}:] is set
(Macro I) \ ((LastLoc (Macro I)) .--> ((Macro I) . (LastLoc (Macro I)))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool (Macro I)
bool (Macro I) is set
card (Macro I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom (Macro I) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card (Macro I)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc (i,((card (Macro I)) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr (i,((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr (i,((card (Macro I)) -' 1))),((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc (Macro I)) +* (Reloc (i,((card (Macro I)) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
J is No-StopCode Element of the InstructionsF of S
(S,(S,I,i),J) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
Macro J is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
K195(S,J) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K196(S,K195(S,J)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
K157(K195(S,J),(Stop S)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
(S,I,i) ';' (Macro J) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc (S,I,i) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc (S,I,i) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
(S,I,i) . (LastLoc (S,I,i)) is set
(LastLoc (S,I,i)) .--> ((S,I,i) . (LastLoc (S,I,i))) is trivial Relation-like NAT -defined {(LastLoc (S,I,i))} -defined Function-like one-to-one set
{(LastLoc (S,I,i))} is non empty trivial 1 -element set
{(LastLoc (S,I,i))} --> ((S,I,i) . (LastLoc (S,I,i))) is non empty Relation-like {(LastLoc (S,I,i))} -defined Function-like constant total V21({(LastLoc (S,I,i))},{((S,I,i) . (LastLoc (S,I,i)))}) Element of bool [:{(LastLoc (S,I,i))},{((S,I,i) . (LastLoc (S,I,i)))}:]
{((S,I,i) . (LastLoc (S,I,i)))} is non empty trivial 1 -element set
[:{(LastLoc (S,I,i))},{((S,I,i) . (LastLoc (S,I,i)))}:] is Relation-like set
bool [:{(LastLoc (S,I,i))},{((S,I,i) . (LastLoc (S,I,i)))}:] is set
(S,I,i) \ ((LastLoc (S,I,i)) .--> ((S,I,i) . (LastLoc (S,I,i)))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool (S,I,i)
bool (S,I,i) is set
card (S,I,i) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom (S,I,i) is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card (S,I,i)) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc ((Macro J),((card (S,I,i)) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr ((Macro J),((card (S,I,i)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr ((Macro J),((card (S,I,i)) -' 1))),((card (S,I,i)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc (S,I,i)) +* (Reloc ((Macro J),((card (S,I,i)) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
(S,i,J) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
i ';' (Macro J) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc i is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc i is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
i . (LastLoc i) is set
(LastLoc i) .--> (i . (LastLoc i)) is trivial Relation-like NAT -defined {(LastLoc i)} -defined Function-like one-to-one set
{(LastLoc i)} is non empty trivial 1 -element set
{(LastLoc i)} --> (i . (LastLoc i)) is non empty Relation-like {(LastLoc i)} -defined Function-like constant total V21({(LastLoc i)},{(i . (LastLoc i))}) Element of bool [:{(LastLoc i)},{(i . (LastLoc i))}:]
{(i . (LastLoc i))} is non empty trivial 1 -element set
[:{(LastLoc i)},{(i . (LastLoc i))}:] is Relation-like set
bool [:{(LastLoc i)},{(i . (LastLoc i))}:] is set
i \ ((LastLoc i) .--> (i . (LastLoc i))) is Relation-like NAT -defined the InstructionsF of S -valued Element of bool i
bool i is set
card i is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of omega
dom i is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative V116() set
(card i) -' 1 is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
Reloc ((Macro J),((card i) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr ((Macro J),((card i) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr ((Macro J),((card i) -' 1))),((card i) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc i) +* (Reloc ((Macro J),((card i) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
(S,I,(S,i,J)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
(Macro I) ';' (S,i,J) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
Reloc ((S,i,J),((card (Macro I)) -' 1)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
IncAddr ((S,i,J),((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Shift ((IncAddr ((S,i,J),((card (Macro I)) -' 1))),((card (Macro I)) -' 1)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like finite set
(CutLastLoc (Macro I)) +* (Reloc ((S,i,J),((card (Macro I)) -' 1))) is Relation-like NAT -defined the InstructionsF of S -valued Function-like set
S is with_non_trivial_Instructions COM-Struct
the InstructionsF of S is non empty Relation-like standard-ins V48() J/A-independent V51() set
I is No-StopCode Element of the InstructionsF of S
J is No-StopCode Element of the InstructionsF of S
(S,I,J) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
Macro I is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
K195(S,I) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K196(S,K195(S,I)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Stop S is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() non halt-free halt-ending unique-halt set
halt S is Element of the InstructionsF of S
halt the InstructionsF of S is ins-loc-free Element of the InstructionsF of S
K167((halt S)) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K157(K195(S,I),(Stop S)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
Macro J is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
K195(S,J) is non empty trivial Relation-like NAT -defined the InstructionsF of S -valued the InstructionsF of S -valued Function-like T-Sequence-like finite 1 -element V46() unique-halt set
K196(S,K195(S,J)) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
K157(K195(S,J),(Stop S)) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
(Macro I) ';' (Macro J) is non empty Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() halt-ending unique-halt set
CutLastLoc (Macro I) is Relation-like NAT -defined the InstructionsF of S -valued Function-like T-Sequence-like finite V46() set
LastLoc (Macro I) is epsilon-transitive epsilon-connected ordinal natural finite cardinal V94() complex ext-real non negative Element of NAT
(Macro I) . (LastLoc (Macro I)) is set
(LastLoc (Macro I)) .--> ((Macro I) . (LastLoc (Macro I))) is trivial Relation-like NAT -defined {(LastLoc (Macro