:: 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

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

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