:: SCMFSA_5 semantic presentation

REAL is set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K32(REAL)

K32(REAL) is set

SCM+FSA is V111() V126(3) IC-Ins-separated strict V134(3) V138(3) V140(3) relocable IC-recognized CurIns-recognized AMI-Struct over 3

3 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() Element of NAT

K528() is set

K213(NAT,K528()) is Element of K528()

K521() is non empty set

K531() is Relation-like Function-like V29(K528(),3) Element of K32(K33(K528(),3))

K33(K528(),3) is Relation-like set

K32(K33(K528(),3)) is set

K532() is Relation-like 3 -defined Function-like total set

K539() is Relation-like Function-like V29(K521(),K160(K236((K531() * K532())),K236((K531() * K532())))) Element of K32(K33(K521(),K160(K236((K531() * K532())),K236((K531() * K532())))))

K531() * K532() is Relation-like Function-like set

K236((K531() * K532())) is set

K160(K236((K531() * K532())),K236((K531() * K532()))) is set

K33(K521(),K160(K236((K531() * K532())),K236((K531() * K532())))) is Relation-like set

K32(K33(K521(),K160(K236((K531() * K532())),K236((K531() * K532()))))) is set

AMI-Struct(# K528(),K213(NAT,K528()),K521(),K531(),K532(),K539() #) is strict AMI-Struct over 3

the U2 of SCM+FSA is set

COMPLEX is set

NAT is non empty epsilon-transitive epsilon-connected ordinal set

K32(NAT) is set

K32(NAT) is set

RAT is set

INT is set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() Element of NAT

9 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() Element of NAT

K194(9) is Element of K32(NAT)

Int-Locations is set

K473() is set

K32(K473()) is set

K33(K473(),2) is Relation-like set

K32(K33(K473(),2)) is set

K475() is Relation-like Function-like V29(K473(),2) Element of K32(K33(K473(),2))

K476() is Relation-like 2 -defined Function-like total set

K475() * K476() is Relation-like Function-like set

K236((K475() * K476())) is set

K467() is non empty set

K160(K236((K475() * K476())),K236((K475() * K476()))) is set

K33(K467(),K160(K236((K475() * K476())),K236((K475() * K476())))) is Relation-like set

K32(K33(K467(),K160(K236((K475() * K476())),K236((K475() * K476()))))) is set

K32( the U2 of SCM+FSA) is set

the InstructionsF of SCM+FSA is non empty Relation-like standard-ins V101() J/A-independent V104() set

K447(3,SCM+FSA) is Relation-like the U2 of SCM+FSA -defined Function-like total set

the Object-Kind of SCM+FSA is Relation-like Function-like V29( the U2 of SCM+FSA,3) Element of K32(K33( the U2 of SCM+FSA,3))

K33( the U2 of SCM+FSA,3) is Relation-like set

K32(K33( the U2 of SCM+FSA,3)) is set

the U7 of SCM+FSA is 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

K508() is V111() V126(2) IC-Ins-separated strict strict V134(2) AMI-Struct over 2

the InstructionsF of K508() is non empty Relation-like standard-ins V101() J/A-independent V104() set

the U2 of K508() is set

K447(2,K508()) is Relation-like the U2 of K508() -defined Function-like total set

the Object-Kind of K508() is Relation-like Function-like V29( the U2 of K508(),2) Element of K32(K33( the U2 of K508(),2))

K33( the U2 of K508(),2) is Relation-like set

K32(K33( the U2 of K508(),2)) is set

the U7 of K508() is Relation-like 2 -defined Function-like total set

the Object-Kind of K508() * the U7 of K508() is Relation-like Function-like set

K520() is set

K32(K528()) is set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() Element of NAT

12 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() Element of NAT

0 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

4 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() Element of NAT

5 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() Element of NAT

6 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() Element of NAT

7 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() Element of NAT

8 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() Element of NAT

10 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() Element of NAT

11 is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() Element of NAT

K530() is Element of K32(K528())

IC is Element of the U2 of SCM+FSA

halt SCM+FSA is ins-loc-free V133(3, SCM+FSA ) V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

Data-Locations is Element of K32( the U2 of SCM+FSA)

Int-Locations is Element of K32( the U2 of SCM+FSA)

FinSeq-Locations is non finite Element of K32( the U2 of SCM+FSA)

Int-Locations \/ FinSeq-Locations is Element of K32( the U2 of SCM+FSA)

K474() is Element of K32(K473())

k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

q is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite non halt-free set

Reloc (q,k) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite non halt-free set

p is non empty Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible finite q -autonomic set

IncIC (p,k) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

IC p is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

p . (IC ) is set

(IC p) + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

Start-At (((IC p) + k),SCM+FSA) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

K185((IC ),((IC p) + k)) is V5() set

p +* (Start-At (((IC p) + k),SCM+FSA)) is non empty Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

DataPart p is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

p | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Data-Locations -defined the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

dom (DataPart p) is set

s1 is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

s2 is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

DataPart s2 is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

s2 | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Data-Locations -defined the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

s1 +* (DataPart s2) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

dom p is non empty set

P1 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set

P2 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set

loc is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

Comput (P1,s1,loc) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

IC (Comput (P1,s1,loc)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(Comput (P1,s1,loc)) . (IC ) is set

(IC (Comput (P1,s1,loc))) + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

Comput (P2,s2,loc) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

IC (Comput (P2,s2,loc)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(Comput (P2,s2,loc)) . (IC ) is set

CurInstr (P1,(Comput (P1,s1,loc))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

P1 /. (IC (Comput (P1,s1,loc))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

IncAddr ((CurInstr (P1,(Comput (P1,s1,loc)))),k) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

CurInstr (P2,(Comput (P2,s2,loc))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

P2 /. (IC (Comput (P2,s2,loc))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (P1,s1,loc)) | (dom (DataPart p)) is Relation-like the U2 of SCM+FSA -defined dom (DataPart p) -defined the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

(Comput (P2,s2,loc)) | (dom (DataPart p)) is Relation-like the U2 of SCM+FSA -defined dom (DataPart p) -defined the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

Comput (P1,(s1 +* (DataPart s2)),loc) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

DataPart (Comput (P1,(s1 +* (DataPart s2)),loc)) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

(Comput (P1,(s1 +* (DataPart s2)),loc)) | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Data-Locations -defined the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

DataPart (Comput (P2,s2,loc)) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

(Comput (P2,s2,loc)) | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Data-Locations -defined the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

loc + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

Comput (P1,s1,(loc + 1)) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

IC (Comput (P1,s1,(loc + 1))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(Comput (P1,s1,(loc + 1))) . (IC ) is set

(IC (Comput (P1,s1,(loc + 1)))) + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

Comput (P2,s2,(loc + 1)) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

IC (Comput (P2,s2,(loc + 1))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(Comput (P2,s2,(loc + 1))) . (IC ) is set

CurInstr (P1,(Comput (P1,s1,(loc + 1)))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

P1 /. (IC (Comput (P1,s1,(loc + 1)))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

IncAddr ((CurInstr (P1,(Comput (P1,s1,(loc + 1))))),k) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

CurInstr (P2,(Comput (P2,s2,(loc + 1)))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

P2 /. (IC (Comput (P2,s2,(loc + 1)))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (P1,s1,(loc + 1))) | (dom (DataPart p)) is Relation-like the U2 of SCM+FSA -defined dom (DataPart p) -defined the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

(Comput (P2,s2,(loc + 1))) | (dom (DataPart p)) is Relation-like the U2 of SCM+FSA -defined dom (DataPart p) -defined the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

Comput (P1,(s1 +* (DataPart s2)),(loc + 1)) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Data-Locations -defined the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

DataPart (Comput (P2,s2,(loc + 1))) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

(Comput (P2,s2,(loc + 1))) | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Data-Locations -defined the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

dom (Comput (P1,s1,(loc + 1))) is set

{(IC )} is set

(Data-Locations ) \/ {(IC )} is set

dom (Comput (P1,s1,loc)) is set

dom (Comput (P2,s2,(loc + 1))) is set

dom (Comput (P2,s2,loc)) is set

Following (P2,(Comput (P2,s2,loc))) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

Exec ((CurInstr (P2,(Comput (P2,s2,loc)))),(Comput (P2,s2,loc))) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set

K160(K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set

the Execution of SCM+FSA is Relation-like Function-like V29( the InstructionsF of SCM+FSA,K160(K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K160(K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))

K33( the InstructionsF of SCM+FSA,K160(K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set

K32(K33( the InstructionsF of SCM+FSA,K160(K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set

K162( the InstructionsF of SCM+FSA,K160(K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,loc))))) is Element of K160(K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

K162( the InstructionsF of SCM+FSA,K160(K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,loc))))) . (Comput (P2,s2,loc)) is set

j is FinSeq-Location

Cs3i1 is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

DataPart Cs3i1 is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

Cs3i1 | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Data-Locations -defined the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

dom (DataPart Cs3i1) is set

Cs3i1 is FinSeq-Location

dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),loc))) is set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . Cs3i1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(DataPart (Comput (P1,(s1 +* (DataPart s2)),loc))) . Cs3i1 is set

(Comput (P2,s2,loc)) . Cs3i1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

dom (DataPart (Comput (P2,s2,loc))) is set

dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) is set

j is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

da is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

dom q is set

j + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

dom (Reloc (q,k)) is set

dom P2 is set

dom P1 is set

P1 . j is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

q . j is set

(Reloc (q,k)) . (j + k) is set

P2 . (IC (Comput (P2,s2,(loc + 1)))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

da is V141() Element of the U2 of SCM+FSA

j is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

DataPart j is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

j | (Data-Locations ) is Relation-like the U2 of SCM+FSA -defined Data-Locations -defined the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set

dom (DataPart j) is set

j is V141() Element of the U2 of SCM+FSA

(Comput (P1,(s1 +* (DataPart s2)),loc)) . j is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),loc))) . j is set

(Comput (P2,s2,loc)) . j is V24() V25() integer ext-real set

(dom p) /\ (Data-Locations ) is Element of K32( the U2 of SCM+FSA)

{(IC )} \/ (Data-Locations ) is set

InsCode (CurInstr (P1,(Comput (P1,s1,loc)))) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of InsCodes the InstructionsF of SCM+FSA

InsCodes the InstructionsF of SCM+FSA is non empty set

dom ((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) is set

(dom (Comput (P1,s1,(loc + 1)))) /\ (dom (DataPart p)) is set

dom (DataPart (Comput (P2,s2,(loc + 1)))) is set

j is set

dom ((Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) | (Data-Locations )) is set

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . j is set

(Comput (P2,s2,(loc + 1))) . j is set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . j is set

(DataPart (Comput (P2,s2,(loc + 1)))) . j is set

j is set

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . j is set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . j is set

(Comput (P2,s2,(loc + 1))) . j is set

(Comput (P2,s2,loc)) . j is set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),loc))) . j is set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . j is set

(DataPart (Comput (P2,s2,(loc + 1)))) . j is set

Following (P1,(Comput (P1,(s1 +* (DataPart s2)),loc))) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

CurInstr (P1,(Comput (P1,(s1 +* (DataPart s2)),loc))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

IC (Comput (P1,(s1 +* (DataPart s2)),loc)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(Comput (P1,(s1 +* (DataPart s2)),loc)) . (IC ) is set

P1 /. (IC (Comput (P1,(s1 +* (DataPart s2)),loc))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

Exec ((CurInstr (P1,(Comput (P1,(s1 +* (DataPart s2)),loc)))),(Comput (P1,(s1 +* (DataPart s2)),loc))) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

K162( the InstructionsF of SCM+FSA,K160(K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,(s1 +* (DataPart s2)),loc))))) is Element of K160(K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

K162( the InstructionsF of SCM+FSA,K160(K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,(s1 +* (DataPart s2)),loc))))) . (Comput (P1,(s1 +* (DataPart s2)),loc)) is set

