:: The {\bf loop} and {\bf Times} Macroinstruction for {\SCMFSA}
:: by Noriko Asamoto
::
:: Received October 29, 1997
:: Copyright (c) 1997 Association of Mizar Users

begin

set SA0 = Start-At (0,SCM+FSA);

set Q = (intloc 0) .--> 1;

theorem :: SCMFSA8C:1

canceled;

theorem Th2: :: SCMFSA8C:2

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being initial FinPartState of SCM+FSA st I is_pseudo-closed_on s,P holds
for k being Element of NAT st ( for n being Element of NAT st n <= k holds
IC (Comput ((P +* (ProgramPart I)),(s +* (Initialize I)),n)) in dom I ) holds
k < pseudo-LifeSpan (s,P,I)

proof end;

theorem :: SCMFSA8C:3

canceled;

theorem :: SCMFSA8C:4

canceled;

theorem :: SCMFSA8C:5

canceled;

theorem :: SCMFSA8C:6

canceled;

theorem :: SCMFSA8C:7

canceled;

theorem :: SCMFSA8C:8

canceled;

theorem :: SCMFSA8C:9

canceled;

theorem :: SCMFSA8C:10

canceled;

theorem :: SCMFSA8C:11

canceled;

theorem :: SCMFSA8C:12

canceled;

theorem Th13: :: SCMFSA8C:13

for I, J being Program of SCM+FSA
for k being Element of NAT st card I <= k & k < (card I) + (card J) holds
for i being Instruction of SCM+FSA st i = J . (k -' (card I)) holds
(I ';' J) . k = IncAddr (i,(card I))

proof end;

theorem Th14: :: SCMFSA8C:14

for s being State of SCM+FSA st s . (intloc 0) = 1 & IC s = 0 holds
Initialized s = s

proof end;

theorem Th15: :: SCMFSA8C:15

for s being State of SCM+FSA holds Initialized (Initialized s) = Initialized s

proof end;

theorem Th16: :: SCMFSA8C:16

for s being State of SCM+FSA
for I being Program of SCM+FSA holds s +* (Initialize (Initialized I)) = (Initialized s) +* (Initialize I)

proof end;

theorem Th17: :: SCMFSA8C:17

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA holds IExec (I,P,s) = IExec (I,P,(Initialized s))

proof end;

theorem Th18: :: SCMFSA8C:18

for s being State of SCM+FSA
for I being Program of SCM+FSA st s . (intloc 0) = 1 holds
s +* (Initialize I) = s +* (Initialized I)

proof end;

theorem Th19: :: SCMFSA8C:19

for I being Program of SCM+FSA holds Initialize I c= Initialized I

proof end;

theorem Th20: :: SCMFSA8C:20

for l being Element of NAT
for I being Program of SCM+FSA holds
( l in dom I iff l in dom (Initialized I) )

proof end;

theorem :: SCMFSA8C:21

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA holds
( Initialized I is_closed_on s,P iff I is_closed_on Initialized s,P )

proof end;

theorem Th22: :: SCMFSA8C:22

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA holds
( Initialized I is_halting_on s,P iff I is_halting_on Initialized s,P )

proof end;

theorem :: SCMFSA8C:23

for I being Program of SCM+FSA st ( for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds I is_halting_on Initialized s,P ) holds
Initialized I is halting

proof end;

theorem Th24: :: SCMFSA8C:24

for I being Program of SCM+FSA st ( for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds Initialized I is_halting_on s,P ) holds
Initialized I is halting

proof end;

theorem :: SCMFSA8C:25

canceled;

theorem :: SCMFSA8C:26

for s being State of SCM+FSA
for I being Program of SCM+FSA
for l being Element of NAT
for x being set st x in dom I holds
I . x = (s +* (I +* (Start-At (l,SCM+FSA)))) . x

proof end;

theorem Th27: :: SCMFSA8C:27

for s being State of SCM+FSA st s . (intloc 0) = 1 holds
DataPart (Initialized s) = DataPart s

proof end;

theorem Th28: :: SCMFSA8C:28

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location
for l being Element of NAT holds (s +* (I +* (Start-At (l,SCM+FSA)))) . a = s . a

proof end;

theorem :: SCMFSA8C:29

for I being preProgram of SCM+FSA
for l being Element of NAT holds IC in dom (I +* (Start-At (l,SCM+FSA)))

proof end;

theorem :: SCMFSA8C:30

for I being preProgram of SCM+FSA
for l being Element of NAT holds (I +* (Start-At (l,SCM+FSA))) . (IC ) = l

proof end;

theorem Th31: :: SCMFSA8C:31

for s being State of SCM+FSA
for I being FinPartState of SCM+FSA
for l being Element of NAT holds IC (s +* (I +* (Start-At (l,SCM+FSA)))) = l

proof end;

theorem Th32: :: SCMFSA8C:32

for s being State of SCM+FSA
for i being Instruction of SCM+FSA st InsCode i in {0,6,7,8} holds
DataPart (Exec (i,s)) = DataPart s

proof end;

theorem Th33: :: SCMFSA8C:33

for s1, s2 being State of SCM+FSA st s1 . (intloc 0) = s2 . (intloc 0) & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
DataPart s1 = DataPart s2

proof end;

theorem :: SCMFSA8C:34

canceled;

theorem :: SCMFSA8C:35

canceled;

theorem Th36: :: SCMFSA8C:36

for s being State of SCM+FSA holds (Initialized s) | NAT = s | NAT

proof end;

theorem :: SCMFSA8C:37

canceled;

theorem Th38: :: SCMFSA8C:38

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA holds IExec ((Stop SCM+FSA),P,s) = Initialize (Initialized s)

proof end;

theorem Th39: :: SCMFSA8C:39

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P holds
0 in dom I

proof end;

theorem :: SCMFSA8C:40

canceled;

theorem :: SCMFSA8C:41

canceled;

theorem Th42: :: SCMFSA8C:42

for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1,P1 & Initialize I c= s1 & I c= P1 holds
for n being Element of NAT st Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

proof end;

theorem Th43: :: SCMFSA8C:43

for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1,P1 & Initialize I c= s1 & Initialize I c= s2 & I c= P1 & I c= P2 & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )

proof end;

theorem Th44: :: SCMFSA8C:44

for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & Initialize I c= s1 & Initialize I c= s2 & I c= P1 & I c= P2 & DataPart s1 = DataPart s2 holds
LifeSpan (P1,s1) = LifeSpan (P2,s2)

proof end;

theorem Th45: :: SCMFSA8C:45

for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st s1 . (intloc 0) = 1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 & ( for a being read-write Int-Location holds s1 . a = s2 . a ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) holds
DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))

proof end;

theorem Th46: :: SCMFSA8C:46

for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st s1 . (intloc 0) = 1 & I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
DataPart (IExec (I,P1,s1)) = DataPart (IExec (I,P2,s2))

proof end;

registration

let I be Program of SCM+FSA;
cluster Initialized I -> initial ;
correctness
coherence
Initialized I is initial ;

proof end;

end;

Lm1: now

let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA holds
( ( Initialized I is_pseudo-closed_on s,P implies ( I is_pseudo-closed_on Initialized s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) ) ) & ( I is_pseudo-closed_on Initialized s,P implies ( Initialized I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) ) ) )
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA holds
( ( Initialized I is_pseudo-closed_on s,P implies ( I is_pseudo-closed_on Initialized s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) ) ) & ( I is_pseudo-closed_on Initialized s,P implies ( Initialized I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) ) ) )
let I be Program of SCM+FSA; :: thesis: ( ( Initialized I is_pseudo-closed_on s,P implies ( I is_pseudo-closed_on Initialized s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) ) ) & ( I is_pseudo-closed_on Initialized s,P implies ( Initialized I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) ) ) )
set k = pseudo-LifeSpan ((Initialized s),P,I);
A1: ProgramPart (Initialized I) = I by SCMFSA6A:33;
A2: ProgramPart I = I by RELAT_1:209;

hereby :: thesis: ( I is_pseudo-closed_on Initialized s,P implies ( Initialized I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) ) )

set k = pseudo-LifeSpan (s,P,(Initialized I));
A3: s +* (Initialize (Initialized I)) = (Initialized s) +* (Initialize I) by Th16;
assume A4: Initialized I is_pseudo-closed_on s,P ; :: thesis: ( I is_pseudo-closed_on Initialized s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) )
then IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),(pseudo-LifeSpan (s,P,(Initialized I))))) = card I by SCMFSA8A:def 5, A1;
then IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),(pseudo-LifeSpan (s,P,(Initialized I))))) = card I by A3;
then A5: IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),(pseudo-LifeSpan (s,P,(Initialized I))))) = card (ProgramPart I) by RELAT_1:209;

