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

begin

theorem :: SCMFSA8C:1

canceled;

theorem Th2: :: SCMFSA8C:2

for s being State of SCM+FSA
for P being initial FinPartState of SCM+FSA st P is_pseudo-closed_on s holds
for k being Element of NAT st ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart (s +* (P +* (Start-At 0 ,SCM+FSA )))),(s +* (P +* (Start-At 0 ,SCM+FSA ))),n) in dom P ) holds
k < pseudo-LifeSpan s,P

proof end;

theorem :: SCMFSA8C:3

canceled;

theorem :: SCMFSA8C:4

canceled;

theorem :: SCMFSA8C:5

canceled;

theorem :: SCMFSA8C:6

canceled;

theorem :: SCMFSA8C:7

canceled;

theorem Th8: :: SCMFSA8C:8

for i being Instruction of SCM+FSA holds IncAddr i,0 = i

proof end;

theorem Th9: :: SCMFSA8C:9

for P being preProgram of SCM+FSA holds ProgramPart (Relocated P,0 ) = P

proof end;

theorem :: SCMFSA8C:10

canceled;

theorem :: SCMFSA8C:11

canceled;

theorem Th12: :: SCMFSA8C:12

for P, Q being FinPartState of SCM+FSA
for k being Element of NAT st P c= Q holds
ProgramPart (Relocated P,k) c= ProgramPart (Relocated Q,k)

proof end;

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
Initialize s = s

proof end;

theorem Th15: :: SCMFSA8C:15

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

proof end;

theorem Th16: :: SCMFSA8C:16

for s being State of SCM+FSA
for I being Program of SCM+FSA holds s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) = (Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))

proof end;

theorem Th17: :: SCMFSA8C:17

for s being State of SCM+FSA
for I being Program of SCM+FSA holds IExec I,s = IExec I,(Initialize 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 +* (I +* (Start-At 0 ,SCM+FSA )) = s +* (Initialized I)

proof end;

theorem Th19: :: SCMFSA8C:19

for I being Program of SCM+FSA holds I +* (Start-At 0 ,SCM+FSA ) 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 s being State of SCM+FSA
for I being Program of SCM+FSA holds
( Initialized I is_closed_on s iff I is_closed_on Initialize s )

proof end;

theorem Th22: :: SCMFSA8C:22

for s being State of SCM+FSA
for I being Program of SCM+FSA holds
( Initialized I is_halting_on s iff I is_halting_on Initialize s )

proof end;

theorem :: SCMFSA8C:23

for I being Program of SCM+FSA st ( for s being State of SCM+FSA holds I is_halting_on Initialize s ) 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 holds Initialized I is_halting_on s ) holds
Initialized I is halting

proof end;

theorem :: SCMFSA8C:25

for I being Program of SCM+FSA holds ProgramPart (Initialized I) = I by SCMFSA6A:33;

theorem Th26: :: 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 (Initialize 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 SCM+FSA 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 SCM+FSA ) = l

proof end;

theorem Th31: :: SCMFSA8C:31

for s being State of SCM+FSA
for P being FinPartState of SCM+FSA
for l being Element of NAT holds IC (s +* (P +* (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

for s being State of SCM+FSA
for P being preProgram of SCM+FSA holds DataPart (s +* P) = DataPart s

proof end;

theorem Th35: :: SCMFSA8C:35

for s, ss being State of SCM+FSA holds DataPart (s +* (ss | NAT )) = DataPart s

proof end;

theorem Th36: :: SCMFSA8C:36

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

proof end;

theorem Th37: :: SCMFSA8C:37

for s, ss being State of SCM+FSA
for I being Program of SCM+FSA holds DataPart (ss +* (s | NAT )) = DataPart ss

proof end;

theorem Th38: :: SCMFSA8C:38

for s being State of SCM+FSA holds IExec (Stop SCM+FSA ),s = (Initialize s) +* (Start-At 0 ,SCM+FSA )

proof end;

theorem Th39: :: SCMFSA8C:39

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s holds
0 in dom I

proof end;

theorem :: SCMFSA8C:40

for s being State of SCM+FSA
for I being paraclosed Program of SCM+FSA holds 0 in dom I

proof end;

theorem :: SCMFSA8C:41

for i being Instruction of SCM+FSA holds rng (Macro i) = {i,(halt SCM+FSA )} by FUNCT_4:67;

theorem Th42: :: SCMFSA8C:42

for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1 & I +* (Start-At 0 ,SCM+FSA ) c= s1 holds
for n being Element of NAT st ProgramPart (Relocated I,n) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) )

proof end;

theorem Th43: :: SCMFSA8C:43

for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1 & I +* (Start-At 0 ,SCM+FSA ) c= s1 & I +* (Start-At 0 ,SCM+FSA ) c= s2 & DataPart s1 = DataPart s2 holds
for i being Element of NAT holds
( IC (Comput (ProgramPart s1),s1,i) = IC (Comput (ProgramPart s2),s2,i) & CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) & DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) )