Exec ((CurInstr (P1,(Comput (P1,s1,loc)))),(Comput (P1,(s1 +* (DataPart s2)),loc))) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

K162( the InstructionsF of SCM+FSA,K160(K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,loc))))) is Element of K160(K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))

K162( the InstructionsF of SCM+FSA,K160(K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,loc))))) . (Comput (P1,(s1 +* (DataPart s2)),loc)) is set

dom ((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) is set

(dom (Comput (P2,s2,(loc + 1)))) /\ (dom (DataPart p)) is set

da is set

j is set

(Comput (P1,s1,(loc + 1))) . da is set

(Comput (P2,s2,(loc + 1))) . da is set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . j is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . j is set

dom ((Comput (P1,s1,loc)) | (dom (DataPart p))) is set

(dom (Comput (P1,s1,loc))) /\ (dom (DataPart p)) is set

Following (P1,(Comput (P1,s1,loc))) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

Exec ((CurInstr (P1,(Comput (P1,s1,loc)))),(Comput (P1,s1,loc))) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set

K162( the InstructionsF of SCM+FSA,K160(K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K236(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,loc))))) . (Comput (P1,s1,loc)) is set

dom ((Comput (P2,s2,loc)) | (dom (DataPart p))) is set

(dom (Comput (P2,s2,loc))) /\ (dom (DataPart p)) is set