A6: now

let n be Element of NAT ; :: thesis: ( n < pseudo-LifeSpan (s,P,(Initialized I)) implies IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),n)) in dom I )
A7: s +* (Initialize (Initialized I)) = (Initialized s) +* (Initialize I) by Th16;
assume n < pseudo-LifeSpan (s,P,(Initialized I)) ; :: thesis: IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),n)) in dom I
then IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),n)) in dom (Initialized I) by A4, SCMFSA8A:def 5, A1;
then IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),n)) in dom (Initialized I) by A7;
hence IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),n)) in dom I by Th20; :: thesis: verum

end;

hence A8: I is_pseudo-closed_on Initialized s,P by A5, SCMFSA8A:def 3, A2; :: thesis: pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I)
for n being Element of NAT st not IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),n)) in dom I holds
pseudo-LifeSpan (s,P,(Initialized I)) <= n by A6;
hence pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) by A5, A8, SCMFSA8A:def 5, A2; :: thesis: verum

end;

A9: s +* (Initialize (Initialized I)) = (Initialized s) +* (Initialize I) by Th16;
assume A10: I is_pseudo-closed_on Initialized s,P ; :: thesis: ( Initialized I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) )
then IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),(pseudo-LifeSpan ((Initialized s),P,I)))) = card (ProgramPart I) by SCMFSA8A:def 5, A2;
then IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),(pseudo-LifeSpan ((Initialized s),P,I)))) = card (ProgramPart I) by A9;
then A11: IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),(pseudo-LifeSpan ((Initialized s),P,I)))) = card I by RELAT_1:209;

A12: now

let n be Element of NAT ; :: thesis: ( n < pseudo-LifeSpan ((Initialized s),P,I) implies IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),n)) in dom (Initialized I) )
A13: s +* (Initialize (Initialized I)) = (Initialized s) +* (Initialize I) by Th16;
assume n < pseudo-LifeSpan ((Initialized s),P,I) ; :: thesis: IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),n)) in dom (Initialized I)
then IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),n)) in dom I by A10, SCMFSA8A:def 5, A2;
then IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),n)) in dom I by A13;
hence IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),n)) in dom (Initialized I) by Th20; :: thesis: verum

end;

hence A14: Initialized I is_pseudo-closed_on s,P by A11, SCMFSA8A:def 3, A1; :: thesis: pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I)
for n being Element of NAT st not IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),n)) in dom (Initialized I) holds
pseudo-LifeSpan ((Initialized s),P,I) <= n by A12;
hence pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) by A11, A14, SCMFSA8A:def 5, A1; :: thesis: verum

end;

theorem :: SCMFSA8C:47

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA holds
( Initialized I is_pseudo-closed_on s,P iff I is_pseudo-closed_on Initialized s,P ) by Lm1;

theorem :: SCMFSA8C:48

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_pseudo-closed_on Initialized s,P holds
pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) by Lm1;

theorem :: SCMFSA8C:49

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA st Initialized I is_pseudo-closed_on s,P holds
pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) by Lm1;

theorem Th50: :: SCMFSA8C:50

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
( I is_pseudo-closed_on s +* (Initialize I),P +* I & pseudo-LifeSpan (s,P,I) = pseudo-LifeSpan ((s +* (Initialize I)),(P +* I),I) )

proof end;

theorem Th51: :: SCMFSA8C:51

for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st Initialize I c= s1 & I c= P1 & I is_pseudo-closed_on s1,P1 holds
for n being Element of NAT st Reloc (I,n) c= s2 & Reloc (I,n) c= P2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( ( for i being Element of NAT st i < pseudo-LifeSpan (s1,P1,I) holds
IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),n) = CurInstr (P2,(Comput (P2,s2,i))) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan (s1,P1,I) holds
( (IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) & DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) )

proof end;

theorem Th52: :: SCMFSA8C:52

for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_pseudo-closed_on s1,P1 holds
I is_pseudo-closed_on s2,P2

proof end;