proof end;

theorem Th44: :: SCMFSA8C:44

for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1 & I is_halting_on s1 & I +* (Start-At 0 ,SCM+FSA ) c= s1 & I +* (Start-At 0 ,SCM+FSA ) c= s2 & DataPart s1 = DataPart s2 holds
LifeSpan s1 = LifeSpan s2

proof end;

theorem Th45: :: SCMFSA8C:45

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 & I is_halting_on s1 & ( 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,s1) = DataPart (IExec I,s2)

proof end;

theorem Th46: :: SCMFSA8C:46

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 & I is_halting_on s1 & DataPart s1 = DataPart s2 holds
DataPart (IExec I,s1) = DataPart (IExec I,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 s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA holds
( ( Initialized I is_pseudo-closed_on s implies ( I is_pseudo-closed_on Initialize s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) & ( I is_pseudo-closed_on Initialize s implies ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) )
let I be Program of SCM+FSA ; :: thesis: ( ( Initialized I is_pseudo-closed_on s implies ( I is_pseudo-closed_on Initialize s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) & ( I is_pseudo-closed_on Initialize s implies ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I ) ) )
set k = pseudo-LifeSpan (Initialize s),I;
A1: ProgramPart (Initialized I) = I by SCMFSA6A:33;

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

set k = pseudo-LifeSpan s,(Initialized I);
X: s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) = (Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )) by Th16;
assume A2: Initialized I is_pseudo-closed_on s ; :: thesis: ( I is_pseudo-closed_on Initialize s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I )
then IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,(Initialized I))) = card (ProgramPart (Initialized I)) by SCMFSA8A:def 5;
then IC (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,(Initialized I))) = card (ProgramPart (Initialized I)) by X;
then A3: IC (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,(Initialized I))) = card (ProgramPart I) by A1, AMI_1:105;

A4: now

let n be Element of NAT ; :: thesis: ( n < pseudo-LifeSpan s,(Initialized I) implies IC (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I )
X: s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) = (Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )) by Th16;
assume n < pseudo-LifeSpan s,(Initialized I) ; :: thesis: IC (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I
then IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),n) in dom (Initialized I) by A2, SCMFSA8A:def 5;
then IC (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom (Initialized I) by X;
hence IC (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I by Th20; :: thesis: verum

end;

hence A5: I is_pseudo-closed_on Initialize s by A3, SCMFSA8A:def 3; :: thesis: pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I
for n being Element of NAT st not IC (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I holds
pseudo-LifeSpan s,(Initialized I) <= n by A4;
hence pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I by A3, A5, SCMFSA8A:def 5; :: thesis: verum

end;

X: s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) = (Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )) by Th16;
assume A6: I is_pseudo-closed_on Initialize s ; :: thesis: ( Initialized I is_pseudo-closed_on s & pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I )
then IC (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan (Initialize s),I)) = card (ProgramPart I) by SCMFSA8A:def 5;
then IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan (Initialize s),I)) = card (ProgramPart I) by X;
then A7: IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan (Initialize s),I)) = card (ProgramPart (Initialized I)) by A1, AMI_1:105;

A8: now

let n be Element of NAT ; :: thesis: ( n < pseudo-LifeSpan (Initialize s),I implies IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),n) in dom (Initialized I) )
X: s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )) = (Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )) by Th16;
assume n < pseudo-LifeSpan (Initialize s),I ; :: thesis: IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),n) in dom (Initialized I)
then IC (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I by A6, SCMFSA8A:def 5;
then IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),n) in dom I by X;
hence IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),n) in dom (Initialized I) by Th20; :: thesis: verum

end;