f is set

da is set

(Comput (P1,s1,(loc + 1))) . f is set

(Comput (P1,s1,loc)) . f is set

(Comput (P2,s2,(loc + 1))) . f is set

(Comput (P2,s2,loc)) . f is set

((Comput (P1,s1,loc)) | (dom (DataPart p))) . f is set

((Comput (P2,s2,loc)) | (dom (DataPart p))) . f is set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . da is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . da is set

succ ((IC (Comput (P1,s1,loc))) + k) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() set

j is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

j + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(j + k) + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

j + 1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(j + 1) + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

succ (IC (Comput (P1,s1,loc))) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() set

(succ (IC (Comput (P1,s1,loc)))) + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

da is V141() Element of the U2 of SCM+FSA

f is V141() Element of the U2 of SCM+FSA

da := f is ins-loc-free V105( the InstructionsF of SCM+FSA) V133(3, SCM+FSA ) V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Exec ((CurInstr (P1,(Comput (P1,s1,loc)))),(Comput (P1,s1,loc)))) . (IC ) is set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . f is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . f is V24() V25() integer ext-real set

x is set

d is FinSeq-Location

(Comput (P1,s1,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,s1,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

(Comput (P1,s1,loc)) . f is V24() V25() integer ext-real set

(Comput (P1,s1,(loc + 1))) . x is set

(Comput (P2,s2,(loc + 1))) . x is set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

d is V141() Element of the U2 of SCM+FSA

(Comput (P1,s1,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P1,s1,loc)) . d is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . d is V24() V25() integer ext-real set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

x is set

d is FinSeq-Location

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,(s1 +* (DataPart s2)),loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . da is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . da is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

d is V141() Element of the U2 of SCM+FSA

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . d is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . d is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

da is V141() Element of the U2 of SCM+FSA

f is V141() Element of the U2 of SCM+FSA

AddTo (da,f) is ins-loc-free V105( the InstructionsF of SCM+FSA) V133(3, SCM+FSA ) V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (P1,(s1 +* (DataPart s2)),loc)) . f is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . f is V24() V25() integer ext-real set

(Exec ((CurInstr (P1,(Comput (P1,s1,loc)))),(Comput (P1,s1,loc)))) . (IC ) is set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . da is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . da is V24() V25() integer ext-real set

x is set

d is FinSeq-Location

(Comput (P1,s1,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,s1,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

(Comput (P1,s1,(loc + 1))) . x is set

(Comput (P1,s1,loc)) . da is V24() V25() integer ext-real set

(Comput (P1,s1,loc)) . f is V24() V25() integer ext-real set

((Comput (P1,s1,loc)) . da) + ((Comput (P1,s1,loc)) . f) is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . x is set

((Comput (P2,s2,loc)) . da) + ((Comput (P2,s2,loc)) . f) is V24() V25() integer ext-real set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

d is V141() Element of the U2 of SCM+FSA

(Comput (P1,s1,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P1,s1,loc)) . d is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . d is V24() V25() integer ext-real set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

x is set

d is FinSeq-Location

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,(s1 +* (DataPart s2)),loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . x is set

((Comput (P1,(s1 +* (DataPart s2)),loc)) . da) + ((Comput (P1,(s1 +* (DataPart s2)),loc)) . f) is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . x is set

((Comput (P2,s2,loc)) . da) + ((Comput (P2,s2,loc)) . f) is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

d is V141() Element of the U2 of SCM+FSA

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . d is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . d is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

da is V141() Element of the U2 of SCM+FSA

f is V141() Element of the U2 of SCM+FSA

SubFrom (da,f) is ins-loc-free V105( the InstructionsF of SCM+FSA) V133(3, SCM+FSA ) V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (P1,(s1 +* (DataPart s2)),loc)) . f is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . f is V24() V25() integer ext-real set

(Exec ((CurInstr (P1,(Comput (P1,s1,loc)))),(Comput (P1,s1,loc)))) . (IC ) is set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . da is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . da is V24() V25() integer ext-real set

x is set

d is FinSeq-Location

(Comput (P1,s1,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,s1,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

(Comput (P1,s1,(loc + 1))) . x is set

(Comput (P1,s1,loc)) . da is V24() V25() integer ext-real set

(Comput (P1,s1,loc)) . f is V24() V25() integer ext-real set

((Comput (P1,s1,loc)) . da) - ((Comput (P1,s1,loc)) . f) is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . x is set

((Comput (P2,s2,loc)) . da) - ((Comput (P2,s2,loc)) . f) is V24() V25() integer ext-real set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

d is V141() Element of the U2 of SCM+FSA

(Comput (P1,s1,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P1,s1,loc)) . d is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . d is V24() V25() integer ext-real set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

x is set

d is FinSeq-Location

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,(s1 +* (DataPart s2)),loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . x is set

((Comput (P1,(s1 +* (DataPart s2)),loc)) . da) - ((Comput (P1,(s1 +* (DataPart s2)),loc)) . f) is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . x is set

((Comput (P2,s2,loc)) . da) - ((Comput (P2,s2,loc)) . f) is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

d is V141() Element of the U2 of SCM+FSA

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . d is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . d is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

da is V141() Element of the U2 of SCM+FSA

f is V141() Element of the U2 of SCM+FSA

MultBy (da,f) is ins-loc-free V105( the InstructionsF of SCM+FSA) V133(3, SCM+FSA ) V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (P1,(s1 +* (DataPart s2)),loc)) . f is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . f is V24() V25() integer ext-real set

(Exec ((CurInstr (P1,(Comput (P1,s1,loc)))),(Comput (P1,s1,loc)))) . (IC ) is set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . da is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . da is V24() V25() integer ext-real set

x is set

d is FinSeq-Location

(Comput (P1,s1,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,s1,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

(Comput (P1,s1,(loc + 1))) . x is set

(Comput (P1,s1,loc)) . da is V24() V25() integer ext-real set

(Comput (P1,s1,loc)) . f is V24() V25() integer ext-real set

((Comput (P1,s1,loc)) . da) * ((Comput (P1,s1,loc)) . f) is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . x is set

((Comput (P2,s2,loc)) . da) * ((Comput (P2,s2,loc)) . f) is V24() V25() integer ext-real set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

d is V141() Element of the U2 of SCM+FSA

(Comput (P1,s1,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P1,s1,loc)) . d is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . d is V24() V25() integer ext-real set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

x is set

d is FinSeq-Location

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,(s1 +* (DataPart s2)),loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . x is set

((Comput (P1,(s1 +* (DataPart s2)),loc)) . da) * ((Comput (P1,(s1 +* (DataPart s2)),loc)) . f) is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . x is set

((Comput (P2,s2,loc)) . da) * ((Comput (P2,s2,loc)) . f) is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

d is V141() Element of the U2 of SCM+FSA

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . d is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . d is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

da is V141() Element of the U2 of SCM+FSA

f is V141() Element of the U2 of SCM+FSA

Divide (da,f) is ins-loc-free V105( the InstructionsF of SCM+FSA) V133(3, SCM+FSA ) V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (P1,(s1 +* (DataPart s2)),loc)) . f is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . f is V24() V25() integer ext-real set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . da is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . da is V24() V25() integer ext-real set

(Exec ((CurInstr (P1,(Comput (P1,s1,loc)))),(Comput (P1,s1,loc)))) . (IC ) is set

x is set

d is FinSeq-Location

(Comput (P1,s1,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,s1,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P1,(s1 +* (DataPart s2)),loc)) . da) div ((Comput (P1,(s1 +* (DataPart s2)),loc)) . f) is V24() V25() integer ext-real set

(Comput (P1,s1,loc)) . da is V24() V25() integer ext-real set

(Comput (P1,s1,loc)) . f is V24() V25() integer ext-real set

((Comput (P1,s1,loc)) . da) div ((Comput (P1,s1,loc)) . f) is V24() V25() integer ext-real set

(Comput (P1,s1,(loc + 1))) . x is set

(Comput (P2,s2,(loc + 1))) . x is set

((Comput (P2,s2,loc)) . da) div ((Comput (P2,s2,loc)) . f) is V24() V25() integer ext-real set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

(Comput (P1,s1,(loc + 1))) . x is set

(Comput (P1,s1,loc)) . da is V24() V25() integer ext-real set

(Comput (P1,s1,loc)) . f is V24() V25() integer ext-real set

((Comput (P1,s1,loc)) . da) mod ((Comput (P1,s1,loc)) . f) is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . x is set

((Comput (P2,s2,loc)) . da) mod ((Comput (P2,s2,loc)) . f) is V24() V25() integer ext-real set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

d is V141() Element of the U2 of SCM+FSA

(Comput (P1,s1,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P1,s1,loc)) . d is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . d is V24() V25() integer ext-real set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

x is set

d is FinSeq-Location

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,(s1 +* (DataPart s2)),loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . x is set

((Comput (P1,(s1 +* (DataPart s2)),loc)) . da) div ((Comput (P1,(s1 +* (DataPart s2)),loc)) . f) is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . x is set

((Comput (P2,s2,loc)) . da) div ((Comput (P2,s2,loc)) . f) is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . x is set

((Comput (P1,(s1 +* (DataPart s2)),loc)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),loc)) . f) is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . x is set

((Comput (P2,s2,loc)) . da) mod ((Comput (P2,s2,loc)) . f) is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

d is V141() Element of the U2 of SCM+FSA

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . d is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . d is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

(Exec ((CurInstr (P1,(Comput (P1,s1,loc)))),(Comput (P1,s1,loc)))) . (IC ) is set

x is set

d is FinSeq-Location

(Comput (P1,s1,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,s1,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

(Comput (P2,s2,(loc + 1))) . x is set

((Comput (P1,s1,loc)) | (dom (DataPart p))) . x is set

(Comput (P1,s1,loc)) . x is set

((Comput (P2,s2,loc)) | (dom (DataPart p))) . x is set

(Comput (P2,s2,loc)) . x is set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

(Comput (P1,s1,(loc + 1))) . x is set

((Comput (P2,s2,loc)) . da) mod ((Comput (P2,s2,loc)) . f) is V24() V25() integer ext-real set

d is V141() Element of the U2 of SCM+FSA

(Comput (P1,s1,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P1,s1,loc)) . d is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . d is V24() V25() integer ext-real set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

x is set

d is FinSeq-Location

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,(s1 +* (DataPart s2)),loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . x is set

((Comput (P1,(s1 +* (DataPart s2)),loc)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),loc)) . f) is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . x is set

((Comput (P2,s2,loc)) . da) mod ((Comput (P2,s2,loc)) . f) is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

d is V141() Element of the U2 of SCM+FSA

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . d is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . d is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . d is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

da is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

goto da is V105( the InstructionsF of SCM+FSA) V133(3, SCM+FSA ) V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K514(da) is Element of the InstructionsF of K508()

da + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

goto (da + k) is V105( the InstructionsF of SCM+FSA) V133(3, SCM+FSA ) V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

K514((da + k)) is Element of the InstructionsF of K508()

f is set

(Comput (P2,s2,(loc + 1))) . f is set

(Comput (P2,s2,loc)) . f is set

(Comput (P1,s1,(loc + 1))) . f is set

(Comput (P1,s1,loc)) . f is set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . f is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . f is set

f is set

(Comput (P2,s2,(loc + 1))) . f is set

(Comput (P2,s2,loc)) . f is set

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . f is set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . f is set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . f is set

(DataPart (Comput (P2,s2,(loc + 1)))) . f is set

da is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

f is V141() Element of the U2 of SCM+FSA

f =0_goto da is V105( the InstructionsF of SCM+FSA) V133(3, SCM+FSA ) V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (P1,s1,loc)) . f is V24() V25() integer ext-real set

da + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(Comput (P1,s1,loc)) . f is V24() V25() integer ext-real set

succ (IC (Comput (P2,s2,loc))) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() set

(Comput (P1,s1,loc)) . f is V24() V25() integer ext-real set

da + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

succ (IC (Comput (P2,s2,loc))) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() set

(Comput (P1,s1,loc)) . f is V24() V25() integer ext-real set

da + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

succ (IC (Comput (P2,s2,loc))) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() set

f =0_goto (da + k) is V105( the InstructionsF of SCM+FSA) V133(3, SCM+FSA ) V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (P2,s2,loc)) . f is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . f is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . f is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . f is V24() V25() integer ext-real set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . f is V24() V25() integer ext-real set

x is set

(Comput (P2,s2,(loc + 1))) . x is set

(Comput (P2,s2,loc)) . x is set

(Comput (P1,s1,(loc + 1))) . x is set

(Comput (P1,s1,loc)) . x is set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

x is set

(Comput (P2,s2,(loc + 1))) . x is set

(Comput (P2,s2,loc)) . x is set

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . x is set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . x is set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

da is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

f is V141() Element of the U2 of SCM+FSA

f >0_goto da is V105( the InstructionsF of SCM+FSA) V133(3, SCM+FSA ) V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (P1,s1,loc)) . f is V24() V25() integer ext-real set

da + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(Comput (P1,s1,loc)) . f is V24() V25() integer ext-real set

succ (IC (Comput (P2,s2,loc))) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() set

(Comput (P1,s1,loc)) . f is V24() V25() integer ext-real set

da + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

succ (IC (Comput (P2,s2,loc))) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() set

(Comput (P1,s1,loc)) . f is V24() V25() integer ext-real set

da + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

succ (IC (Comput (P2,s2,loc))) is non empty epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real V92() set

f >0_goto (da + k) is V105( the InstructionsF of SCM+FSA) V133(3, SCM+FSA ) V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

(Comput (P2,s2,loc)) . f is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . f is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . f is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . f is V24() V25() integer ext-real set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . f is V24() V25() integer ext-real set

x is set

(Comput (P2,s2,(loc + 1))) . x is set

(Comput (P2,s2,loc)) . x is set

(Comput (P1,s1,(loc + 1))) . x is set

(Comput (P1,s1,loc)) . x is set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

x is set

(Comput (P2,s2,(loc + 1))) . x is set

(Comput (P2,s2,loc)) . x is set

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . x is set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . x is set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set

(DataPart (Comput (P2,s2,(loc + 1)))) . x is set

f is V141() Element of the U2 of SCM+FSA

da is V141() Element of the U2 of SCM+FSA