theorem Th53: :: SCMFSA8C:53

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA st s . (intloc 0) = 1 holds
( I is_pseudo-closed_on s,P iff I is_pseudo-closed_on Initialized s,P )

proof end;

theorem Th54: :: SCMFSA8C:54

for a being Int-Location
for I, J being Program of SCM+FSA holds
( 0 in dom (if=0 (a,I,J)) & 1 in dom (if=0 (a,I,J)) & 0 in dom (if>0 (a,I,J)) & 1 in dom (if>0 (a,I,J)) )

proof end;

theorem Th55: :: SCMFSA8C:55

for a being Int-Location
for I, J being Program of SCM+FSA holds
( (if=0 (a,I,J)) . 0 = a =0_goto ((card J) + 3) & (if=0 (a,I,J)) . 1 = goto 2 & (if>0 (a,I,J)) . 0 = a >0_goto ((card J) + 3) & (if>0 (a,I,J)) . 1 = goto 2 )

proof end;

theorem Th56: :: SCMFSA8C:56

for a being Int-Location
for I, J being Program of SCM+FSA
for n being Element of NAT st n < ((card I) + (card J)) + 3 holds
( n in dom (if=0 (a,I,J)) & (if=0 (a,I,J)) . n <> halt SCM+FSA )

proof end;

theorem Th57: :: SCMFSA8C:57

for a being Int-Location
for I, J being Program of SCM+FSA
for n being Element of NAT st n < ((card I) + (card J)) + 3 holds
( n in dom (if>0 (a,I,J)) & (if>0 (a,I,J)) . n <> halt SCM+FSA )

proof end;

theorem Th58: :: SCMFSA8C:58

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s,P holds
( I ';' (Stop SCM+FSA) is_closed_on s,P & I ';' (Stop SCM+FSA) is_halting_on s,P & LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = pseudo-LifeSpan (s,P,(Directed I)) & ( for n being Element of NAT st n < pseudo-LifeSpan (s,P,(Directed I)) holds
IC (Comput ((P +* I),(s +* (Initialize I)),n)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan (s,P,(Directed I)) holds
DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) )

proof end;

theorem Th59: :: SCMFSA8C:59

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s,P holds
DataPart (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))) = DataPart (Comput ((P +* I),(s +* (Initialize I)),(pseudo-LifeSpan (s,P,(Directed I)))))

proof end;

theorem :: SCMFSA8C:60

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA st s . (intloc 0) = 1 & Directed I is_pseudo-closed_on s,P holds
DataPart (IExec ((I ';' (Stop SCM+FSA)),P,s)) = DataPart (Comput ((P +* I),(s +* (Initialize I)),(pseudo-LifeSpan (s,P,(Directed I)))))

proof end;

theorem Th61: :: SCMFSA8C:61

for I, J being Program of SCM+FSA
for a being Int-Location holds (if=0 (a,I,J)) . (((card I) + (card J)) + 3) = halt SCM+FSA

proof end;

theorem Th62: :: SCMFSA8C:62

for I, J being Program of SCM+FSA
for a being Int-Location holds (if>0 (a,I,J)) . (((card I) + (card J)) + 3) = halt SCM+FSA

proof end;

theorem Th63: :: SCMFSA8C:63

for I, J being Program of SCM+FSA
for a being Int-Location holds (if=0 (a,I,J)) . ((card J) + 2) = goto (((card I) + (card J)) + 3)

proof end;

theorem Th64: :: SCMFSA8C:64

for I, J being Program of SCM+FSA
for a being Int-Location holds (if>0 (a,I,J)) . ((card J) + 2) = goto (((card I) + (card J)) + 3)

proof end;

theorem Th65: :: SCMFSA8C:65

for J being Program of SCM+FSA
for a being Int-Location holds (if=0 (a,(Goto 2),J)) . ((card J) + 3) = goto ((card J) + 5)

proof end;

theorem Th66: :: SCMFSA8C:66

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a = 0 & Directed I is_pseudo-closed_on s,P holds
( if=0 (a,I,J) is_halting_on s,P & if=0 (a,I,J) is_closed_on s,P & LifeSpan ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J))))) = (LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))) + 1 )

proof end;

theorem :: SCMFSA8C:67

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . (intloc 0) = 1 & s . a = 0 & Directed I is_pseudo-closed_on s,P holds
DataPart (IExec ((if=0 (a,I,J)),P,s)) = DataPart (IExec ((I ';' (Stop SCM+FSA)),P,s))