hence A9: Initialized I is_pseudo-closed_on s by A7, SCMFSA8A:def 3; :: thesis: pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I
for n being Element of NAT st not IC (Comput (ProgramPart (s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Initialized I) +* (Start-At 0 ,SCM+FSA ))),n) in dom (Initialized I) holds
pseudo-LifeSpan (Initialize s),I <= n by A8;
hence pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I by A7, A9, SCMFSA8A:def 5; :: thesis: verum

end;

theorem :: SCMFSA8C:47

for s being State of SCM+FSA
for I being Program of SCM+FSA holds
( Initialized I is_pseudo-closed_on s iff I is_pseudo-closed_on Initialize s ) by Lm1;

theorem :: SCMFSA8C:48

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_pseudo-closed_on Initialize s holds
pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I by Lm1;

theorem :: SCMFSA8C:49

for s being State of SCM+FSA
for I being Program of SCM+FSA st Initialized I is_pseudo-closed_on s holds
pseudo-LifeSpan s,(Initialized I) = pseudo-LifeSpan (Initialize s),I by Lm1;

theorem Th50: :: SCMFSA8C:50

for s being State of SCM+FSA
for I being initial FinPartState of SCM+FSA st I is_pseudo-closed_on s holds
( I is_pseudo-closed_on s +* (I +* (Start-At 0 ,SCM+FSA )) & pseudo-LifeSpan s,I = pseudo-LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))),I )

proof end;

theorem Th51: :: SCMFSA8C:51

for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I +* (Start-At 0 ,SCM+FSA ) c= s1 & I is_pseudo-closed_on s1 holds
for n being Element of NAT st ProgramPart (Relocated I,n) c= s2 & IC s2 = n & DataPart s1 = DataPart s2 holds
( ( for i being Element of NAT st i < pseudo-LifeSpan s1,I holds
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),(Comput (ProgramPart s2),s2,i) ) & ( for i being Element of NAT st i <= pseudo-LifeSpan s1,I holds
( (IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) & DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) ) ) )

proof end;

theorem Th52: :: SCMFSA8C:52

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 holds
I is_pseudo-closed_on s2

proof end;

theorem Th53: :: SCMFSA8C:53

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 iff I is_pseudo-closed_on Initialize s )

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 s being State of SCM+FSA
for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s holds
( I ';' (Stop SCM+FSA ) is_closed_on s & I ';' (Stop SCM+FSA ) is_halting_on s & LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = pseudo-LifeSpan s,(Directed I) & ( for n being Element of NAT st n < pseudo-LifeSpan s,(Directed I) holds
IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) = IC (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),n) ) & ( for n being Element of NAT st n <= pseudo-LifeSpan s,(Directed I) holds
DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) = DataPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),n) ) )

proof end;

theorem Th59: :: SCMFSA8C:59

for s being State of SCM+FSA
for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s holds
DataPart (Result (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,(Directed I)))

proof end;

theorem :: SCMFSA8C:60

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 holds
DataPart (IExec (I ';' (Stop SCM+FSA )),s) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,(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 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 holds
( if=0 a,I,J is_halting_on s & if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) + 1 )

proof end;

theorem :: SCMFSA8C:67

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 holds
DataPart (IExec (if=0 a,I,J),s) = DataPart (IExec (I ';' (Stop SCM+FSA )),s)

proof end;

theorem Th68: :: SCMFSA8C:68

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 holds
( if>0 a,I,J is_halting_on s & if>0 a,I,J is_closed_on s & LifeSpan (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) + 1 )

proof end;

theorem Th69: :: SCMFSA8C:69

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 holds
DataPart (IExec (if>0 a,I,J),s) = DataPart (IExec (I ';' (Stop SCM+FSA )),s)

proof end;