x is FinSeq-Location

f := (x,da) is ins-loc-free V105( the InstructionsF of SCM+FSA) V133(3, SCM+FSA ) V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

{} is set

<*f,x,da*> is non empty Relation-like NAT -defined Function-like finite V41(3) FinSequence-like FinSubsequence-like set

K15(9,{},<*f,x,da*>) is set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . x is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . x is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Exec ((CurInstr (P1,(Comput (P1,s1,loc)))),(Comput (P1,s1,loc)))) . (IC ) is set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . da is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . da is V24() V25() integer ext-real set

d is set

k2 is FinSeq-Location

(Comput (P1,s1,(loc + 1))) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,s1,loc)) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . d is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . d is set

(Comput (P1,s1,loc)) . da is V24() V25() integer ext-real set

abs ((Comput (P1,s1,loc)) . da) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(Comput (P1,s1,(loc + 1))) . d is set

(Comput (P1,s1,loc)) . x is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

k2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

((Comput (P1,s1,loc)) . x) /. k2 is V24() V25() integer ext-real Element of INT

abs ((Comput (P2,s2,loc)) . da) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(Comput (P2,s2,(loc + 1))) . d is set

k2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

((Comput (P2,s2,loc)) . x) /. k2 is V24() V25() integer ext-real Element of INT