proof end;

theorem Th68: :: SCMFSA8C:68

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a > 0 & Directed I is_pseudo-closed_on s,P holds
( if>0 (a,I,J) is_halting_on s,P & if>0 (a,I,J) is_closed_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J))))) = (LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))) + 1 )

proof end;

theorem Th69: :: SCMFSA8C:69

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . (intloc 0) = 1 & s . a > 0 & Directed I is_pseudo-closed_on s,P holds
DataPart (IExec ((if>0 (a,I,J)),P,s)) = DataPart (IExec ((I ';' (Stop SCM+FSA)),P,s))

proof end;

theorem Th70: :: SCMFSA8C:70

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a <> 0 & Directed J is_pseudo-closed_on s,P holds
( if=0 (a,I,J) is_halting_on s,P & if=0 (a,I,J) is_closed_on s,P & LifeSpan ((P +* (if=0 (a,I,J))),(s +* (Initialize (if=0 (a,I,J))))) = (LifeSpan ((P +* (J ';' (Stop SCM+FSA))),(s +* (Initialize (J ';' (Stop SCM+FSA)))))) + 3 )

proof end;

theorem :: SCMFSA8C:71

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . (intloc 0) = 1 & s . a <> 0 & Directed J is_pseudo-closed_on s,P holds
DataPart (IExec ((if=0 (a,I,J)),P,s)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,s))

proof end;

theorem Th72: :: SCMFSA8C:72

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . a <= 0 & Directed J is_pseudo-closed_on s,P holds
( if>0 (a,I,J) is_halting_on s,P & if>0 (a,I,J) is_closed_on s,P & LifeSpan ((P +* (if>0 (a,I,J))),(s +* (Initialize (if>0 (a,I,J))))) = (LifeSpan ((P +* (J ';' (Stop SCM+FSA))),(s +* (Initialize (J ';' (Stop SCM+FSA)))))) + 3 )

proof end;

theorem Th73: :: SCMFSA8C:73

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st s . (intloc 0) = 1 & s . a <= 0 & Directed J is_pseudo-closed_on s,P holds
DataPart (IExec ((if>0 (a,I,J)),P,s)) = DataPart (IExec ((J ';' (Stop SCM+FSA)),P,s))

proof end;

theorem :: SCMFSA8C:74

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st Directed I is_pseudo-closed_on s,P & Directed J is_pseudo-closed_on s,P holds
( if=0 (a,I,J) is_closed_on s,P & if=0 (a,I,J) is_halting_on s,P )

proof end;

theorem :: SCMFSA8C:75

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for a being read-write Int-Location st Directed I is_pseudo-closed_on s,P & Directed J is_pseudo-closed_on s,P holds
( if>0 (a,I,J) is_closed_on s,P & if>0 (a,I,J) is_halting_on s,P )

proof end;

theorem :: SCMFSA8C:76

for I being Program of SCM+FSA
for a being Int-Location st not I destroys a holds
not Directed I destroys a by SCMFSA8A:27;

theorem Th77: :: SCMFSA8C:77

for i being Instruction of SCM+FSA
for a being Int-Location st not i destroys a holds
not Macro i destroys a

proof end;

theorem Th78: :: SCMFSA8C:78

for a being Int-Location holds not halt SCM+FSA refers a

proof end;

theorem :: SCMFSA8C:79

for a, b, c being Int-Location st a <> b holds
not AddTo (c,b) refers a

proof end;

theorem :: SCMFSA8C:80

for i being Instruction of SCM+FSA
for a being Int-Location st not i refers a holds
not Macro i refers a

proof end;

theorem Th81: :: SCMFSA8C:81

for I, J being Program of SCM+FSA
for a being Int-Location st not I destroys a & not J destroys a holds
not I ';' J destroys a

proof end;

theorem Th82: :: SCMFSA8C:82

for J being Program of SCM+FSA
for i being Instruction of SCM+FSA
for a being Int-Location st not i destroys a & not J destroys a holds
not i ';' J destroys a

proof end;

theorem :: SCMFSA8C:83

for I being Program of SCM+FSA
for j being Instruction of SCM+FSA
for a being Int-Location st not I destroys a & not j destroys a holds
not I ';' j destroys a

