:: SCMFSA_3 semantic presentation

REAL is set
NAT is non empty V5() V17() V18() V19() non finite V33() V34() Element of K32(REAL)
K32(REAL) is set
SCM+FSA is non empty V83(3) IC-Ins-separated strict V91(3) AMI-Struct over 3
3 is non empty V17() V18() V19() V23() V24() V25() integer finite V33() V64() ext-real positive Element of NAT
K505() is set
K517(NAT,K505()) is Element of K505()
K498() is non empty set
K508() is Relation-like Function-like V40(K505(),3) Element of K32(K33(K505(),3))
K33(K505(),3) is Relation-like set
K32(K33(K505(),3)) is set
K509() is Relation-like 3 -defined Function-like total set
K516() is Relation-like Function-like V40(K498(),K170(K198((K508() * K509())),K198((K508() * K509())))) Element of K32(K33(K498(),K170(K198((K508() * K509())),K198((K508() * K509())))))
K508() * K509() is Relation-like Function-like set
K198((K508() * K509())) is set
K170(K198((K508() * K509())),K198((K508() * K509()))) is set
K33(K498(),K170(K198((K508() * K509())),K198((K508() * K509())))) is Relation-like set
K32(K33(K498(),K170(K198((K508() * K509())),K198((K508() * K509()))))) is set
AMI-Struct(# K505(),K517(NAT,K505()),K498(),K508(),K509(),K516() #) is strict AMI-Struct over 3
the carrier of SCM+FSA is non empty set
COMPLEX is set
NAT is non empty V5() V17() V18() V19() non finite V33() V34() set
K32(NAT) is V5() non finite set
K32(NAT) is V5() non finite set
9 is non empty V17() V18() V19() V23() V24() V25() integer finite V33() V64() ext-real positive Element of NAT
K144(9) is Element of K32(NAT)
Int-Locations is set
1 is non empty V17() V18() V19() V23() V24() V25() integer finite V33() V64() ext-real positive Element of NAT
K80(NAT,1) is non empty V5() finite V32() V35(1) Element of K32(NAT)
K66(NAT,REAL,K80(NAT,1),NAT) is V5() Relation-like non finite Element of K32(K33(NAT,REAL))
K33(NAT,REAL) is Relation-like set
K32(K33(NAT,REAL)) is set
K216() is set
K32(K216()) is set
2 is non empty V17() V18() V19() V23() V24() V25() integer finite V33() V64() ext-real positive Element of NAT
K33(K216(),2) is Relation-like set
K32(K33(K216(),2)) is set
K218() is Relation-like Function-like V40(K216(),2) Element of K32(K33(K216(),2))
K219() is Relation-like 2 -defined Function-like total set
K218() * K219() is Relation-like Function-like set
K198((K218() * K219())) is set
K210() is non empty set
K170(K198((K218() * K219())),K198((K218() * K219()))) is set
K33(K210(),K170(K198((K218() * K219())),K198((K218() * K219())))) is Relation-like set
K32(K33(K210(),K170(K198((K218() * K219())),K198((K218() * K219()))))) is set
K340() is non empty V83(2) IC-Ins-separated strict strict V91(2) AMI-Struct over 2
the InstructionsF of K340() is V72() V73() V74() V76() set
the carrier of K340() is non empty set
K304(2,K340()) is Relation-like non-empty the carrier of K340() -defined Function-like total set
the Object-Kind of K340() is Relation-like Function-like V40( the carrier of K340(),2) Element of K32(K33( the carrier of K340(),2))
K33( the carrier of K340(),2) is Relation-like set
K32(K33( the carrier of K340(),2)) is set
the U7 of K340() is Relation-like 2 -defined Function-like total set
the Object-Kind of K340() * the U7 of K340() is Relation-like Function-like set
K32( the carrier of SCM+FSA) is set
the InstructionsF of SCM+FSA is V72() V73() V74() V76() set
INT is set
RAT is set
{} is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() V25() integer finite finite-yielding V32() V33() V35( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V95() ext-real set
K497() is set
K32(K505()) is set
K304(3,SCM+FSA) is Relation-like non-empty the carrier of SCM+FSA -defined Function-like total set
the Object-Kind of SCM+FSA is Relation-like Function-like V40( the carrier of SCM+FSA,3) Element of K32(K33( the carrier of SCM+FSA,3))
K33( the carrier of SCM+FSA,3) is Relation-like set
K32(K33( the carrier 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
0 is empty Relation-like non-empty empty-yielding NAT -defined Function-like one-to-one constant functional V17() V18() V19() V21() V22() V23() V24() V25() integer finite finite-yielding V32() V33() V35( {} ) FinSequence-like FinSubsequence-like FinSequence-membered Function-yielding V95() ext-real Element of NAT
K507() is Element of K32(K505())
IC is V51( SCM+FSA ) Element of the carrier of SCM+FSA
NonZero SCM+FSA is Element of K32( the carrier of SCM+FSA)
Int-Locations is Element of K32( the carrier of SCM+FSA)
FinSeq-Locations is V5() non finite Element of K32( the carrier of SCM+FSA)
Int-Locations \/ FinSeq-Locations is Element of K32( the carrier of SCM+FSA)
K217() is Element of K32(K216())
q is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
p is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Start-At (p,SCM+FSA) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite p -started set
(IC ) .--> p is V5() Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued Function-like one-to-one constant finite set
{(IC )} is non empty V5() finite V35(1) set
{(IC )} --> p is non empty Relation-like {(IC )} -defined NAT -valued Function-like constant finite total V40({(IC )},{p}) Element of K32(K33({(IC )},{p}))
{p} is non empty V5() finite V32() V35(1) set
K33({(IC )},{p}) is Relation-like finite set
K32(K33({(IC )},{p})) is finite V32() set
q +* (Start-At (p,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible K304(3,SCM+FSA) -compatible total p -started set
s1 is V63() Element of the carrier of SCM+FSA
q . s1 is V24() V25() integer ext-real set
(q +* (Start-At (p,SCM+FSA))) . s1 is V24() V25() integer ext-real set
dom q is set
dom (Start-At (p,SCM+FSA)) is non empty finite set
(dom q) \/ (dom (Start-At (p,SCM+FSA))) is non empty set
q is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
p is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Start-At (p,SCM+FSA) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite p -started set
(IC ) .--> p is V5() Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued Function-like one-to-one constant finite set
{(IC )} is non empty V5() finite V35(1) set
{(IC )} --> p is non empty Relation-like {(IC )} -defined NAT -valued Function-like constant finite total V40({(IC )},{p}) Element of K32(K33({(IC )},{p}))
{p} is non empty V5() finite V32() V35(1) set
K33({(IC )},{p}) is Relation-like finite set
K32(K33({(IC )},{p})) is finite V32() set
q +* (Start-At (p,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible K304(3,SCM+FSA) -compatible total p -started set
s1 is FinSeq-Location
q . s1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(q +* (Start-At (p,SCM+FSA))) . s1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
dom q is set
dom (Start-At (p,SCM+FSA)) is non empty finite set
(dom q) \/ (dom (Start-At (p,SCM+FSA))) is non empty set
q is V63() Element of the carrier of SCM+FSA
p is V24() V25() integer ext-real set
q .--> p is V5() Relation-like the carrier of SCM+FSA -defined {q} -defined Function-like one-to-one constant finite set
{q} is non empty V5() finite V35(1) set
{q} --> p is non empty Relation-like {q} -defined Function-like constant finite total V40({q},{p}) Element of K32(K33({q},{p}))
{p} is non empty V5() finite V35(1) set
K33({q},{p}) is Relation-like finite set
K32(K33({q},{p})) is finite V32() set
Values q is non empty set
K304(3,SCM+FSA) . q is set
q is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite non halt-free set
p is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite q -autonomic set
DataPart p is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite data-only set
p | (NonZero SCM+FSA) is Relation-like NonZero SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
dom p is finite set
dom (DataPart p) is finite set
{(IC )} is non empty V5() finite V35(1) set
dom q is finite set
NAT \ (dom q) is Element of K32(REAL)
the Element of NAT \ (dom q) is Element of NAT \ (dom q)
Int-Locations \ (dom p) is Element of K32( the carrier of SCM+FSA)
the Element of Int-Locations \ (dom p) is Element of Int-Locations \ (dom p)
the Element of dom (DataPart p) is Element of dom (DataPart p)
da is Element of the carrier of SCM+FSA
i is V63() Element of the carrier of SCM+FSA
(i,0) is V5() Relation-like the carrier of SCM+FSA -defined {i} -defined NAT -valued Function-like one-to-one constant K304(3,SCM+FSA) -compatible finite data-only Function-yielding V95() set
{i} is non empty V5() finite V35(1) set
{i} --> 0 is non empty Relation-like {i} -defined NAT -valued Function-like constant finite total V40({i},{0}) Function-yielding V95() Element of K32(K33({i},{0}))
{0} is non empty V5() functional finite V32() V35(1) set
K33({i},{0}) is Relation-like finite set
K32(K33({i},{0})) is finite V32() set
P2 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Start-At (P2,SCM+FSA) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite P2 -started set
(IC ) .--> P2 is V5() Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued Function-like one-to-one constant finite set
{(IC )} --> P2 is non empty Relation-like {(IC )} -defined NAT -valued Function-like constant finite total V40({(IC )},{P2}) Element of K32(K33({(IC )},{P2}))
{P2} is non empty V5() finite V32() V35(1) set
K33({(IC )},{P2}) is Relation-like finite set
K32(K33({(IC )},{P2})) is finite V32() set
(i,0) +* (Start-At (P2,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible K304(3,SCM+FSA) -compatible finite P2 -started set
p +* ((i,0) +* (Start-At (P2,SCM+FSA))) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible K304(3,SCM+FSA) -compatible finite P2 -started set
(i,1) is V5() Relation-like the carrier of SCM+FSA -defined {i} -defined NAT -valued Function-like one-to-one constant K304(3,SCM+FSA) -compatible finite data-only set
{i} --> 1 is non empty Relation-like non-empty {i} -defined NAT -valued Function-like constant finite total V40({i},{1}) Element of K32(K33({i},{1}))
{1} is non empty V5() finite V32() V35(1) set
K33({i},{1}) is Relation-like finite set
K32(K33({i},{1})) is finite V32() set
(i,1) +* (Start-At (P2,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible K304(3,SCM+FSA) -compatible finite P2 -started set
p +* ((i,1) +* (Start-At (P2,SCM+FSA))) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible K304(3,SCM+FSA) -compatible finite P2 -started set
f is V63() Element of the carrier of SCM+FSA
f := i is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
P2 .--> (f := i) is V5() Relation-like NAT -defined {P2} -defined Function-like one-to-one constant finite set
{P2} --> (f := i) is non empty Relation-like {P2} -defined Function-like constant finite total V40({P2},{(f := i)}) Element of K32(K33({P2},{(f := i)}))
{(f := i)} is non empty V5() finite V35(1) set
K33({P2},{(f := i)}) is Relation-like finite set
K32(K33({P2},{(f := i)})) is finite V32() set
q +* (P2 .--> (f := i)) is Relation-like NAT -defined Function-like finite set
I is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
i1 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
i2 is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
i2 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Cs2k is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
k is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
dom (P2 .--> (f := i)) is V5() finite set
dom ((i,0) +* (Start-At (P2,SCM+FSA))) is non empty finite set
dom (i,0) is V5() finite set
dom (Start-At (P2,SCM+FSA)) is non empty finite set
(dom (i,0)) \/ (dom (Start-At (P2,SCM+FSA))) is non empty finite set
(dom (i,0)) \/ {(IC )} is non empty finite set
{i} \/ {(IC )} is non empty finite set
(dom p) /\ (dom ((i,0) +* (Start-At (P2,SCM+FSA)))) is finite set
(dom p) /\ {i} is finite set
(dom p) /\ {(IC )} is finite set
((dom p) /\ {i}) \/ ((dom p) /\ {(IC )}) is finite set
((dom p) /\ {i}) \/ {} is finite set
dom ((i,1) +* (Start-At (P2,SCM+FSA))) is non empty finite set
dom (i,1) is V5() finite set
(dom (i,1)) \/ (dom (Start-At (P2,SCM+FSA))) is non empty finite set
(dom (i,1)) \/ {(IC )} is non empty finite set
(dom p) /\ (dom ((i,1) +* (Start-At (P2,SCM+FSA)))) is finite set
Comput (Cs2k,I,1) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
(Comput (Cs2k,I,1)) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
Comput (k,i2,1) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
(Comput (k,i2,1)) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
Comput (i2,i2,1) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
dom (Comput (i2,i2,1)) is set
(Comput (i2,i2,1)) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
dom ((Comput (i2,i2,1)) | (dom p)) is finite set
dom (p +* ((i,0) +* (Start-At (P2,SCM+FSA)))) is non empty finite set
(dom p) \/ (dom ((i,0) +* (Start-At (P2,SCM+FSA)))) is non empty finite set
IC I is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
I . (IC ) is set
(p +* ((i,0) +* (Start-At (P2,SCM+FSA)))) . (IC ) is set
((i,0) +* (Start-At (P2,SCM+FSA))) . (IC ) is set
(Start-At (P2,SCM+FSA)) . (IC ) is set
I . i is V24() V25() integer ext-real set
(p +* ((i,0) +* (Start-At (P2,SCM+FSA)))) . i is set
((i,0) +* (Start-At (P2,SCM+FSA))) . i is set
(i,0) . i is Relation-like Function-like set
dom (q +* (P2 .--> (f := i))) is finite set
(dom q) \/ (dom (P2 .--> (f := i))) is finite set
i1 . P2 is Element of the InstructionsF of SCM+FSA
(q +* (P2 .--> (f := i))) . P2 is set
(P2 .--> (f := i)) . P2 is set
Comput (i1,I,1) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
dom (Comput (i1,I,1)) is set
(Comput (i1,I,1)) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
dom ((Comput (i1,I,1)) | (dom p)) is finite set
dom (p +* ((i,1) +* (Start-At (P2,SCM+FSA)))) is non empty finite set
(dom p) \/ (dom ((i,1) +* (Start-At (P2,SCM+FSA)))) is non empty finite set
IC i2 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
i2 . (IC ) is set
(p +* ((i,1) +* (Start-At (P2,SCM+FSA)))) . (IC ) is set
((i,1) +* (Start-At (P2,SCM+FSA))) . (IC ) is set
i2 . i is V24() V25() integer ext-real set
(p +* ((i,1) +* (Start-At (P2,SCM+FSA)))) . i is set
((i,1) +* (Start-At (P2,SCM+FSA))) . i is set
(i,1) . i is set
i2 . P2 is Element of the InstructionsF of SCM+FSA
i2 /. (IC i2) is Element of the InstructionsF of SCM+FSA
i2 . (IC i2) is Element of the InstructionsF of SCM+FSA
0 + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (i2,i2,(0 + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
(Comput (i2,i2,(0 + 1))) . f is V24() V25() integer ext-real set
Comput (i2,i2,0) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Following (i2,(Comput (i2,i2,0))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (i2,(Comput (i2,i2,0))) is Element of the InstructionsF of SCM+FSA
IC (Comput (i2,i2,0)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (i2,i2,0)) . (IC ) is set
i2 /. (IC (Comput (i2,i2,0))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i2,(Comput (i2,i2,0)))),(Comput (i2,i2,0))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,(Comput (i2,i2,0))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,(Comput (i2,i2,0))))) . (Comput (i2,i2,0)) is set
(Following (i2,(Comput (i2,i2,0)))) . f is V24() V25() integer ext-real set
Following (i2,i2) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (i2,i2) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i2,i2)),i2) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,i2))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i2,i2))) . i2 is set
(Following (i2,i2)) . f is V24() V25() integer ext-real set
i1 /. (IC I) is Element of the InstructionsF of SCM+FSA
i1 . (IC I) is Element of the InstructionsF of SCM+FSA
Comput (i1,I,(0 + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
(Comput (i1,I,(0 + 1))) . f is V24() V25() integer ext-real set
Comput (i1,I,0) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Following (i1,(Comput (i1,I,0))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (i1,(Comput (i1,I,0))) is Element of the InstructionsF of SCM+FSA
IC (Comput (i1,I,0)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (i1,I,0)) . (IC ) is set
i1 /. (IC (Comput (i1,I,0))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i1,(Comput (i1,I,0)))),(Comput (i1,I,0))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,(Comput (i1,I,0))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,(Comput (i1,I,0))))) . (Comput (i1,I,0)) is set
(Following (i1,(Comput (i1,I,0)))) . f is V24() V25() integer ext-real set
Following (i1,I) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (i1,I) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i1,I)),I) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,I))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,I))) . I is set
(Following (i1,I)) . f is V24() V25() integer ext-real set
((Comput (i1,I,1)) | (dom p)) . f is set
da is Element of the carrier of SCM+FSA
i is V63() Element of the carrier of SCM+FSA
(i,0) is V5() Relation-like the carrier of SCM+FSA -defined {i} -defined NAT -valued Function-like one-to-one constant K304(3,SCM+FSA) -compatible finite data-only Function-yielding V95() set
{i} is non empty V5() finite V35(1) set
{i} --> 0 is non empty Relation-like {i} -defined NAT -valued Function-like constant finite total V40({i},{0}) Function-yielding V95() Element of K32(K33({i},{0}))
{0} is non empty V5() functional finite V32() V35(1) set
K33({i},{0}) is Relation-like finite set
K32(K33({i},{0})) is finite V32() set
P2 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Start-At (P2,SCM+FSA) is non empty Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite P2 -started set
(IC ) .--> P2 is V5() Relation-like the carrier of SCM+FSA -defined {(IC )} -defined NAT -valued Function-like one-to-one constant finite set
{(IC )} --> P2 is non empty Relation-like {(IC )} -defined NAT -valued Function-like constant finite total V40({(IC )},{P2}) Element of K32(K33({(IC )},{P2}))
{P2} is non empty V5() finite V32() V35(1) set
K33({(IC )},{P2}) is Relation-like finite set
K32(K33({(IC )},{P2})) is finite V32() set
(i,0) +* (Start-At (P2,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible K304(3,SCM+FSA) -compatible finite P2 -started set
p +* ((i,0) +* (Start-At (P2,SCM+FSA))) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible K304(3,SCM+FSA) -compatible finite P2 -started set
(i,1) is V5() Relation-like the carrier of SCM+FSA -defined {i} -defined NAT -valued Function-like one-to-one constant K304(3,SCM+FSA) -compatible finite data-only set
{i} --> 1 is non empty Relation-like non-empty {i} -defined NAT -valued Function-like constant finite total V40({i},{1}) Element of K32(K33({i},{1}))
{1} is non empty V5() finite V32() V35(1) set
K33({i},{1}) is Relation-like finite set
K32(K33({i},{1})) is finite V32() set
(i,1) +* (Start-At (P2,SCM+FSA)) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible K304(3,SCM+FSA) -compatible finite P2 -started set
p +* ((i,1) +* (Start-At (P2,SCM+FSA))) is non empty Relation-like the carrier of SCM+FSA -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible K304(3,SCM+FSA) -compatible finite P2 -started set
f is FinSeq-Location
f :=<0,...,0> i is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
12 is non empty V17() V18() V19() V23() V24() V25() integer finite V33() V64() ext-real positive Element of NAT
<*i,f*> is non empty Relation-like NAT -defined Function-like finite V35(2) FinSequence-like FinSubsequence-like set
K15(12,{},<*i,f*>) is set
P2 .--> (f :=<0,...,0> i) is V5() Relation-like NAT -defined {P2} -defined Function-like one-to-one constant finite set
{P2} --> (f :=<0,...,0> i) is non empty Relation-like {P2} -defined Function-like constant finite total V40({P2},{(f :=<0,...,0> i)}) Element of K32(K33({P2},{(f :=<0,...,0> i)}))
{(f :=<0,...,0> i)} is non empty V5() finite V35(1) set
K33({P2},{(f :=<0,...,0> i)}) is Relation-like finite set
K32(K33({P2},{(f :=<0,...,0> i)})) is finite V32() set
q +* (P2 .--> (f :=<0,...,0> i)) is Relation-like NAT -defined Function-like finite set
I is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
i1 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
dom ((i,0) +* (Start-At (P2,SCM+FSA))) is non empty finite set
dom (i,0) is V5() finite set
dom (Start-At (P2,SCM+FSA)) is non empty finite set
(dom (i,0)) \/ (dom (Start-At (P2,SCM+FSA))) is non empty finite set
I . i is V24() V25() integer ext-real set
abs (I . i) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Exec ((f :=<0,...,0> i),I) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(f :=<0,...,0> i)) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(f :=<0,...,0> i)) . I is set
(Exec ((f :=<0,...,0> i),I)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
i2 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
i2 |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of i2 -tuples_on NAT
i2 -tuples_on NAT is FinSequenceSet of NAT
dom (p +* ((i,0) +* (Start-At (P2,SCM+FSA)))) is non empty finite set
(dom p) \/ (dom ((i,0) +* (Start-At (P2,SCM+FSA)))) is non empty finite set
dom (q +* (P2 .--> (f :=<0,...,0> i))) is finite set
dom (P2 .--> (f :=<0,...,0> i)) is V5() finite set
(dom q) \/ (dom (P2 .--> (f :=<0,...,0> i))) is finite set
IC I is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
I . (IC ) is set
(p +* ((i,0) +* (Start-At (P2,SCM+FSA)))) . (IC ) is set
((i,0) +* (Start-At (P2,SCM+FSA))) . (IC ) is set
(Start-At (P2,SCM+FSA)) . (IC ) is set
i2 is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Cs2k is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
(p +* ((i,0) +* (Start-At (P2,SCM+FSA)))) . i is set
((i,0) +* (Start-At (P2,SCM+FSA))) . i is set
(i,0) . i is Relation-like Function-like set
0 |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of 0 -tuples_on NAT
0 -tuples_on NAT is FinSequenceSet of NAT
i1 . P2 is Element of the InstructionsF of SCM+FSA
(q +* (P2 .--> (f :=<0,...,0> i))) . P2 is set
(P2 .--> (f :=<0,...,0> i)) . P2 is set
Comput (i1,I,1) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
dom (Comput (i1,I,1)) is set
(Comput (i1,I,1)) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
dom ((Comput (i1,I,1)) | (dom p)) is finite set
i2 . i is V24() V25() integer ext-real set
abs (i2 . i) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Exec ((f :=<0,...,0> i),i2) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(f :=<0,...,0> i)) . i2 is set
(Exec ((f :=<0,...,0> i),i2)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
k is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
k |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of k -tuples_on NAT
k -tuples_on NAT is FinSequenceSet of NAT
dom (p +* ((i,1) +* (Start-At (P2,SCM+FSA)))) is non empty finite set
dom ((i,1) +* (Start-At (P2,SCM+FSA))) is non empty finite set
(dom p) \/ (dom ((i,1) +* (Start-At (P2,SCM+FSA)))) is non empty finite set
P is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Q is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
(dom (i,0)) \/ {(IC )} is non empty finite set
{i} \/ {(IC )} is non empty finite set
(dom p) /\ (dom ((i,0) +* (Start-At (P2,SCM+FSA)))) is finite set
(dom p) /\ {i} is finite set
(dom p) /\ {(IC )} is finite set
((dom p) /\ {i}) \/ ((dom p) /\ {(IC )}) is finite set
((dom p) /\ {i}) \/ {} is finite set
dom (i,1) is V5() finite set
(dom (i,1)) \/ (dom (Start-At (P2,SCM+FSA))) is non empty finite set
(dom (i,1)) \/ {(IC )} is non empty finite set
(dom p) /\ (dom ((i,1) +* (Start-At (P2,SCM+FSA)))) is finite set
Comput (P,I,1) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
(Comput (P,I,1)) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
Comput (Q,i2,1) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
(Comput (Q,i2,1)) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
IC i2 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
i2 . (IC ) is set
(p +* ((i,1) +* (Start-At (P2,SCM+FSA)))) . (IC ) is set
((i,1) +* (Start-At (P2,SCM+FSA))) . (IC ) is set
(p +* ((i,1) +* (Start-At (P2,SCM+FSA)))) . i is set
((i,1) +* (Start-At (P2,SCM+FSA))) . i is set
(i,1) . i is set
1 |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of 1 -tuples_on NAT
1 -tuples_on NAT is FinSequenceSet of NAT
<*0*> is non empty V5() Relation-like NAT -defined NAT -valued Function-like constant finite V35(1) FinSequence-like FinSubsequence-like FinSequence of NAT
Cs2k . P2 is Element of the InstructionsF of SCM+FSA
0 + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (Cs2k,i2,(0 + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
(Comput (Cs2k,i2,(0 + 1))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Comput (Cs2k,i2,0) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Following (Cs2k,(Comput (Cs2k,i2,0))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (Cs2k,(Comput (Cs2k,i2,0))) is Element of the InstructionsF of SCM+FSA
IC (Comput (Cs2k,i2,0)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (Cs2k,i2,0)) . (IC ) is set
Cs2k /. (IC (Comput (Cs2k,i2,0))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (Cs2k,(Comput (Cs2k,i2,0)))),(Comput (Cs2k,i2,0))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (Cs2k,(Comput (Cs2k,i2,0))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (Cs2k,(Comput (Cs2k,i2,0))))) . (Comput (Cs2k,i2,0)) is set
(Following (Cs2k,(Comput (Cs2k,i2,0)))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Following (Cs2k,i2) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (Cs2k,i2) is Element of the InstructionsF of SCM+FSA
Cs2k /. (IC i2) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (Cs2k,i2)),i2) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (Cs2k,i2))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (Cs2k,i2))) . i2 is set
(Following (Cs2k,i2)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Comput (Cs2k,i2,1) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
dom (Comput (Cs2k,i2,1)) is set
(Comput (Cs2k,i2,1)) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
dom ((Comput (Cs2k,i2,1)) | (dom p)) is finite set
Comput (i1,I,(0 + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
(Comput (i1,I,(0 + 1))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Comput (i1,I,0) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Following (i1,(Comput (i1,I,0))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (i1,(Comput (i1,I,0))) is Element of the InstructionsF of SCM+FSA
IC (Comput (i1,I,0)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (i1,I,0)) . (IC ) is set
i1 /. (IC (Comput (i1,I,0))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i1,(Comput (i1,I,0)))),(Comput (i1,I,0))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,(Comput (i1,I,0))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,(Comput (i1,I,0))))) . (Comput (i1,I,0)) is set
(Following (i1,(Comput (i1,I,0)))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Following (i1,I) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (i1,I) is Element of the InstructionsF of SCM+FSA
i1 /. (IC I) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (i1,I)),I) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,I))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (i1,I))) . I is set
(Following (i1,I)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
((Comput (i1,I,1)) | (dom p)) . f is set
da is Element of the carrier of SCM+FSA
q is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like finite non halt-free set
dom q is finite set
p is non empty Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite q -autonomic set
s1 is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
s2 is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
P1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (s2,s1,P1) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
IC (Comput (s2,s1,P1)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (s2,s1,P1)) . (IC ) is set
(IC (Comput (s2,s1,P1))) + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
intloc 0 is V63() Element of the carrier of SCM+FSA
K349(0) is V63() Element of the carrier of K340()
(intloc 0) := (intloc 0) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(IC (Comput (s2,s1,P1))) .--> ((intloc 0) := (intloc 0)) is V5() Relation-like NAT -defined {(IC (Comput (s2,s1,P1)))} -defined Function-like one-to-one constant finite set
{(IC (Comput (s2,s1,P1)))} is non empty V5() finite V32() V35(1) set
{(IC (Comput (s2,s1,P1)))} --> ((intloc 0) := (intloc 0)) is non empty Relation-like {(IC (Comput (s2,s1,P1)))} -defined Function-like constant finite total V40({(IC (Comput (s2,s1,P1)))},{((intloc 0) := (intloc 0))}) Element of K32(K33({(IC (Comput (s2,s1,P1)))},{((intloc 0) := (intloc 0))}))
{((intloc 0) := (intloc 0))} is non empty V5() finite V35(1) set
K33({(IC (Comput (s2,s1,P1)))},{((intloc 0) := (intloc 0))}) is Relation-like finite set
K32(K33({(IC (Comput (s2,s1,P1)))},{((intloc 0) := (intloc 0))})) is finite V32() set
q +* ((IC (Comput (s2,s1,P1))) .--> ((intloc 0) := (intloc 0))) is Relation-like NAT -defined Function-like finite set
halt SCM+FSA is V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(IC (Comput (s2,s1,P1))) .--> (halt SCM+FSA) is V5() Relation-like NAT -defined {(IC (Comput (s2,s1,P1)))} -defined Function-like one-to-one constant finite set
{(IC (Comput (s2,s1,P1)))} --> (halt SCM+FSA) is non empty Relation-like {(IC (Comput (s2,s1,P1)))} -defined Function-like constant finite total V40({(IC (Comput (s2,s1,P1)))},{(halt SCM+FSA)}) Element of K32(K33({(IC (Comput (s2,s1,P1)))},{(halt SCM+FSA)}))
{(halt SCM+FSA)} is non empty V5() finite V35(1) set
K33({(IC (Comput (s2,s1,P1)))},{(halt SCM+FSA)}) is Relation-like finite set
K32(K33({(IC (Comput (s2,s1,P1)))},{(halt SCM+FSA)})) is finite V32() set
q +* ((IC (Comput (s2,s1,P1))) .--> (halt SCM+FSA)) is Relation-like NAT -defined Function-like finite set
s2 +* ((IC (Comput (s2,s1,P1))) .--> ((intloc 0) := (intloc 0))) is Relation-like NAT -defined Function-like total set
s2 +* ((IC (Comput (s2,s1,P1))) .--> (halt SCM+FSA)) is Relation-like NAT -defined Function-like total set
dom ((IC (Comput (s2,s1,P1))) .--> (halt SCM+FSA)) is V5() finite set
dom ((IC (Comput (s2,s1,P1))) .--> ((intloc 0) := (intloc 0))) is V5() finite set
Cs2i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Cs1i is Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like total set
Comput (Cs1i,s1,P1) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Comput (Cs2i,s1,P1) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
((IC (Comput (s2,s1,P1))) .--> (halt SCM+FSA)) . (IC (Comput (s2,s1,P1))) is set
Cs1i . (IC (Comput (s2,s1,P1))) is Element of the InstructionsF of SCM+FSA
((IC (Comput (s2,s1,P1))) .--> ((intloc 0) := (intloc 0))) . (IC (Comput (s2,s1,P1))) is set
dom p is non empty finite set
(Comput (Cs2i,s1,P1)) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
(Comput (s2,s1,P1)) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
(Comput (Cs1i,s1,P1)) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
P1 + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
i2 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (Cs2i,s1,i2) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
(Comput (Cs2i,s1,i2)) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
Comput (Cs1i,s1,i2) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
(Comput (Cs1i,s1,i2)) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
IC ((Comput (s2,s1,P1)) | (dom p)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
((Comput (s2,s1,P1)) | (dom p)) . (IC ) is set
IC (Comput (Cs2i,s1,P1)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (Cs2i,s1,P1)) . (IC ) is set
CurInstr (Cs2i,(Comput (Cs2i,s1,P1))) is Element of the InstructionsF of SCM+FSA
Cs2i /. (IC (Comput (Cs2i,s1,P1))) is Element of the InstructionsF of SCM+FSA
Cs2i . (IC (Comput (s2,s1,P1))) is Element of the InstructionsF of SCM+FSA
Following (Cs2i,(Comput (Cs2i,s1,P1))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Exec ((CurInstr (Cs2i,(Comput (Cs2i,s1,P1)))),(Comput (Cs2i,s1,P1))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (Cs2i,(Comput (Cs2i,s1,P1))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (Cs2i,(Comput (Cs2i,s1,P1))))) . (Comput (Cs2i,s1,P1)) is set
Exec (((intloc 0) := (intloc 0)),(Comput (Cs2i,s1,P1))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,((intloc 0) := (intloc 0))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,((intloc 0) := (intloc 0))) . (Comput (Cs2i,s1,P1)) is set
IC (Exec (((intloc 0) := (intloc 0)),(Comput (Cs2i,s1,P1)))) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Exec (((intloc 0) := (intloc 0)),(Comput (Cs2i,s1,P1)))) . (IC ) is set
succ (IC (Comput (Cs2i,s1,P1))) is non empty V17() V18() V19() V23() V24() V25() integer finite V33() V64() ext-real set
IC (Comput (Cs2i,s1,i2)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (Cs2i,s1,i2)) . (IC ) is set
succ (IC (Comput (s2,s1,P1))) is non empty V17() V18() V19() V23() V24() V25() integer finite V33() V64() ext-real set
Following (Cs1i,(Comput (Cs1i,s1,P1))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (Cs1i,(Comput (Cs1i,s1,P1))) is Element of the InstructionsF of SCM+FSA
IC (Comput (Cs1i,s1,P1)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (Cs1i,s1,P1)) . (IC ) is set
Cs1i /. (IC (Comput (Cs1i,s1,P1))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (Cs1i,(Comput (Cs1i,s1,P1)))),(Comput (Cs1i,s1,P1))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (Cs1i,(Comput (Cs1i,s1,P1))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (Cs1i,(Comput (Cs1i,s1,P1))))) . (Comput (Cs1i,s1,P1)) is set
Cs1i . (IC (Comput (Cs1i,s1,P1))) is Element of the InstructionsF of SCM+FSA
IC (Comput (Cs1i,s1,i2)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (Cs1i,s1,i2)) . (IC ) is set
IC ((Comput (Cs2i,s1,i2)) | (dom p)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
((Comput (Cs2i,s1,i2)) | (dom p)) . (IC ) is set
IC ((Comput (Cs1i,s1,i2)) | (dom p)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
((Comput (Cs1i,s1,i2)) | (dom p)) . (IC ) is 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 carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite q -autonomic set
dom p is non empty finite set
s1 is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
s2 is Relation-like the carrier of SCM+FSA -defined Function-like K304(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
i is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
Comput (P2,s2,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
da is V63() Element of the carrier of SCM+FSA
f is V63() Element of the carrier of SCM+FSA
da := f is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(Comput (P1,s1,i)) . f is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . f is V24() V25() integer ext-real set
i + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
((Comput (P1,s1,(i + 1))) | (dom p)) . da is set
(Comput (P1,s1,(i + 1))) . da is V24() V25() integer ext-real set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
((Comput (P2,s2,(i + 1))) | (dom p)) . da is set
(Comput (P2,s2,(i + 1))) . da is V24() V25() integer ext-real set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is 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 carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite q -autonomic set
dom p is non empty finite set
s1 is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
s2 is Relation-like the carrier of SCM+FSA -defined Function-like K304(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
i is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
Comput (P2,s2,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
da is V63() Element of the carrier of SCM+FSA
f is V63() Element of the carrier of SCM+FSA
AddTo (da,f) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(Comput (P1,s1,i)) . da is V24() V25() integer ext-real set
(Comput (P1,s1,i)) . f is V24() V25() integer ext-real set
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . f) is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . da is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . f is V24() V25() integer ext-real set
((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . f) is V24() V25() integer ext-real set
i + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
((Comput (P1,s1,(i + 1))) | (dom p)) . da is set
(Comput (P1,s1,(i + 1))) . da is V24() V25() integer ext-real set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
((Comput (P2,s2,(i + 1))) | (dom p)) . da is set
(Comput (P2,s2,(i + 1))) . da is V24() V25() integer ext-real set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is 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 carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite q -autonomic set
dom p is non empty finite set
s1 is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
s2 is Relation-like the carrier of SCM+FSA -defined Function-like K304(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
i is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
Comput (P2,s2,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
da is V63() Element of the carrier of SCM+FSA
f is V63() Element of the carrier of SCM+FSA
SubFrom (da,f) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(Comput (P1,s1,i)) . da is V24() V25() integer ext-real set
(Comput (P1,s1,i)) . f is V24() V25() integer ext-real set
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . f) is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . da is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . f is V24() V25() integer ext-real set
((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . f) is V24() V25() integer ext-real set
i + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
((Comput (P1,s1,(i + 1))) | (dom p)) . da is set
(Comput (P1,s1,(i + 1))) . da is V24() V25() integer ext-real set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
((Comput (P2,s2,(i + 1))) | (dom p)) . da is set
(Comput (P2,s2,(i + 1))) . da is V24() V25() integer ext-real set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is 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 carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite q -autonomic set
dom p is non empty finite set
s1 is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
s2 is Relation-like the carrier of SCM+FSA -defined Function-like K304(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
i is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
Comput (P2,s2,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
da is V63() Element of the carrier of SCM+FSA
f is V63() Element of the carrier of SCM+FSA
MultBy (da,f) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(Comput (P1,s1,i)) . da is V24() V25() integer ext-real set
(Comput (P1,s1,i)) . f is V24() V25() integer ext-real set
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . f) is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . da is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . f is V24() V25() integer ext-real set
((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . f) is V24() V25() integer ext-real set
i + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
((Comput (P1,s1,(i + 1))) | (dom p)) . da is set
(Comput (P1,s1,(i + 1))) . da is V24() V25() integer ext-real set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
((Comput (P2,s2,(i + 1))) | (dom p)) . da is set
(Comput (P2,s2,(i + 1))) . da is V24() V25() integer ext-real set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is 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 carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite q -autonomic set
dom p is non empty finite set
s1 is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
s2 is Relation-like the carrier of SCM+FSA -defined Function-like K304(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
i is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
Comput (P2,s2,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
da is V63() Element of the carrier of SCM+FSA
f is V63() Element of the carrier of SCM+FSA
Divide (da,f) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(Comput (P1,s1,i)) . da is V24() V25() integer ext-real set
(Comput (P1,s1,i)) . f is V24() V25() integer ext-real set
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . f) is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . da is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . f is V24() V25() integer ext-real set
((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . f) is V24() V25() integer ext-real set
i + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
((Comput (P1,s1,(i + 1))) | (dom p)) . da is set
(Comput (P1,s1,(i + 1))) . da is V24() V25() integer ext-real set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
((Comput (P2,s2,(i + 1))) | (dom p)) . da is set
(Comput (P2,s2,(i + 1))) . da is V24() V25() integer ext-real set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is 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 carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite q -autonomic set
dom p is non empty finite set
s1 is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
s2 is Relation-like the carrier of SCM+FSA -defined Function-like K304(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
i is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
Comput (P2,s2,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
da is V63() Element of the carrier of SCM+FSA
f is V63() Element of the carrier of SCM+FSA
Divide (da,f) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
(Comput (P1,s1,i)) . da is V24() V25() integer ext-real set
(Comput (P1,s1,i)) . f is V24() V25() integer ext-real set
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . f) is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . da is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . f is V24() V25() integer ext-real set
((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . f) is V24() V25() integer ext-real set
i + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
((Comput (P1,s1,(i + 1))) | (dom p)) . f is set
(Comput (P1,s1,(i + 1))) . f is V24() V25() integer ext-real set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
((Comput (P2,s2,(i + 1))) | (dom p)) . f is set
(Comput (P2,s2,(i + 1))) . f is V24() V25() integer ext-real set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is 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 carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite q -autonomic set
s1 is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
s2 is Relation-like the carrier of SCM+FSA -defined Function-like K304(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
i is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
succ (IC (Comput (P1,s1,i))) is non empty V17() V18() V19() V23() V24() V25() integer finite V33() V64() ext-real set
Comput (P2,s2,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
da is V63() Element of the carrier of SCM+FSA
(Comput (P1,s1,i)) . da is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . da is V24() V25() integer ext-real set
f is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
da =0_goto f is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
i + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
dom p is non empty finite set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
((Comput (P1,s1,(i + 1))) | (dom p)) . (IC ) is set
(Comput (P1,s1,(i + 1))) . (IC ) is set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
((Comput (P2,s2,(i + 1))) | (dom p)) . (IC ) is set
(Comput (P2,s2,(i + 1))) . (IC ) is set
succ (IC (Comput (P2,s2,i))) is non empty V17() V18() V19() V23() V24() V25() integer finite V33() V64() ext-real 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 carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite q -autonomic set
s1 is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
s2 is Relation-like the carrier of SCM+FSA -defined Function-like K304(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
i is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
succ (IC (Comput (P1,s1,i))) is non empty V17() V18() V19() V23() V24() V25() integer finite V33() V64() ext-real set
Comput (P2,s2,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
da is V63() Element of the carrier of SCM+FSA
(Comput (P1,s1,i)) . da is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . da is V24() V25() integer ext-real set
f is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
da >0_goto f is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
i + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
dom p is non empty finite set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is set
((Comput (P1,s1,(i + 1))) | (dom p)) . (IC ) is set
(Comput (P1,s1,(i + 1))) . (IC ) is set
((Comput (P2,s2,(i + 1))) | (dom p)) . (IC ) is set
(Comput (P2,s2,(i + 1))) . (IC ) is set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is 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 carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite q -autonomic set
dom p is non empty finite set
s1 is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
s2 is Relation-like the carrier of SCM+FSA -defined Function-like K304(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
i is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
Comput (P2,s2,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
da is V63() Element of the carrier of SCM+FSA
f is V63() Element of the carrier of SCM+FSA
(Comput (P1,s1,i)) . f is V24() V25() integer ext-real set
abs ((Comput (P1,s1,i)) . f) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . f is V24() V25() integer ext-real set
abs ((Comput (P2,s2,i)) . f) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Cs1i1 is FinSeq-Location
da := (Cs1i1,f) is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
<*da,Cs1i1,f*> is non empty Relation-like NAT -defined Function-like finite V35(3) FinSequence-like FinSubsequence-like set
K15(9,{},<*da,Cs1i1,f*>) is set
(Comput (P1,s1,i)) . Cs1i1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Comput (P2,s2,i)) . Cs1i1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
i + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is set
((Comput (P1,s1,(i + 1))) | (dom p)) . da is set
(Comput (P1,s1,(i + 1))) . da is V24() V25() integer ext-real set
((Comput (P2,s2,(i + 1))) | (dom p)) . da is set
(Comput (P2,s2,(i + 1))) . da is V24() V25() integer ext-real set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . da is V24() V25() integer ext-real set
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P2,s2,i)) is set
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i)))) . da is V24() V25() integer ext-real set
i2 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
i2 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
((Comput (P1,s1,i)) . Cs1i1) /. i2 is V24() V25() integer ext-real Element of INT
((Comput (P2,s2,i)) . Cs1i1) /. i2 is V24() V25() integer ext-real Element of INT
Cs2k is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
((Comput (P1,s1,i)) . Cs1i1) /. Cs2k is V24() V25() integer ext-real Element of INT
k is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
((Comput (P2,s2,i)) . Cs1i1) /. k is V24() V25() integer ext-real Element of INT
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 carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite q -autonomic set
dom p is non empty finite set
s1 is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
s2 is Relation-like the carrier of SCM+FSA -defined Function-like K304(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
i is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
Comput (P2,s2,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
da is V63() Element of the carrier of SCM+FSA
f is V63() Element of the carrier of SCM+FSA
(Comput (P1,s1,i)) . f is V24() V25() integer ext-real set
abs ((Comput (P1,s1,i)) . f) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . f is V24() V25() integer ext-real set
abs ((Comput (P2,s2,i)) . f) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P1,s1,i)) . da is V24() V25() integer ext-real set
(Comput (P2,s2,i)) . da is V24() V25() integer ext-real set
Cs1i1 is FinSeq-Location
(Cs1i1,f) := da is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
10 is non empty V17() V18() V19() V23() V24() V25() integer finite V33() V64() ext-real positive Element of NAT
<*da,Cs1i1,f*> is non empty Relation-like NAT -defined Function-like finite V35(3) FinSequence-like FinSubsequence-like set
K15(10,{},<*da,Cs1i1,f*>) is set
(Comput (P1,s1,i)) . Cs1i1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
(Comput (P2,s2,i)) . Cs1i1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
i + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is set
((Comput (P1,s1,(i + 1))) | (dom p)) . Cs1i1 is set
(Comput (P1,s1,(i + 1))) . Cs1i1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
((Comput (P2,s2,(i + 1))) | (dom p)) . Cs1i1 is set
(Comput (P2,s2,(i + 1))) . Cs1i1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . Cs1i1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P2,s2,i)) is set
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i)))) . Cs1i1 is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
i2 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
i2 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
((Comput (P1,s1,i)) . Cs1i1) +* (i2,((Comput (P1,s1,i)) . da)) is Relation-like Function-like set
((Comput (P2,s2,i)) . Cs1i1) +* (i2,((Comput (P2,s2,i)) . da)) is Relation-like Function-like set
Cs2k is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
((Comput (P1,s1,i)) . Cs1i1) +* (Cs2k,((Comput (P1,s1,i)) . da)) is Relation-like Function-like set
k is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
((Comput (P2,s2,i)) . Cs1i1) +* (k,((Comput (P2,s2,i)) . da)) is Relation-like Function-like 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 carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite q -autonomic set
dom p is non empty finite set
s1 is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
s2 is Relation-like the carrier of SCM+FSA -defined Function-like K304(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
i is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
Comput (P2,s2,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
da is V63() Element of the carrier of SCM+FSA
f is FinSeq-Location
da :=len f is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
11 is non empty V17() V18() V19() V23() V24() V25() integer finite V33() V64() ext-real positive Element of NAT
<*da,f*> is non empty Relation-like NAT -defined Function-like finite V35(2) FinSequence-like FinSubsequence-like set
K15(11,{},<*da,f*>) is set
(Comput (P1,s1,i)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len ((Comput (P1,s1,i)) . f) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
len ((Comput (P2,s2,i)) . f) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
i + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is set
((Comput (P1,s1,(i + 1))) | (dom p)) . da is set
(Comput (P1,s1,(i + 1))) . da is V24() V25() integer ext-real set
((Comput (P2,s2,(i + 1))) | (dom p)) . da is set
(Comput (P2,s2,(i + 1))) . da is V24() V25() integer ext-real set
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . da is V24() V25() integer ext-real set
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P2,s2,i)) is set
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i)))) . da is V24() V25() integer ext-real 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 carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite q -autonomic set
dom p is non empty finite set
s1 is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
s2 is Relation-like the carrier of SCM+FSA -defined Function-like K304(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
i is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P1,(Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P1,s1,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P1,s1,i)) . (IC ) is set
P1 /. (IC (Comput (P1,s1,i))) is Element of the InstructionsF of SCM+FSA
Comput (P2,s2,i) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
da is V63() Element of the carrier of SCM+FSA
(Comput (P1,s1,i)) . da is V24() V25() integer ext-real set
abs ((Comput (P1,s1,i)) . da) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . da is V24() V25() integer ext-real set
abs ((Comput (P2,s2,i)) . da) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
f is FinSeq-Location
f :=<0,...,0> da is V77( the InstructionsF of SCM+FSA) V90(3, SCM+FSA ) Element of the InstructionsF of SCM+FSA
12 is non empty V17() V18() V19() V23() V24() V25() integer finite V33() V64() ext-real positive Element of NAT
<*da,f*> is non empty Relation-like NAT -defined Function-like finite V35(2) FinSequence-like FinSubsequence-like set
K15(12,{},<*da,f*>) is set
i + 1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Comput (P1,s1,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Comput (P2,s2,(i + 1)) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
(Comput (P1,s1,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
(Comput (P2,s2,(i + 1))) | (dom p) is Relation-like dom p -defined the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible finite set
Following (P1,(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)) is set
K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))) is set
the Execution of SCM+FSA is Relation-like Function-like V40( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) Element of K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))))
K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))) is Relation-like set
K32(K33( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))))) is set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P1,s1,i)) is set
((Comput (P1,s1,(i + 1))) | (dom p)) . f is set
(Comput (P1,s1,(i + 1))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
((Comput (P2,s2,(i + 1))) | (dom p)) . f is set
(Comput (P2,s2,(i + 1))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Following (P2,(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
CurInstr (P2,(Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
IC (Comput (P2,s2,i)) is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
(Comput (P2,s2,i)) . (IC ) is set
P2 /. (IC (Comput (P2,s2,i))) is Element of the InstructionsF of SCM+FSA
Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) is Element of K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)))
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P2,(Comput (P2,s2,i))))) . (Comput (P2,s2,i)) is set
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i))) is Relation-like the carrier of SCM+FSA -defined Function-like K304(3,SCM+FSA) -compatible total set
K172( the InstructionsF of SCM+FSA,K170(K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA)),K198(( the Object-Kind of SCM+FSA * the U7 of SCM+FSA))), the Execution of SCM+FSA,(CurInstr (P1,(Comput (P1,s1,i))))) . (Comput (P2,s2,i)) is set
(Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P2,s2,i)))) . f is Relation-like NAT -defined INT -valued Function-like finite FinSequence-like FinSubsequence-like FinSequence of INT
i1 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
i2 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
i1 |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of i1 -tuples_on NAT
i1 -tuples_on NAT is FinSequenceSet of NAT
i2 |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of i2 -tuples_on NAT
i2 -tuples_on NAT is FinSequenceSet of NAT
i2 is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
i2 |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of i2 -tuples_on NAT
i2 -tuples_on NAT is FinSequenceSet of NAT
Cs2k is V17() V18() V19() V23() V24() V25() integer finite V33() ext-real Element of NAT
Cs2k |-> 0 is Relation-like NAT -defined NAT -valued Function-like finite FinSequence-like FinSubsequence-like Element of Cs2k -tuples_on NAT
Cs2k -tuples_on NAT is FinSequenceSet of NAT