((Comput (P1,(s1 +* (DataPart s2)),loc)) . x) /. k2 is V24() V25() integer ext-real Element of INT

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . d is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . d is set

k2 is V141() Element of the U2 of SCM+FSA

(Comput (P1,s1,(loc + 1))) . k2 is V24() V25() integer ext-real set

(Comput (P1,s1,loc)) . k2 is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . k2 is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . k2 is V24() V25() integer ext-real set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . d is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . d is set

d is set

k2 is FinSeq-Location

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,(s1 +* (DataPart s2)),loc)) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . d is set

(DataPart (Comput (P2,s2,(loc + 1)))) . d is set

abs ((Comput (P1,(s1 +* (DataPart s2)),loc)) . da) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . d is set

abs ((Comput (P2,s2,loc)) . da) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(Comput (P2,s2,(loc + 1))) . d is set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . d is set

(DataPart (Comput (P2,s2,(loc + 1)))) . d is set

k2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

((Comput (P2,s2,loc)) . x) /. k2 is V24() V25() integer ext-real Element of INT

k2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

((Comput (P1,(s1 +* (DataPart s2)),loc)) . x) /. k2 is V24() V25() integer ext-real Element of INT

k2 is V141() Element of the U2 of SCM+FSA

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . k2 is V24() V25() integer ext-real set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . k2 is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . k2 is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . k2 is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . d is set

(DataPart (Comput (P2,s2,(loc + 1)))) . d is set