proof end;

theorem :: SCMFSA8C:84

for i, j being Instruction of SCM+FSA
for a being Int-Location st not i destroys a & not j destroys a holds
not i ';' j destroys a

proof end;

theorem Th85: :: SCMFSA8C:85

for a being Int-Location holds not Stop SCM+FSA destroys a

proof end;

theorem Th86: :: SCMFSA8C:86

for a being Int-Location
for l being Element of NAT holds not Goto l destroys a

proof end;

theorem Th87: :: SCMFSA8C:87

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_halting_on Initialized s,P holds
( ( for a being read-write Int-Location holds (IExec (I,P,s)) . a = (Comput ((P +* I),((Initialized s) +* (Initialize I)),(LifeSpan ((P +* I),((Initialized s) +* (Initialize I)))))) . a ) & ( for f being FinSeq-Location holds (IExec (I,P,s)) . f = (Comput ((P +* I),((Initialized s) +* (Initialize I)),(LifeSpan ((P +* I),((Initialized s) +* (Initialize I)))))) . f ) )

proof end;

theorem Th88: :: SCMFSA8C:88

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being parahalting Program of SCM+FSA
for a being read-write Int-Location holds (IExec (I,P,s)) . a = (Comput ((P +* I),((Initialized s) +* (Initialize I)),(LifeSpan ((P +* I),((Initialized s) +* (Initialize I)))))) . a

proof end;

theorem Th89: :: SCMFSA8C:89

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location
for k being Element of NAT st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P & not I destroys a holds
(IExec (I,P,s)) . a = (Comput ((P +* I),((Initialized s) +* (Initialize I)),k)) . a

proof end;

theorem Th90: :: SCMFSA8C:90

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being parahalting Program of SCM+FSA
for a being Int-Location
for k being Element of NAT st not I destroys a holds
(IExec (I,P,s)) . a = (Comput ((P +* I),((Initialized s) +* (Initialize I)),k)) . a

proof end;

theorem Th91: :: SCMFSA8C:91

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being parahalting Program of SCM+FSA
for a being Int-Location st not I destroys a holds
(IExec (I,P,s)) . a = (Initialized s) . a

proof end;

theorem Th92: :: SCMFSA8C:92

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being keeping_0 Program of SCM+FSA st I is_halting_on Initialized s,P holds
( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Element of NAT holds (Comput ((P +* I),((Initialized s) +* (Initialize I)),k)) . (intloc 0) = 1 ) )

proof end;

theorem Th93: :: SCMFSA8C:93

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location st not I destroys a holds
for k being Element of NAT st IC (Comput ((P +* I),(s +* (Initialize I)),k)) in dom I holds
(Comput ((P +* I),(s +* (Initialize I)),(k + 1))) . a = (Comput ((P +* I),(s +* (Initialize I)),k)) . a

proof end;

theorem Th94: :: SCMFSA8C:94

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location st not I destroys a holds
for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Comput ((P +* I),(s +* (Initialize I)),n)) in dom I ) holds
for n being Element of NAT st n <= m holds
(Comput ((P +* I),(s +* (Initialize I)),n)) . a = s . a

proof end;

theorem Th95: :: SCMFSA8C:95

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being good Program of SCM+FSA
for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Comput ((P +* I),(s +* (Initialize I)),n)) in dom I ) holds
for n being Element of NAT st n <= m holds
(Comput ((P +* I),(s +* (Initialize I)),n)) . (intloc 0) = s . (intloc 0)

proof end;

theorem Th96: :: SCMFSA8C:96

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being good Program of SCM+FSA st I is_halting_on Initialized s,P & I is_closed_on Initialized s,P holds
( (IExec (I,P,s)) . (intloc 0) = 1 & ( for k being Element of NAT holds (Comput ((P +* I),((Initialized s) +* (Initialize I)),k)) . (intloc 0) = 1 ) )

proof end;

theorem :: SCMFSA8C:97

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being good Program of SCM+FSA st I is_closed_on s,P holds
for k being Element of NAT holds (Comput ((P +* I),(s +* (Initialize I)),k)) . (intloc 0) = s . (intloc 0)

proof end;