theorem Th70: :: SCMFSA8C:70

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 holds
( if=0 a,I,J is_halting_on s & if=0 a,I,J is_closed_on s & LifeSpan (s +* ((if=0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) + 3 )

proof end;

theorem :: SCMFSA8C:71

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 holds
DataPart (IExec (if=0 a,I,J),s) = DataPart (IExec (J ';' (Stop SCM+FSA )),s)

proof end;

theorem Th72: :: SCMFSA8C:72

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 holds
( if>0 a,I,J is_halting_on s & if>0 a,I,J is_closed_on s & LifeSpan (s +* ((if>0 a,I,J) +* (Start-At 0 ,SCM+FSA ))) = (LifeSpan (s +* ((J ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) + 3 )

proof end;

theorem Th73: :: SCMFSA8C:73

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 holds
DataPart (IExec (if>0 a,I,J),s) = DataPart (IExec (J ';' (Stop SCM+FSA )),s)

proof end;

theorem :: SCMFSA8C:74

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 & Directed J is_pseudo-closed_on s holds
( if=0 a,I,J is_closed_on s & if=0 a,I,J is_halting_on s )

proof end;

theorem :: SCMFSA8C:75

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 & Directed J is_pseudo-closed_on s holds
( if>0 a,I,J is_closed_on s & if>0 a,I,J is_halting_on s )

proof end;

theorem :: SCMFSA8C:76

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

theorem Th77: :: SCMFSA8C:77

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

proof end;

theorem Th78: :: SCMFSA8C:78

for a being Int-Location holds halt SCM+FSA does_not_refer a

proof end;

theorem :: SCMFSA8C:79

for a, b, c being Int-Location st a <> b holds
AddTo c,b does_not_refer a

proof end;

theorem :: SCMFSA8C:80

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

proof end;

theorem Th81: :: SCMFSA8C:81

for I, J being Program of SCM+FSA
for a being Int-Location st I does_not_destroy a & J does_not_destroy a holds
I ';' J does_not_destroy 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 i does_not_destroy a & J does_not_destroy a holds
i ';' J does_not_destroy 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 I does_not_destroy a & j does_not_destroy a holds
I ';' j does_not_destroy a

proof end;

theorem :: SCMFSA8C:84

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

proof end;

theorem Th85: :: SCMFSA8C:85

for a being Int-Location holds Stop SCM+FSA does_not_destroy a

proof end;

theorem Th86: :: SCMFSA8C:86

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

proof end;

theorem Th87: :: SCMFSA8C:87

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_halting_on Initialize s holds
( ( for a being read-write Int-Location holds (IExec I,s) . a = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . a ) & ( for f being FinSeq-Location holds (IExec I,s) . f = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . f ) )

proof end;

theorem Th88: :: SCMFSA8C:88

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,s) . a = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))))) . a

proof end;

theorem Th89: :: SCMFSA8C:89

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 Initialize s & I is_halting_on Initialize s & I does_not_destroy a holds
(IExec I,s) . a = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),k) . a

proof end;

theorem Th90: :: SCMFSA8C:90

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 I does_not_destroy a holds
(IExec I,s) . a = (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),k) . a

proof end;

theorem Th91: :: SCMFSA8C:91

for s being State of SCM+FSA
for I being parahalting Program of SCM+FSA
for a being Int-Location st I does_not_destroy a holds
(IExec I,s) . a = (Initialize s) . a

proof end;

theorem Th92: :: SCMFSA8C:92

for s being State of SCM+FSA
for I being keeping_0 Program of SCM+FSA st I is_halting_on Initialize s holds
( (IExec I,s) . (intloc 0 ) = 1 & ( for k being Element of NAT holds (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),k) . (intloc 0 ) = 1 ) )

proof end;

theorem Th93: :: SCMFSA8C:93

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location st I does_not_destroy a holds
for k being Element of NAT st IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) in dom I holds
(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) . a = (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) . a

proof end;

theorem Th94: :: SCMFSA8C:94

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location st I does_not_destroy a holds
for m being Element of NAT st ( for n being Element of NAT st n < m holds
IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I ) holds
for n being Element of NAT st n <= m holds
(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) . a = s . a

proof end;

theorem Th95: :: SCMFSA8C:95

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 (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) in dom I ) holds
for n being Element of NAT st n <= m holds
(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) . (intloc 0 ) = s . (intloc 0 )

proof end;

theorem Th96: :: SCMFSA8C:96

for s being State of SCM+FSA
for I being good Program of SCM+FSA st I is_halting_on Initialize s & I is_closed_on Initialize s holds
( (IExec I,s) . (intloc 0 ) = 1 & ( for k being Element of NAT holds (Comput (ProgramPart ((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (I +* (Start-At 0 ,SCM+FSA ))),k) . (intloc 0 ) = 1 ) )

proof end;

theorem :: SCMFSA8C:97

for s being State of SCM+FSA
for I being good Program of SCM+FSA st I is_closed_on s holds
for k being Element of NAT holds (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) . (intloc 0 ) = s . (intloc 0 )

proof end;

theorem Th98: :: SCMFSA8C:98

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 I does_not_destroy a holds
(Comput (ProgramPart ((Initialize s) +* ((I ';' (SubFrom a,(intloc 0 ))) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* ((I ';' (SubFrom a,(intloc 0 ))) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan ((Initialize s) +* ((I ';' (SubFrom a,(intloc 0 ))) +* (Start-At 0 ,SCM+FSA ))))) . a = (s . a) - 1

proof end;

theorem Th99: :: SCMFSA8C:99

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

proof end;

theorem Th100: :: SCMFSA8C:100

for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1 & I is_halting_on s1 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds
( Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),k, Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),k equal_outside NAT & CurInstr (ProgramPart (Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),k)),(Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),k) = CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),k)),(Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),k) )

