:: 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 ordinal natural V24() V25() integer ext-real Element of NAT
(Comput (P1,s1,loc)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len ((Comput (P1,s1,loc)) . f) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(Comput (P1,s1,(loc + 1))) . x is set
(Comput (P2,s2,(loc + 1))) . x is set
len ((Comput (P2,s2,loc)) . f) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
((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
len ((Comput (P1,(s1 +* (DataPart s2)),loc)) . f) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(Comput (P2,s2,(loc + 1))) . x is set
len ((Comput (P2,s2,loc)) . f) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(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 FinSeq-Location
f :=<0,...,0> 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
<*da,f*> is non empty Relation-like NAT -defined Function-like finite V41(2) FinSequence-like FinSubsequence-like set
K15(12,{},<*da,f*>) is 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 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
(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))) . x is set
d is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
d |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of d -tuples_on NAT
d -tuples_on NAT is FinSequenceSet of NAT
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))) . x is set
k2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
k2 |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of k2 -tuples_on NAT
k2 -tuples_on NAT is FinSequenceSet of NAT
((Comput (P1,s1,(loc + 1))) | (dom (DataPart p))) . x is set
((Comput (P2,s2,(loc + 1))) | (dom (DataPart p))) . 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
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
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))) . x 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))) . x is set
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(loc + 1)))) . x is set
(DataPart (Comput (P2,s2,(loc + 1)))) . x is set
d is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
d |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of d -tuples_on NAT
d -tuples_on NAT is FinSequenceSet of NAT
k2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
k2 |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of k2 -tuples_on NAT
k2 -tuples_on NAT is FinSequenceSet of NAT
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
dom (IncIC (p,k)) is set
Comput (P1,s1,0) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set
IC (Comput (P1,s1,0)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(Comput (P1,s1,0)) . (IC ) is set
(IC (Comput (P1,s1,0))) + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
IC s1 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
s1 . (IC ) is set
(IC s1) + k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
IC (IncIC (p,k)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(IncIC (p,k)) . (IC ) is set
IC s2 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
s2 . (IC ) is set
Comput (P2,s2,0) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set
IC (Comput (P2,s2,0)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(Comput (P2,s2,0)) . (IC ) is set
loc is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
dom q is set
dom (Reloc (q,k)) is set
q . (IC p) is set
P1 . (IC s1) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
dom P2 is set
CurInstr (P2,(Comput (P2,s2,0))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
P2 /. (IC (Comput (P2,s2,0))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
P2 . (IC (Comput (P2,s2,0))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
P2 . (IC s2) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
P2 . (IC (IncIC (p,k))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
P2 . ((IC p) + k) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(Reloc (q,k)) . ((IC p) + k) is set
dom P1 is set
CurInstr (P1,(Comput (P1,s1,0))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
P1 /. (IC (Comput (P1,s1,0))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
CurInstr (P1,s1) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
P1 /. (IC s1) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
DataPart (IncIC (p,k)) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set
(IncIC (p,k)) | (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
(Comput (P1,s1,0)) | (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
s1 | (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
s2 | (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,0)) | (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)),0) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set
DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set
(Comput (P1,(s1 +* (DataPart s2)),0)) | (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 (s1 +* (DataPart s2)) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set
(s1 +* (DataPart 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
DataPart (Comput (P2,s2,0)) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible set
(Comput (P2,s2,0)) | (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
q 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
s1 is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set
k is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
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
s2 is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set
P1 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Reloc (q,k) is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite non halt-free set
P2 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
s3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
Comput (P1,s1,s3) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set
CurInstr (P1,(Comput (P1,s1,s3))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
IC (Comput (P1,s1,s3)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(Comput (P1,s1,s3)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,s3))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
IncAddr ((CurInstr (P1,(Comput (P1,s1,s3)))),k) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
Comput (P2,s2,s3) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set
CurInstr (P2,(Comput (P2,s2,s3))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
IC (Comput (P2,s2,s3)) is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
(Comput (P2,s2,s3)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,s3))) is V137(3, SCM+FSA ) V139(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
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
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
s3 is epsilon-transitive epsilon-connected ordinal natural V24() V25() integer ext-real Element of NAT
Comput (P1,s1,s3) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set
(Comput (P1,s1,s3)) | (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,s3) is Relation-like the U2 of SCM+FSA -defined Function-like K447(3,SCM+FSA) -compatible total set
(Comput (P2,s2,s3)) | (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