theorem Th98: :: SCMFSA8C:98

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being parahalting keeping_0 Program of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
(Comput ((P +* (I ';' (SubFrom (a,(intloc 0))))),((Initialized s) +* (Initialize (I ';' (SubFrom (a,(intloc 0)))))),(LifeSpan ((P +* (I ';' (SubFrom (a,(intloc 0))))),((Initialized s) +* (Initialize (I ';' (SubFrom (a,(intloc 0)))))))))) . a = (s . a) - 1

proof end;

theorem Th99: :: SCMFSA8C:99

for i being Instruction of SCM+FSA st not i destroys intloc 0 holds
Macro i is good

proof end;

theorem Th100: :: SCMFSA8C:100

for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds
( Comput ((P1 +* I),(s1 +* (Initialize I)),k), Comput ((P2 +* I),(s2 +* (Initialize I)),k) equal_outside NAT & CurInstr ((P1 +* I),(Comput ((P1 +* I),(s1 +* (Initialize I)),k))) = CurInstr ((P2 +* I),(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) )

proof end;

theorem Th101: :: SCMFSA8C:101

for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & DataPart s1 = DataPart s2 holds
( LifeSpan ((P1 +* I),(s1 +* (Initialize I))) = LifeSpan ((P2 +* I),(s2 +* (Initialize I))) & Result ((P1 +* I),(s1 +* (Initialize I))), Result ((P2 +* I),(s2 +* (Initialize I))) equal_outside NAT )

proof end;

theorem :: SCMFSA8C:102

canceled;

theorem Th103: :: SCMFSA8C:103

for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1,P1 & I is_halting_on s1,P1 & Initialize I c= s1 & Initialize I c= s2 & I c= P1 & I c= P2 & ex k being Element of NAT st Comput (P1,s1,k),s2 equal_outside NAT holds
Result (P1,s1), Result (P2,s2) equal_outside NAT

proof end;

begin

registration

let I be Program of SCM+FSA;
let k be Element of NAT ;
cluster IncAddr (I,k) -> NAT -defined initial ;
correctness
coherence
( IncAddr (I,k) is initial & IncAddr (I,k) is NAT -defined );

proof end;

end;

definition

let I be Program of SCM+FSA;
canceled;
canceled;
canceled;
func loop I -> halt-free Program of SCM+FSA equals :: SCMFSA8C:def 4
Directed (I,0);
coherence
Directed (I,0) is halt-free Program of SCM+FSA

proof end;

end;

:: deftheorem SCMFSA8C:def 1 :
canceled;

:: deftheorem SCMFSA8C:def 2 :
canceled;

:: deftheorem SCMFSA8C:def 3 :
canceled;

:: deftheorem defines loop SCMFSA8C:def 4 :
for I being Program of SCM+FSA holds loop I = Directed (I,0);

theorem :: SCMFSA8C:104

canceled;

theorem :: SCMFSA8C:105

for I being Program of SCM+FSA
for a being Int-Location st loop I destroys a holds
I destroys a by SCMFSA8A:27;

registration

let I be good Program of SCM+FSA;
cluster loop I -> halt-free good ;
correctness
coherence
loop I is good ;
;

end;

theorem :: SCMFSA8C:106

canceled;

theorem Th107: :: SCMFSA8C:107

for I being Program of SCM+FSA holds not halt SCM+FSA in rng (loop I)

proof end;

theorem :: SCMFSA8C:108

canceled;

theorem Th109: :: SCMFSA8C:109

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
for m being Element of NAT st m <= LifeSpan ((P +* I),(s +* (Initialize I))) holds
Comput ((P +* I),(s +* (Initialize I)),m), Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m) equal_outside NAT

proof end;

theorem Th110: :: SCMFSA8C:110

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
for m being Element of NAT st m < LifeSpan ((P +* I),(s +* (Initialize I))) holds
CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize I)),m))) = CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m)))

proof end;

Lm2: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),(LifeSpan ((P +* I),(s +* (Initialize I))))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((P +* I),(s +* (Initialize I))) holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) <> halt SCM+FSA ) )

proof end;

theorem :: SCMFSA8C:111

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
for m being Element of NAT st m <= LifeSpan ((P +* I),(s +* (Initialize I))) holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) <> halt SCM+FSA by Lm2;

theorem :: SCMFSA8C:112

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),(LifeSpan ((P +* I),(s +* (Initialize I))))))) = goto 0 by Lm2;