proof end;

theorem Th101: :: SCMFSA8C:101

for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1 & I is_halting_on s1 & DataPart s1 = DataPart s2 holds
( LifeSpan (s1 +* (I +* (Start-At 0 ,SCM+FSA ))) = LifeSpan (s2 +* (I +* (Start-At 0 ,SCM+FSA ))) & Result (s1 +* (I +* (Start-At 0 ,SCM+FSA ))), Result (s2 +* (I +* (Start-At 0 ,SCM+FSA ))) equal_outside NAT )

proof end;

theorem :: SCMFSA8C:102

canceled;

theorem Th103: :: SCMFSA8C:103

for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s1 & I is_halting_on s1 & I +* (Start-At 0 ,SCM+FSA ) c= s1 & I +* (Start-At 0 ,SCM+FSA ) c= s2 & ex k being Element of NAT st Comput (ProgramPart s1),s1,k,s2 equal_outside NAT holds
Result s1, Result 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 -> 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 ;

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 I does_not_destroy a holds
loop I does_not_destroy 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 s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
for m being Element of NAT st m <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) holds
Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),m, Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),m equal_outside NAT

proof end;

theorem Th110: :: SCMFSA8C:110

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
for m being Element of NAT st m < LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),m)),(Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),m) = CurInstr (ProgramPart (Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),m)),(Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),m)

proof end;

Lm2: for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( CurInstr (ProgramPart (Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))))),(Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),m)),(Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),m) <> halt SCM+FSA ) )

proof end;

theorem :: SCMFSA8C:111

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
for m being Element of NAT st m <= LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),m)),(Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),m) <> halt SCM+FSA by Lm2;

theorem :: SCMFSA8C:112

for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))))),(Comput (ProgramPart (s +* ((loop I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((loop I) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))) = goto 0 by Lm2;

theorem Th113: :: SCMFSA8C:113

for s being State of SCM+FSA
for I being paraclosed Program of SCM+FSA st I +* (Start-At 0 ,SCM+FSA ) c= s & ProgramPart s halts_on s holds
for m being Element of NAT st m <= LifeSpan s holds
Comput (ProgramPart s),s,m, Comput (ProgramPart (s +* (loop I))),(s +* (loop I)),m equal_outside NAT

proof end;

theorem :: SCMFSA8C:114

for s being State of SCM+FSA
for I being parahalting Program of SCM+FSA st Initialized I c= s holds
for k being Element of NAT st k <= LifeSpan s holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (loop I))),(s +* (loop I)),k)),(Comput (ProgramPart (s +* (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 );

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 s being State of SCM+FSA
for I being parahalting good Program of SCM+FSA
for a being read-write Int-Location st I does_not_destroy 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

proof end;

theorem :: SCMFSA8C:118

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

proof end;

theorem :: SCMFSA8C:119

for s being State of SCM+FSA
for I being parahalting good Program of SCM+FSA
for a being read-write Int-Location st I does_not_destroy a & s . (intloc 0 ) = 1 holds
( Times a,I is_closed_on s & Times a,I is_halting_on s )

proof end;

theorem :: SCMFSA8C:120

for I being parahalting good Program of SCM+FSA
for a being read-write Int-Location st I does_not_destroy 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 I does_not_destroy c & J does_not_destroy c holds
( if=0 a,I,J does_not_destroy c & if>0 a,I,J does_not_destroy c )

proof end;

theorem Th122: :: SCMFSA8C:122

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

proof end;

theorem Th123: :: SCMFSA8C:123

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),s) = DataPart s

proof end;

theorem Th124: :: SCMFSA8C:124

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

proof end;

begin

theorem :: SCMFSA8C:125

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))),s) . b = (s . b) + ((s . c) * (s . a))

proof end;