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