theorem Th113: :: SCMFSA8C:113

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being paraclosed Program of SCM+FSA st Initialize I c= s & I c= P & P halts_on s holds
for m being Element of NAT st m <= LifeSpan (P,s) holds
Comput (P,s,m), Comput ((P +* (loop I)),(s +* (loop I)),m) equal_outside NAT

proof end;

theorem :: SCMFSA8C:114

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being parahalting Program of SCM+FSA st Initialized I c= s & I c= P holds
for k being Element of NAT st k <= LifeSpan (P,s) holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (loop I)),k))) <> halt SCM+FSA

proof end;

begin

definition

let a be Int-Location ;
let I be Program of SCM+FSA;
func Times (a,I) -> Program of SCM+FSA equals :: SCMFSA8C:def 5
if>0 (a,(loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Stop SCM+FSA));
correctness
coherence
if>0 (a,(loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Stop SCM+FSA)) is Program of SCM+FSA;
;

end;

:: deftheorem defines Times SCMFSA8C:def 5 :
for a being Int-Location
for I being Program of SCM+FSA holds Times (a,I) = if>0 (a,(loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Stop SCM+FSA));

registration

let a be Int-Location ;
let I be Program of SCM+FSA;
cluster Times (a,I) -> non halt-free ;
coherence
not Times (a,I) is halt-free ;

end;

theorem Th115: :: SCMFSA8C:115

for I being good Program of SCM+FSA
for a being read-write Int-Location holds if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) is good

proof end;

theorem Th116: :: SCMFSA8C:116

for I, J being Program of SCM+FSA
for a being Int-Location holds (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) . ((card (I ';' (SubFrom (a,(intloc 0))))) + 3) = goto ((card (I ';' (SubFrom (a,(intloc 0))))) + 5)

proof end;

theorem Th117: :: SCMFSA8C:117

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being parahalting good Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 & s . a > 0 holds
loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) is_pseudo-closed_on s,P

proof end;

theorem :: SCMFSA8C:118

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being parahalting good Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . a > 0 holds
Initialized (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) is_pseudo-closed_on s,P

proof end;

theorem :: SCMFSA8C:119

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being parahalting good Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 holds
( Times (a,I) is_closed_on s,P & Times (a,I) is_halting_on s,P )

proof end;

theorem :: SCMFSA8C:120

for I being parahalting good Program of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
Initialized (Times (a,I)) is halting

proof end;

theorem :: SCMFSA8C:121

for I, J being Program of SCM+FSA
for a, c being Int-Location st not I destroys c & not J destroys c holds
( not if=0 (a,I,J) destroys c & not if>0 (a,I,J) destroys c )

proof end;

theorem Th122: :: SCMFSA8C:122

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being parahalting good Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 & s . a > 0 holds
ex s2 being State of SCM+FSA ex P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT ex k being Element of NAT st
( s2 = s +* (Initialize (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) & P2 = P +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) & k = (LifeSpan ((P +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(s +* (Initialize (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 1 & (Comput (P2,s2,k)) . a = (s . a) - 1 & (Comput (P2,s2,k)) . (intloc 0) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (P2,s2,k)) . b = (IExec (I,P,s)) . b ) & ( for f being FinSeq-Location holds (Comput (P2,s2,k)) . f = (IExec (I,P,s)) . f ) & IC (Comput (P2,s2,k)) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (P2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )

proof end;

theorem Th123: :: SCMFSA8C:123

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being parahalting good Program of SCM+FSA
for a being read-write Int-Location st s . (intloc 0) = 1 & s . a <= 0 holds
DataPart (IExec ((Times (a,I)),P,s)) = DataPart s

proof end;

theorem Th124: :: SCMFSA8C:124

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being parahalting good Program of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . a > 0 holds
( (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . a = (s . a) - 1 & DataPart (IExec ((Times (a,I)),P,s)) = DataPart (IExec ((Times (a,I)),P,(IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)))) )

proof end;

begin

theorem :: SCMFSA8C:125

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for a, b, c being read-write Int-Location st a <> b & a <> c & b <> c & s . a >= 0 holds
(IExec ((Times (a,(Macro (AddTo (b,c))))),P,s)) . b = (s . b) + ((s . c) * (s . a))

proof end;