f is V141() Element of the U2 of SCM+FSA

da is V141() Element of the U2 of SCM+FSA

x is FinSeq-Location

(x,da) := f is ins-loc-free V105( the InstructionsF of SCM+FSA) V133(3, SCM+FSA ) V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

{} is set

<*f,x,da*> is non empty Relation-like NAT -defined Function-like finite V41(3) FinSequence-like FinSubsequence-like set

K15(10,{},<*f,x,da*>) is set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . x is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . x is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Exec ((CurInstr (P1,(Comput (P1,s1,loc)))),(Comput (P1,s1,loc)))) . (IC ) is set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . f is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . f is V24() V25() integer ext-real set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . da is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . da is V24() V25() integer ext-real set

d is set

k2 is V141() Element of the U2 of SCM+FSA

(Comput (P1,s1,(loc + 1))) . k2 is V24() V25() integer ext-real set

(Comput (P1,s1,loc)) . k2 is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . k2 is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . k2 is V24() V25() integer ext-real set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . d is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . d is set

(Comput (P1,s1,loc)) . da is V24() V25() integer ext-real set

abs ((Comput (P1,s1,loc)) . da) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(Comput (P1,s1,(loc + 1))) . d is set

(Comput (P1,s1,loc)) . x is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,s1,loc)) . f is V24() V25() integer ext-real set

k2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

((Comput (P1,s1,loc)) . x) +* (k2,((Comput (P1,s1,loc)) . f)) is Relation-like Function-like set

abs ((Comput (P2,s2,loc)) . da) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(Comput (P2,s2,(loc + 1))) . d is set

k2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

((Comput (P2,s2,loc)) . x) +* (k2,((Comput (P2,s2,loc)) . f)) is Relation-like Function-like set

((Comput (P1,(s1 +* (DataPart s2)),loc)) . x) +* (k2,((Comput (P1,(s1 +* (DataPart s2)),loc)) . f)) is Relation-like Function-like set

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . d is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . d is set

k2 is FinSeq-Location

(Comput (P1,s1,(loc + 1))) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,s1,loc)) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . d is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . d is set

d is set

k2 is V141() Element of the U2 of SCM+FSA

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . k2 is V24() V25() integer ext-real set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . k2 is V24() V25() integer ext-real set

(Comput (P2,s2,(loc + 1))) . k2 is V24() V25() integer ext-real set

(Comput (P2,s2,loc)) . k2 is V24() V25() integer ext-real set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . d is set

(DataPart (Comput (P2,s2,(loc + 1)))) . d is set

abs ((Comput (P1,(s1 +* (DataPart s2)),loc)) . da) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . d is set

abs ((Comput (P2,s2,loc)) . da) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

(Comput (P2,s2,(loc + 1))) . d is set

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . d is set

(DataPart (Comput (P2,s2,(loc + 1)))) . d is set

k2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

((Comput (P2,s2,loc)) . x) +* (k2,((Comput (P2,s2,loc)) . f)) is Relation-like Function-like set

k2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT

((Comput (P1,(s1 +* (DataPart s2)),loc)) . x) +* (k2,((Comput (P1,(s1 +* (DataPart s2)),loc)) . f)) is Relation-like Function-like set

k2 is FinSeq-Location

(Comput (P1,(s1 +* (DataPart s2)),(loc + 1))) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,(s1 +* (DataPart s2)),loc)) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . k2 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . d is set

(DataPart (Comput (P2,s2,(loc + 1)))) . d is set

da is V141() Element of the U2 of SCM+FSA

f is FinSeq-Location

da :=len f is ins-loc-free V105( the InstructionsF of SCM+FSA) V133(3, SCM+FSA ) V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA

{} is set

<*da,f*> is non empty Relation-like NAT -defined Function-like finite V41(2) FinSequence-like FinSubsequence-like set

K15(11,{},<*da,f*>) is set

(Exec ((CurInstr (P1,(Comput (P1,s1,loc)))),(Comput (P1,s1,loc)))) . (IC ) is set

(Comput (P1,(s1 +* (DataPart s2)),loc)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

x is set

d is FinSeq-Location

(Comput (P1,s1,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P1,s1,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,(loc + 1))) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

(Comput (P2,s2,loc)) . d is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT

((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set

((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . x is set

len ((Comput (P1,(s1 +* (DataPart s2)),loc)) . f) is epsilon-transitive epsilon-connected