:: SFMASTR1 semantic presentation

REAL is non empty V5() V50() V51() V52() V56() non finite V68() V69() V71() V102() set
NAT is non empty V26() V27() V28() V50() V51() V52() V53() V54() V55() V56() V66() V68() Element of K32(REAL)
K32(REAL) is non empty set
K458() is non empty V120(2) IC-Ins-separated strict V128(2) AMI-Struct over 2
2 is non empty V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V66() V68() V101() Element of NAT
the carrier of K458() is non empty set
K422(2,K458()) is non empty Relation-like non-empty non empty-yielding the carrier of K458() -defined Function-like total set
the Object-Kind of K458() is Relation-like Function-like V18( the carrier of K458(),2) Element of K32(K33( the carrier of K458(),2))
K33( the carrier of K458(),2) is non empty Relation-like set
K32(K33( the carrier of K458(),2)) is non empty set
the U7 of K458() is non empty Relation-like 2 -defined Function-like total set
the Object-Kind of K458() * the U7 of K458() is Relation-like Function-like set
SCM+FSA is non empty V120(3) IC-Ins-separated strict V128(3) with_explicit_jumps IC-relocable V157(3) AMI-Struct over 3
3 is non empty V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V66() V68() V101() Element of NAT
K552() is set
K619(NAT,K552()) is Element of K552()
K545() is non empty set
K555() is Relation-like Function-like V18(K552(),3) Element of K32(K33(K552(),3))
K33(K552(),3) is Relation-like set
K32(K33(K552(),3)) is non empty set
K556() is non empty Relation-like 3 -defined Function-like total set
K563() is Relation-like Function-like V18(K545(),K99(K316((K555() * K556())),K316((K555() * K556())))) Element of K32(K33(K545(),K99(K316((K555() * K556())),K316((K555() * K556())))))
K555() * K556() is Relation-like Function-like set
K316((K555() * K556())) is set
K99(K316((K555() * K556())),K316((K555() * K556()))) is set
K33(K545(),K99(K316((K555() * K556())),K316((K555() * K556())))) is Relation-like set
K32(K33(K545(),K99(K316((K555() * K556())),K316((K555() * K556()))))) is non empty set
AMI-Struct(# K552(),K619(NAT,K552()),K545(),K555(),K556(),K563() #) is strict AMI-Struct over 3
the carrier of SCM+FSA is non empty set
COMPLEX is non empty V5() V50() V56() non finite V102() set
RAT is non empty V5() V50() V51() V52() V53() V56() non finite V102() set
INT is non empty V5() V50() V51() V52() V53() V54() V56() non finite V102() set
NAT is non empty V26() V27() V28() V50() V51() V52() V53() V54() V55() V56() V66() V68() set
K32(NAT) is non empty set
K32(NAT) is non empty set
K33(COMPLEX,COMPLEX) is non empty Relation-like set
K32(K33(COMPLEX,COMPLEX)) is non empty set
K33(COMPLEX,REAL) is non empty Relation-like set
K32(K33(COMPLEX,REAL)) is non empty set
9 is non empty V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V66() V68() V101() Element of NAT
Segm 9 is V50() V51() V52() V53() V54() V55() V68() Element of K32(NAT)
Int-Locations is non empty set
K334() is set
K32(K334()) is non empty set
K33(K334(),2) is Relation-like set
K32(K33(K334(),2)) is non empty set
K336() is Relation-like Function-like V18(K334(),2) Element of K32(K33(K334(),2))
K337() is non empty Relation-like 2 -defined Function-like total set
K336() * K337() is Relation-like Function-like set
K316((K336() * K337())) is set
K328() is non empty set
K99(K316((K336() * K337())),K316((K336() * K337()))) is set
K33(K328(),K99(K316((K336() * K337())),K316((K336() * K337())))) is Relation-like set
K32(K33(K328(),K99(K316((K336() * K337())),K316((K336() * K337()))))) is non empty set
the InstructionsF of K458() is non empty Relation-like standard-ins V110() J/A-independent V113() set
K32( the carrier of SCM+FSA) is non empty set
the InstructionsF of SCM+FSA is non empty Relation-like standard-ins V110() J/A-independent V113() set
Int-Locations is non empty Element of K32( the carrier of SCM+FSA)
K113(Int-Locations) is V24() set
K32(Int-Locations) is non empty set
FinSeq-Locations is non empty V5() non finite V102() Element of K32( the carrier of SCM+FSA)
K554() is Element of K32(K552())
K32(K552()) is non empty set
K113(FinSeq-Locations) is V24() set
K32(FinSeq-Locations) is non empty set
K422(3,SCM+FSA) is non empty Relation-like non-empty non empty-yielding the carrier of SCM+FSA -defined Function-like total set
the Object-Kind of SCM+FSA is Relation-like Function-like V18( the carrier of SCM+FSA,3) Element of K32(K33( the carrier of SCM+FSA,3))
K33( the carrier of SCM+FSA,3) is non empty Relation-like set
K32(K33( the carrier of SCM+FSA,3)) is non empty set
the U7 of SCM+FSA is non empty Relation-like 3 -defined Function-like total set
the Object-Kind of SCM+FSA * the U7 of SCM+FSA is Relation-like Function-like set
K544() is set
K33(NAT,K32(NAT)) is non empty Relation-like set
K32(K33(NAT,K32(NAT))) is non empty set
FinPartSt SCM+FSA is non empty Element of K32(K320(K422(3,SCM+FSA)))
K320(K422(3,SCM+FSA)) is set
K32(K320(K422(3,SCM+FSA))) is non empty set
{ b₁ where b₁ is Element of K320(K422(3,SCM+FSA)) : b₁ is finite } is set
K33((FinPartSt SCM+FSA),(FinPartSt SCM+FSA)) is non empty Relation-like set
K32(K33((FinPartSt SCM+FSA),(FinPartSt SCM+FSA))) is non empty set
1 is non empty V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V66() V68() V101() Element of NAT
{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V26() V27() V28() V30() V31() V32() V33() V34() ext-real non negative V48() V50() V51() V52() V53() V54() V55() V56() finite finite-yielding V61() V68() V69() V70() V71() V75() V76() V77() Function-yielding V132() set
0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V26() V27() V28() V30() V31() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V56() finite finite-yielding V61() V68() V69() V70() V71() V75() V76() V77() Function-yielding V132() Element of NAT
12 is non empty V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V66() V68() V101() Element of NAT
4 is non empty V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V66() V68() V101() Element of NAT
5 is non empty V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V66() V68() V101() Element of NAT
6 is non empty V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V66() V68() V101() Element of NAT
7 is non empty V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V66() V68() V101() Element of NAT
8 is non empty V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V66() V68() V101() Element of NAT
10 is non empty V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V66() V68() V101() Element of NAT
11 is non empty V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V66() V68() V101() Element of NAT
Fib 0 is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Fib 1 is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
IC is V88( SCM+FSA ) Element of the carrier of SCM+FSA
halt SCM+FSA is ins-loc-free V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V156(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
halt the InstructionsF of SCM+FSA is ins-loc-free with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
K15(0,{},{}) is set
NonZero SCM+FSA is Element of K32( the carrier of SCM+FSA)
Int-Locations \/ FinSeq-Locations is non empty Element of K32( the carrier of SCM+FSA)
intloc 0 is V100() read-only Element of the carrier of SCM+FSA
K467(0) is V100() Element of the carrier of K458()
Goto 2 is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() halt-free V118( SCM+FSA ) good set
Stop SCM+FSA is non empty V5() Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like constant finite V108() non halt-free V117( SCM+FSA ) V118( SCM+FSA ) keeping_0 good V159(3, SCM+FSA ) paraclosed parahalting set
K390((halt SCM+FSA)) is set
K335() is non empty Element of K32(K334())
(intloc 0) .--> 1 is V5() Relation-like the carrier of SCM+FSA -defined {(intloc 0)} -defined {(intloc 0)} -defined NAT -valued Function-like one-to-one constant K422(3,SCM+FSA) -compatible finite data-only set
{(intloc 0)} is non empty finite set
{(intloc 0)} --> 1 is non empty Relation-like non-empty non empty-yielding {(intloc 0)} -defined NAT -valued Function-like constant total V18({(intloc 0)},{1}) finite Element of K32(K33({(intloc 0)},{1}))
{1} is non empty V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() V101() V102() set
K33({(intloc 0)},{1}) is non empty Relation-like finite set
K32(K33({(intloc 0)},{1})) is non empty finite V61() set
Initialize ((intloc 0) .--> 1) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible finite 0 -started set
Start-At (0,SCM+FSA) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible finite 0 -started set
(IC ) .--> 0 is V5() Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued Function-like one-to-one constant finite Function-yielding V132() set
{(IC )} is non empty finite set
{(IC )} --> 0 is non empty Relation-like {(IC )} -defined NAT -valued Function-like constant total V18({(IC )},{0}) finite Function-yielding V132() Element of K32(K33({(IC )},{0}))
{0} is non empty functional V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() set
K33({(IC )},{0}) is non empty Relation-like finite set
K32(K33({(IC )},{0})) is non empty finite V61() set
((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible K422(3,SCM+FSA) -compatible finite 0 -started set
dom (Initialize ((intloc 0) .--> 1)) is finite set
(Initialize ((intloc 0) .--> 1)) . (intloc 0) is set
D is V100() non read-only Element of the carrier of SCM+FSA
SAt is V100() Element of the carrier of SCM+FSA
D := SAt is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
Macro (D := SAt) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 paraclosed parahalting set
K418(SCM+FSA,(D := SAt)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,(D := SAt)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
AddTo (D,SAt) is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
Macro (AddTo (D,SAt)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 paraclosed parahalting set
K418(SCM+FSA,(AddTo (D,SAt))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,(AddTo (D,SAt))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
SubFrom (D,SAt) is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
Macro (SubFrom (D,SAt)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 paraclosed parahalting set
K418(SCM+FSA,(SubFrom (D,SAt))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,(SubFrom (D,SAt))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
MultBy (D,SAt) is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
Macro (MultBy (D,SAt)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 paraclosed parahalting set
K418(SCM+FSA,(MultBy (D,SAt))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,(MultBy (D,SAt))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
the V100() non read-only Element of the carrier of SCM+FSA is V100() non read-only Element of the carrier of SCM+FSA
the V100() non read-only Element of the carrier of SCM+FSA := the V100() non read-only Element of the carrier of SCM+FSA is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V158(3, SCM+FSA ) () Element of the InstructionsF of SCM+FSA
D is V100() non read-only Element of the carrier of SCM+FSA
SAt is V100() non read-only Element of the carrier of SCM+FSA
Divide (D,SAt) is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
Macro (Divide (D,SAt)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 paraclosed parahalting set
K418(SCM+FSA,(Divide (D,SAt))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,(Divide (D,SAt))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
D is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
goto D is non ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K464(D) is Element of the InstructionsF of K458()
Macro (goto D) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K418(SCM+FSA,(goto D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,(goto D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
SAt is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
D is V100() Element of the carrier of SCM+FSA
D =0_goto SAt is non ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
Macro (D =0_goto SAt) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K418(SCM+FSA,(D =0_goto SAt)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,(D =0_goto SAt)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
D >0_goto SAt is non ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
Macro (D >0_goto SAt) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K418(SCM+FSA,(D >0_goto SAt)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,(D >0_goto SAt)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
p is V100() non read-only Element of the carrier of SCM+FSA
D is V100() Element of the carrier of SCM+FSA
SAt is FinSeq-Location
p := (SAt,D) is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K252(p,SAt,D) is non empty Relation-like NAT -defined Function-like finite 3 -element V75() V76() set
K15(9,{},K252(p,SAt,D)) is set
Macro (p := (SAt,D)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 paraclosed parahalting set
K418(SCM+FSA,(p := (SAt,D))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,(p := (SAt,D))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
SAt is V100() non read-only Element of the carrier of SCM+FSA
D is FinSeq-Location
SAt :=len D is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K251(SAt,D) is non empty Relation-like NAT -defined Function-like finite 2 -element V75() V76() set
K15(11,{},K251(SAt,D)) is set
Macro (SAt :=len D) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 paraclosed parahalting set
K418(SCM+FSA,(SAt :=len D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,(SAt :=len D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
SAt is V100() Element of the carrier of SCM+FSA
D is FinSeq-Location
D :=<0,...,0> SAt is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K251(SAt,D) is non empty Relation-like NAT -defined Function-like finite 2 -element V75() V76() set
K15(12,{},K251(SAt,D)) is set
Macro (D :=<0,...,0> SAt) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 paraclosed parahalting set
K418(SCM+FSA,(D :=<0,...,0> SAt)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,(D :=<0,...,0> SAt)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
p is V100() Element of the carrier of SCM+FSA
(D,SAt) := p is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K252(p,D,SAt) is non empty Relation-like NAT -defined Function-like finite 3 -element V75() V76() set
K15(10,{},K252(p,D,SAt)) is set
Macro ((D,SAt) := p) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 paraclosed parahalting set
K418(SCM+FSA,((D,SAt) := p)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,((D,SAt) := p)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
D is with_explicit_jumps IC-relocable () Element of the InstructionsF of SCM+FSA
Macro D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K418(SCM+FSA,D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
D is with_explicit_jumps IC-relocable () Element of the InstructionsF of SCM+FSA
SAt is with_explicit_jumps IC-relocable () Element of the InstructionsF of SCM+FSA
D ";" SAt is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
Macro D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() good set
K418(SCM+FSA,D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
Macro SAt is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() good set
K418(SCM+FSA,SAt) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,SAt) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(Macro D) ";" (Macro SAt) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() good set
stop (Macro D) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K380((Macro D),(Stop SCM+FSA)) is Relation-like Function-like V30() set
CutLastLoc (stop (Macro D)) is Relation-like Function-like set
Directed (CutLastLoc (stop (Macro D))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro D) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Reloc ((Macro SAt),(card (Macro D))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro SAt),(card (Macro D))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K229((IncAddr ((Macro SAt),(card (Macro D)))),(card (Macro D))) is Relation-like Function-like set
(Directed (CutLastLoc (stop (Macro D)))) +* (Reloc ((Macro SAt),(card (Macro D)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
D is with_explicit_jumps IC-relocable () Element of the InstructionsF of SCM+FSA
SAt is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() good set
D ";" SAt is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
Macro D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() good set
K418(SCM+FSA,D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,D) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(Macro D) ";" SAt is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() good set
stop (Macro D) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K380((Macro D),(Stop SCM+FSA)) is Relation-like Function-like V30() set
CutLastLoc (stop (Macro D)) is Relation-like Function-like set
Directed (CutLastLoc (stop (Macro D))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro D) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Reloc (SAt,(card (Macro D))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (SAt,(card (Macro D))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K229((IncAddr (SAt,(card (Macro D)))),(card (Macro D))) is Relation-like Function-like set
(Directed (CutLastLoc (stop (Macro D)))) +* (Reloc (SAt,(card (Macro D)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
SAt ";" D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
SAt ";" (Macro D) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() good set
stop SAt is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K380(SAt,(Stop SCM+FSA)) is Relation-like Function-like V30() set
CutLastLoc (stop SAt) is Relation-like Function-like set
Directed (CutLastLoc (stop SAt)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card SAt is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Reloc ((Macro D),(card SAt)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro D),(card SAt)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K229((IncAddr ((Macro D),(card SAt))),(card SAt)) is Relation-like Function-like set
(Directed (CutLastLoc (stop SAt))) +* (Reloc ((Macro D),(card SAt))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
D is V100() non read-only Element of the carrier of SCM+FSA
SAt is V100() non read-only Element of the carrier of SCM+FSA
swap (D,SAt) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 paraclosed parahalting set
D := SAt is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V158(3, SCM+FSA ) () Element of the InstructionsF of SCM+FSA
Macro (D := SAt) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 good paraclosed parahalting set
K418(SCM+FSA,(D := SAt)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,(D := SAt)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
FirstNotUsed (Macro (D := SAt)) is V100() non read-only Element of the carrier of SCM+FSA
(FirstNotUsed (Macro (D := SAt))) := D is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V158(3, SCM+FSA ) () Element of the InstructionsF of SCM+FSA
((FirstNotUsed (Macro (D := SAt))) := D) ";" (D := SAt) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 good paraclosed parahalting set
Macro ((FirstNotUsed (Macro (D := SAt))) := D) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 good paraclosed parahalting set
K418(SCM+FSA,((FirstNotUsed (Macro (D := SAt))) := D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,((FirstNotUsed (Macro (D := SAt))) := D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(Macro ((FirstNotUsed (Macro (D := SAt))) := D)) ";" (Macro (D := SAt)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 good paraclosed parahalting set
stop (Macro ((FirstNotUsed (Macro (D := SAt))) := D)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K380((Macro ((FirstNotUsed (Macro (D := SAt))) := D)),(Stop SCM+FSA)) is Relation-like Function-like V30() set
CutLastLoc (stop (Macro ((FirstNotUsed (Macro (D := SAt))) := D))) is Relation-like Function-like set
Directed (CutLastLoc (stop (Macro ((FirstNotUsed (Macro (D := SAt))) := D)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (Macro ((FirstNotUsed (Macro (D := SAt))) := D)) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Reloc ((Macro (D := SAt)),(card (Macro ((FirstNotUsed (Macro (D := SAt))) := D)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro (D := SAt)),(card (Macro ((FirstNotUsed (Macro (D := SAt))) := D)))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K229((IncAddr ((Macro (D := SAt)),(card (Macro ((FirstNotUsed (Macro (D := SAt))) := D))))),(card (Macro ((FirstNotUsed (Macro (D := SAt))) := D)))) is Relation-like Function-like set
(Directed (CutLastLoc (stop (Macro ((FirstNotUsed (Macro (D := SAt))) := D))))) +* (Reloc ((Macro (D := SAt)),(card (Macro ((FirstNotUsed (Macro (D := SAt))) := D))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
SAt := (FirstNotUsed (Macro (D := SAt))) is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V158(3, SCM+FSA ) () Element of the InstructionsF of SCM+FSA
(((FirstNotUsed (Macro (D := SAt))) := D) ";" (D := SAt)) ";" (SAt := (FirstNotUsed (Macro (D := SAt)))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 good paraclosed parahalting set
Macro (SAt := (FirstNotUsed (Macro (D := SAt)))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 good paraclosed parahalting set
K418(SCM+FSA,(SAt := (FirstNotUsed (Macro (D := SAt))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,(SAt := (FirstNotUsed (Macro (D := SAt))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
(((FirstNotUsed (Macro (D := SAt))) := D) ";" (D := SAt)) ";" (Macro (SAt := (FirstNotUsed (Macro (D := SAt))))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 good paraclosed parahalting set
stop (((FirstNotUsed (Macro (D := SAt))) := D) ";" (D := SAt)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K380((((FirstNotUsed (Macro (D := SAt))) := D) ";" (D := SAt)),(Stop SCM+FSA)) is Relation-like Function-like V30() set
CutLastLoc (stop (((FirstNotUsed (Macro (D := SAt))) := D) ";" (D := SAt))) is Relation-like Function-like set
Directed (CutLastLoc (stop (((FirstNotUsed (Macro (D := SAt))) := D) ";" (D := SAt)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card (((FirstNotUsed (Macro (D := SAt))) := D) ";" (D := SAt)) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Reloc ((Macro (SAt := (FirstNotUsed (Macro (D := SAt))))),(card (((FirstNotUsed (Macro (D := SAt))) := D) ";" (D := SAt)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro (SAt := (FirstNotUsed (Macro (D := SAt))))),(card (((FirstNotUsed (Macro (D := SAt))) := D) ";" (D := SAt)))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K229((IncAddr ((Macro (SAt := (FirstNotUsed (Macro (D := SAt))))),(card (((FirstNotUsed (Macro (D := SAt))) := D) ";" (D := SAt))))),(card (((FirstNotUsed (Macro (D := SAt))) := D) ";" (D := SAt)))) is Relation-like Function-like set
(Directed (CutLastLoc (stop (((FirstNotUsed (Macro (D := SAt))) := D) ";" (D := SAt))))) +* (Reloc ((Macro (SAt := (FirstNotUsed (Macro (D := SAt))))),(card (((FirstNotUsed (Macro (D := SAt))) := D) ";" (D := SAt))))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
SAt is V100() non read-only Element of the carrier of SCM+FSA
D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() good set
Times (SAt,D) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() non halt-free set
SubFrom (SAt,(intloc 0)) is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V158(3, SCM+FSA ) () Element of the InstructionsF of SCM+FSA
D ";" (SubFrom (SAt,(intloc 0))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() good set
Macro (SubFrom (SAt,(intloc 0))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued the InstructionsF of SCM+FSA -valued Function-like finite V108() keeping_0 good paraclosed parahalting set
K418(SCM+FSA,(SubFrom (SAt,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
stop K418(SCM+FSA,(SubFrom (SAt,(intloc 0)))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
D ";" (Macro (SubFrom (SAt,(intloc 0)))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() good set
stop D is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K380(D,(Stop SCM+FSA)) is Relation-like Function-like V30() set
CutLastLoc (stop D) is Relation-like Function-like set
Directed (CutLastLoc (stop D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card D is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Reloc ((Macro (SubFrom (SAt,(intloc 0)))),(card D)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr ((Macro (SubFrom (SAt,(intloc 0)))),(card D)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K229((IncAddr ((Macro (SubFrom (SAt,(intloc 0)))),(card D))),(card D)) is Relation-like Function-like set
(Directed (CutLastLoc (stop D))) +* (Reloc ((Macro (SubFrom (SAt,(intloc 0)))),(card D))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
if=0 (SAt,(Goto 2),(D ";" (SubFrom (SAt,(intloc 0))))) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() good set
p is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() good set
loop p is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() halt-free V118( SCM+FSA ) good set
if>0 (SAt,(loop p),(Stop SCM+FSA)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() good set
D is V100() Element of the carrier of SCM+FSA
SAt is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
UsedIntLoc SAt is finite Element of K32(Int-Locations)
p is with_explicit_jumps IC-relocable Element of the InstructionsF of SCM+FSA
rng SAt is non empty finite set
UsedIntLoc p is Element of K113(Int-Locations)
InsCode p is V26() V27() V28() V32() V33() V34() ext-real non negative V48() Element of InsCodes the InstructionsF of SCM+FSA
InsCodes the InstructionsF of SCM+FSA is non empty set
K23( the InstructionsF of SCM+FSA) is set
s is V100() Element of the carrier of SCM+FSA
N is V100() Element of the carrier of SCM+FSA
s := N is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
{s,N} is non empty finite Element of K32(Int-Locations)
s is V100() Element of the carrier of SCM+FSA
N is V100() Element of the carrier of SCM+FSA
AddTo (s,N) is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
{s,N} is non empty finite Element of K32(Int-Locations)
s is V100() Element of the carrier of SCM+FSA
N is V100() Element of the carrier of SCM+FSA
SubFrom (s,N) is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
{s,N} is non empty finite Element of K32(Int-Locations)
s is V100() Element of the carrier of SCM+FSA
N is V100() Element of the carrier of SCM+FSA
MultBy (s,N) is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
{s,N} is non empty finite Element of K32(Int-Locations)
s is V100() Element of the carrier of SCM+FSA
N is V100() Element of the carrier of SCM+FSA
Divide (s,N) is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
{s,N} is non empty finite Element of K32(Int-Locations)
s is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
goto s is non ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) () Element of the InstructionsF of SCM+FSA
K464(s) is Element of the InstructionsF of K458()
s is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
N is V100() Element of the carrier of SCM+FSA
N =0_goto s is non ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) () Element of the InstructionsF of SCM+FSA
s is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
N is V100() Element of the carrier of SCM+FSA
N >0_goto s is non ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) () Element of the InstructionsF of SCM+FSA
N is V100() Element of the carrier of SCM+FSA
s is V100() Element of the carrier of SCM+FSA
result is FinSeq-Location
N := (result,s) is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K252(N,result,s) is non empty Relation-like NAT -defined Function-like finite 3 -element V75() V76() set
K15(9,{},K252(N,result,s)) is set
{s,N} is non empty finite Element of K32(Int-Locations)
N is V100() Element of the carrier of SCM+FSA
s is V100() Element of the carrier of SCM+FSA
result is FinSeq-Location
(result,s) := N is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) () Element of the InstructionsF of SCM+FSA
K252(N,result,s) is non empty Relation-like NAT -defined Function-like finite 3 -element V75() V76() set
K15(10,{},K252(N,result,s)) is set
s is V100() Element of the carrier of SCM+FSA
N is FinSeq-Location
s :=len N is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
K251(s,N) is non empty Relation-like NAT -defined Function-like finite 2 -element V75() V76() set
K15(11,{},K251(s,N)) is set
{s} is non empty finite Element of K32(Int-Locations)
s is V100() Element of the carrier of SCM+FSA
N is FinSeq-Location
N :=<0,...,0> s is ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) parahalting keeping_0 with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) () Element of the InstructionsF of SCM+FSA
K251(s,N) is non empty Relation-like NAT -defined Function-like finite 2 -element V75() V76() set
K15(12,{},K251(s,N)) is set
p is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
Initialized s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible K422(3,SCM+FSA) -compatible total 0 -started set
N is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
IExec (N,p,s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
result is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
N ";" result is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
stop N is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K380(N,(Stop SCM+FSA)) is Relation-like Function-like V30() set
CutLastLoc (stop N) is Relation-like Function-like set
Directed (CutLastLoc (stop N)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card N is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Reloc (result,(card N)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (result,(card N)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K229((IncAddr (result,(card N))),(card N)) is Relation-like Function-like set
(Directed (CutLastLoc (stop N))) +* (Reloc (result,(card N))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
Initialize (Initialized s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total 0 -started set
(Initialized s) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible K422(3,SCM+FSA) -compatible total 0 -started set
p +* (N ";" result) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Directed N is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() halt-free V118( SCM+FSA ) set
Directed (N,(card N)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() halt-free set
goto (card N) is non ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) () Element of the InstructionsF of SCM+FSA
K464((card N)) is Element of the InstructionsF of K458()
N +~ ((halt SCM+FSA),(goto (card N))) is Relation-like Function-like set
(p +* (N ";" result)) +* (Directed N) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
DataPart (Initialized s) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(Initialized s) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
DataPart (Initialize (Initialized s)) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(Initialize (Initialized s)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
(p +* (N ";" result)) +* N is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialize (Initialize (Initialized s)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total 0 -started set
(Initialize (Initialized s)) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible K422(3,SCM+FSA) -compatible total 0 -started set
LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s)))) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s)))))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
Initialize (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total 0 -started set
(Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))))) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible K422(3,SCM+FSA) -compatible total 0 -started set
((p +* (N ";" result)) +* N) +* result is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
(Initialized s) . (intloc 0) is V33() V34() ext-real V48() set
(Initialize (Initialized s)) . (intloc 0) is V33() V34() ext-real V48() set
Initialized (Initialize (Initialize (Initialized s))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total 0 -started set
(Initialize (Initialize (Initialized s))) +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible K422(3,SCM+FSA) -compatible total 0 -started set
DataPart (IExec (N,p,s)) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(IExec (N,p,s)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
IExec (N,p,(Initialized s)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
DataPart (IExec (N,p,(Initialized s))) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(IExec (N,p,(Initialized s))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
IExec (N,(p +* (N ";" result)),(Initialize (Initialized s))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
DataPart (IExec (N,(p +* (N ";" result)),(Initialize (Initialized s)))) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(IExec (N,(p +* (N ";" result)),(Initialize (Initialized s)))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
Initialized (Initialize (Initialized s)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total 0 -started set
(Initialize (Initialized s)) +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible K422(3,SCM+FSA) -compatible total 0 -started set
Result (((p +* (N ";" result)) +* N),(Initialized (Initialize (Initialized s)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
DataPart (Result (((p +* (N ";" result)) +* N),(Initialized (Initialize (Initialized s))))) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(Result (((p +* (N ";" result)) +* N),(Initialized (Initialize (Initialized s))))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
DataPart (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))))) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
DataPart (Initialize (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s)))))))) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(Initialize (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s)))))))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1 is non empty V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V66() V68() V101() Element of NAT
Comput ((p +* (N ";" result)),(Initialize (Initialized s)),((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
DataPart (Start-At (0,SCM+FSA)) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible finite data-only set
(Start-At (0,SCM+FSA)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible finite set
I3 is Relation-like Function-like set
(DataPart (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s)))))))) +* I3 is Relation-like Function-like set
i4 is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Comput ((p +* (N ";" result)),(Initialize (Initialized s)),i4) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
IC (Comput ((p +* (N ";" result)),(Initialize (Initialized s)),i4)) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(Comput ((p +* (N ";" result)),(Initialize (Initialized s)),i4)) . (IC ) is set
K389((N ";" result)) is non empty V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() Element of K32(NAT)
Comput (((p +* (N ";" result)) +* (Directed N)),(Initialize (Initialized s)),((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
IC (Comput (((p +* (N ";" result)) +* (Directed N)),(Initialize (Initialized s)),((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1))) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(Comput (((p +* (N ";" result)) +* (Directed N)),(Initialize (Initialized s)),((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1))) . (IC ) is set
IC (Comput ((p +* (N ";" result)),(Initialize (Initialized s)),((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1))) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(Comput ((p +* (N ";" result)),(Initialize (Initialized s)),((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1))) . (IC ) is set
DataPart (Comput ((p +* (N ";" result)),(Initialize (Initialized s)),((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1))) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(Comput ((p +* (N ";" result)),(Initialize (Initialized s)),((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
dom N is non empty finite set
dom (N ";" result) is non empty finite set
Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),i4) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
IC (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),i4)) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),i4)) . (IC ) is set
n is V26() V27() V28() V32() V33() V34() ext-real non negative V48() set
((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1) + n is non empty V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V66() V68() V101() Element of NAT
i02 is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Comput ((((p +* (N ";" result)) +* N) +* result),(Initialize (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s)))))))),i02) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
IC (Comput ((((p +* (N ";" result)) +* N) +* result),(Initialize (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s)))))))),i02)) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(Comput ((((p +* (N ";" result)) +* N) +* result),(Initialize (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s)))))))),i02)) . (IC ) is set
Initialize (Initialize (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s)))))))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total 0 -started set
(Initialize (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s)))))))) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible K422(3,SCM+FSA) -compatible total 0 -started set
(((p +* (N ";" result)) +* N) +* result) +* result is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
dom result is non empty finite set
dom (Reloc (result,(card N))) is finite set
{ (b₁ + (card N)) where b₁ is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT : b₁ in dom result } is set
s1 is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
s1 + (card N) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
dom (N ";" result) is non empty finite set
(IC (Comput ((((p +* (N ";" result)) +* N) +* result),(Initialize (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s)))))))),i02))) + (card N) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Comput ((p +* (N ";" result)),(Comput ((p +* (N ";" result)),(Initialize (Initialized s)),((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1))),i02) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
IC (Comput ((p +* (N ";" result)),(Comput ((p +* (N ";" result)),(Initialize (Initialized s)),((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1))),i02)) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(Comput ((p +* (N ";" result)),(Comput ((p +* (N ";" result)),(Initialize (Initialized s)),((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1))),i02)) . (IC ) is set
((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1) + i02 is non empty V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V66() V68() V101() Element of NAT
Comput ((p +* (N ";" result)),(Initialize (Initialized s)),(((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1) + i02)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
IC (Comput ((p +* (N ";" result)),(Initialize (Initialized s)),(((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1) + i02))) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
(Comput ((p +* (N ";" result)),(Initialize (Initialized s)),(((LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))) + 1) + i02))) . (IC ) is set
p is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
Initialized s is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total 0 -started set
s +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible K422(3,SCM+FSA) -compatible total 0 -started set
N is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
IExec (N,p,s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
result is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
N ";" result is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
stop N is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K380(N,(Stop SCM+FSA)) is Relation-like Function-like V30() set
CutLastLoc (stop N) is Relation-like Function-like set
Directed (CutLastLoc (stop N)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
card N is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Reloc (result,(card N)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
IncAddr (result,(card N)) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() set
K229((IncAddr (result,(card N))),(card N)) is Relation-like Function-like set
(Directed (CutLastLoc (stop N))) +* (Reloc (result,(card N))) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite set
Initialize (Initialized s) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total 0 -started set
(Initialized s) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible K422(3,SCM+FSA) -compatible total 0 -started set
p +* (N ";" result) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Directed N is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() halt-free V118( SCM+FSA ) set
Directed (N,(card N)) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite V108() halt-free set
goto (card N) is non ins-loc-free V114( the InstructionsF of SCM+FSA) V127(3, SCM+FSA ) with_explicit_jumps IC-relocable V156(3, SCM+FSA ) V158(3, SCM+FSA ) () Element of the InstructionsF of SCM+FSA
K464((card N)) is Element of the InstructionsF of K458()
N +~ ((halt SCM+FSA),(goto (card N))) is Relation-like Function-like set
(p +* (N ";" result)) +* (Directed N) is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
DataPart (Initialized s) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(Initialized s) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
DataPart (Initialize (Initialized s)) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(Initialize (Initialized s)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
(p +* (N ";" result)) +* N is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Initialize (Initialize (Initialized s)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total 0 -started set
(Initialize (Initialized s)) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible K422(3,SCM+FSA) -compatible total 0 -started set
(Initialized s) . (intloc 0) is V33() V34() ext-real V48() set
(Initialize (Initialized s)) . (intloc 0) is V33() V34() ext-real V48() set
Initialized (Initialize (Initialized s)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total 0 -started set
(Initialize (Initialized s)) +* (Initialize ((intloc 0) .--> 1)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible K422(3,SCM+FSA) -compatible total 0 -started set
LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s)))) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s)))))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
Initialize (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total 0 -started set
(Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))))) +* (Start-At (0,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible K422(3,SCM+FSA) -compatible total 0 -started set
((p +* (N ";" result)) +* N) +* result is non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
LifeSpan ((((p +* (N ";" result)) +* N) +* result),(Initialize (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))))))) is V26() V27() V28() V32() V33() V34() ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() V68() Element of NAT
DataPart (IExec (N,p,s)) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(IExec (N,p,s)) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
IExec (N,p,(Initialized s)) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
DataPart (IExec (N,p,(Initialized s))) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(IExec (N,p,(Initialized s))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
IExec (N,(p +* (N ";" result)),(Initialize (Initialized s))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
DataPart (IExec (N,(p +* (N ";" result)),(Initialize (Initialized s)))) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(IExec (N,(p +* (N ";" result)),(Initialize (Initialized s)))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
Result (((p +* (N ";" result)) +* N),(Initialized (Initialize (Initialized s)))) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible total set
DataPart (Result (((p +* (N ";" result)) +* N),(Initialized (Initialize (Initialized s))))) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(Result (((p +* (N ";" result)) +* N),(Initialized (Initialize (Initialized s))))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
DataPart (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))))) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))))))) | (NonZero SCM+FSA) is Relation-like the carrier of SCM+FSA -defined NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible set
DataPart (Initialize (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s)))))))) is Relation-like the carrier of SCM+FSA -defined Function-like K422(3,SCM+FSA) -compatible data-only set
(Initialize (Comput (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized s))),(LifeSpan (((p +* (N ";" result)) +* N),(Initialize (Initialize (Initialized