:: While Macro Instructions of SCM+FSA
:: by Jing-Chao Chen
::
:: Received December 10, 1997
:: Copyright (c) 1997 Association of Mizar Users

begin

LL: card (Stop SCM+FSA ) = 1
by SCMNORM:3;

KK: (Stop SCM+FSA ) . 0 = halt SCM+FSA
by AFINSQ_1:38;

JJ: 0 in dom (Stop SCM+FSA )
by SCMNORM:2;

theorem Th1: :: SCMFSA_9:1

for I being Program of SCM+FSA
for a being Int-Location holds card (if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = (card I) + 6

proof end;

theorem Th2: :: SCMFSA_9:2

for I being Program of SCM+FSA
for a being Int-Location holds card (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) = (card I) + 6

proof end;

definition

let a be Int-Location ;
let I be Program of SCM+FSA ;
func while=0 a,I -> Program of SCM+FSA equals :: SCMFSA_9:def 1
(if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 ));
correctness
coherence
(if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 )) is Program of SCM+FSA ;

proof end;

func while>0 a,I -> Program of SCM+FSA equals :: SCMFSA_9:def 2
(if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 ));
correctness
coherence
(if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 )) is Program of SCM+FSA ;

proof end;

end;

:: deftheorem defines while=0 SCMFSA_9:def 1 :

for a being Int-Location
for I being Program of SCM+FSA holds while=0 a,I = (if=0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 ));

:: deftheorem defines while>0 SCMFSA_9:def 2 :

for a being Int-Location
for I being Program of SCM+FSA holds while>0 a,I = (if>0 a,(I ';' (Goto 0 )),(Stop SCM+FSA )) +* (((card I) + 4) .--> (goto 0 ));

theorem Th3: :: SCMFSA_9:3

for I being Program of SCM+FSA
for a being Int-Location holds card (if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto 0 )))) = (card I) + 11

proof end;

definition

let a be Int-Location ;
let I be Program of SCM+FSA ;
func while<0 a,I -> Program of SCM+FSA equals :: SCMFSA_9:def 3
(if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto 0 )))) +* (((card I) + 4) .--> (goto 0 ));
correctness
coherence
(if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto 0 )))) +* (((card I) + 4) .--> (goto 0 )) is Program of SCM+FSA ;

proof end;

end;

:: deftheorem defines while<0 SCMFSA_9:def 3 :

for a being Int-Location
for I being Program of SCM+FSA holds while<0 a,I = (if=0 a,(Stop SCM+FSA ),(if>0 a,(Stop SCM+FSA ),(I ';' (Goto 0 )))) +* (((card I) + 4) .--> (goto 0 ));

theorem Th4: :: SCMFSA_9:4

for I being Program of SCM+FSA
for a being Int-Location holds card (while=0 a,I) = (card I) + 6

proof end;

theorem Th5: :: SCMFSA_9:5

for I being Program of SCM+FSA
for a being Int-Location holds card (while>0 a,I) = (card I) + 6

proof end;

theorem :: SCMFSA_9:6

for I being Program of SCM+FSA
for a being Int-Location holds card (while<0 a,I) = (card I) + 11

proof end;

theorem :: SCMFSA_9:7

for a being Int-Location
for l being Element of NAT holds a =0_goto l <> halt SCM+FSA by SCMFSA_2:48, SCMFSA_2:124;

theorem :: SCMFSA_9:8

for a being Int-Location
for l being Element of NAT holds a >0_goto l <> halt SCM+FSA by SCMFSA_2:49, SCMFSA_2:124;

theorem :: SCMFSA_9:9

for l being Element of NAT holds goto l <> halt SCM+FSA by SCMFSA_2:47, SCMFSA_2:124;

theorem Th10: :: SCMFSA_9:10

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

proof end;

theorem Th11: :: SCMFSA_9:11

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

proof end;

theorem Th12: :: SCMFSA_9:12

for a being Int-Location
for I being Program of SCM+FSA
for k being Element of NAT st k < 6 holds
k in dom (while=0 a,I)

proof end;

theorem Th13: :: SCMFSA_9:13

for a being Int-Location
for I being Program of SCM+FSA
for k being Element of NAT st k < 6 holds
(card I) + k in dom (while=0 a,I)

proof end;

theorem Th14: :: SCMFSA_9:14

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

proof end;

theorem Th15: :: SCMFSA_9:15

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

proof end;

theorem Th16: :: SCMFSA_9:16

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

proof end;

theorem :: SCMFSA_9:17

for a being Int-Location
for I being Program of SCM+FSA
for k being Element of NAT st k < (card I) + 6 holds
k in dom (while=0 a,I)

proof end;

theorem Th18: :: SCMFSA_9:18

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location st s . a <> 0 holds
( while=0 a,I is_halting_on s & while=0 a,I is_closed_on s )

proof end;

theorem Th19: :: SCMFSA_9:19

for a being Int-Location
for I being Program of SCM+FSA
for s being State of SCM+FSA
for k being Element of NAT st I is_closed_on s & I is_halting_on s & k < LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) & IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)) + 4 & DataPart (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) holds
( IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) )

proof end;

theorem Th20: :: SCMFSA_9:20

for a being Int-Location
for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s & I is_halting_on s & IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))))) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))))) + 4 holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))))),(Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))))) = goto ((card I) + 4)

proof end;

theorem Th21: :: SCMFSA_9:21

for a being Int-Location
for I being Program of SCM+FSA holds (while=0 a,I) . ((card I) + 4) = goto 0

proof end;

theorem Th22: :: SCMFSA_9:22

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location st I is_closed_on s & I is_halting_on s & s . a = 0 holds
( IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) = 0 & ( for k being Element of NAT st k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 holds
IC (Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),k) in dom (while=0 a,I) ) )

proof end;

set sl0 = Start-At 0 ,SCM+FSA ;

definition

let s be State of SCM+FSA ;
let I be Program of SCM+FSA ;
let a be read-write Int-Location ;
deffunc H₁( Nat, State of SCM+FSA ) -> set = Comput (ProgramPart ($2 +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),($2 +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan ($2 +* (I +* (Start-At 0 ,SCM+FSA )))) + 3);
deffunc H₂( Nat, State of SCM+FSA ) -> Element of product the Object-Kind of SCM+FSA = down (Comput (ProgramPart ($2 +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),($2 +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan ($2 +* (I +* (Start-At 0 ,SCM+FSA )))) + 3));
func StepWhile=0 a,I,s -> Function of NAT ,(product the Object-Kind of SCM+FSA ) means :Def4: :: SCMFSA_9:def 4
( it . 0 = s & ( for i being Nat holds it . (i + 1) = Comput (ProgramPart ((it . i) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),((it . i) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan ((it . i) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) ) );
existence
ex b₁ being Function of NAT ,(product the Object-Kind of SCM+FSA ) st
( b₁ . 0 = s & ( for i being Nat holds b₁ . (i + 1) = Comput (ProgramPart ((b₁ . i) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),((b₁ . i) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan ((b₁ . i) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) ) )

proof end;

uniqueness
for b₁, b₂ being Function of NAT ,(product the Object-Kind of SCM+FSA ) st b₁ . 0 = s & ( for i being Nat holds b₁ . (i + 1) = Comput (ProgramPart ((b₁ . i) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),((b₁ . i) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan ((b₁ . i) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) ) & b₂ . 0 = s & ( for i being Nat holds b₂ . (i + 1) = Comput (ProgramPart ((b₂ . i) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),((b₂ . i) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan ((b₂ . i) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines StepWhile=0 SCMFSA_9:def 4 :

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location
for b₄ being Function of NAT ,(product the Object-Kind of SCM+FSA ) holds
( b₄ = StepWhile=0 a,I,s iff ( b₄ . 0 = s & ( for i being Nat holds b₄ . (i + 1) = Comput (ProgramPart ((b₄ . i) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),((b₄ . i) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan ((b₄ . i) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) ) ) );

theorem :: SCMFSA_9:23

canceled;

theorem :: SCMFSA_9:24

canceled;

theorem Th25: :: SCMFSA_9:25

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location
for k being Element of NAT holds (StepWhile=0 a,I,s) . (k + 1) = (StepWhile=0 a,I,((StepWhile=0 a,I,s) . k)) . 1

proof end;

theorem :: SCMFSA_9:26

canceled;

theorem :: SCMFSA_9:27

canceled;

theorem :: SCMFSA_9:28

canceled;

theorem Th29: :: SCMFSA_9:29

for s1, s2 being State of SCM+FSA st IC s1 = IC s2 & DataPart s1 = DataPart s2 & s1 | NAT = s2 | NAT holds
s1 = s2

proof end;

theorem Th30: :: SCMFSA_9:30

for I being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA holds (StepWhile=0 a,I,s) . (0 + 1) = Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)

proof end;

theorem Th31: :: SCMFSA_9:31

for I being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA
for k, n being Element of NAT st IC ((StepWhile=0 a,I,s) . k) = 0 & (StepWhile=0 a,I,s) . k = Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),n holds
( (StepWhile=0 a,I,s) . k = ((StepWhile=0 a,I,s) . k) +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )) & (StepWhile=0 a,I,s) . (k + 1) = Comput (ProgramPart (s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while=0 a,I) +* (Start-At 0 ,SCM+FSA ))),(n + ((LifeSpan (((StepWhile=0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) )

proof end;

theorem Th32: :: SCMFSA_9:32

for I being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st ( for k being Nat holds
( I is_closed_on (StepWhile=0 a,I,s) . k & I is_halting_on (StepWhile=0 a,I,s) . k ) ) & ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
for k being Nat holds
( ( f . ((StepWhile=0 a,I,s) . (k + 1)) < f . ((StepWhile=0 a,I,s) . k) or f . ((StepWhile=0 a,I,s) . k) = 0 ) & ( f . ((StepWhile=0 a,I,s) . k) = 0 implies ((StepWhile=0 a,I,s) . k) . a <> 0 ) & ( ((StepWhile=0 a,I,s) . k) . a <> 0 implies f . ((StepWhile=0 a,I,s) . k) = 0 ) ) holds
( while=0 a,I is_halting_on s & while=0 a,I is_closed_on s )

proof end;

theorem Th33: :: SCMFSA_9:33

for I being parahalting Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
for k being Nat holds
( ( f . ((StepWhile=0 a,I,s) . (k + 1)) < f . ((StepWhile=0 a,I,s) . k) or f . ((StepWhile=0 a,I,s) . k) = 0 ) & ( f . ((StepWhile=0 a,I,s) . k) = 0 implies ((StepWhile=0 a,I,s) . k) . a <> 0 ) & ( ((StepWhile=0 a,I,s) . k) . a <> 0 implies f . ((StepWhile=0 a,I,s) . k) = 0 ) ) holds
( while=0 a,I is_halting_on s & while=0 a,I is_closed_on s )

proof end;

theorem :: SCMFSA_9:34

for I being parahalting Program of SCM+FSA
for a being read-write Int-Location st ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
for s being State of SCM+FSA holds
( ( f . ((StepWhile=0 a,I,s) . 1) < f . s or f . s = 0 ) & ( f . s = 0 implies s . a <> 0 ) & ( s . a <> 0 implies f . s = 0 ) ) holds
while=0 a,I is parahalting

proof end;

theorem Th35: :: SCMFSA_9:35

for l1, l2 being Element of NAT
for a being Int-Location holds l1 .--> (goto l2) does_not_destroy a

proof end;

theorem Th36: :: SCMFSA_9:36

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

proof end;

registration

let I, J be good Program of SCM+FSA ;
let a be Int-Location ;
cluster if=0 a,I,J -> good ;
correctness
coherence
if=0 a,I,J is good ;

proof end;

end;

registration

let I be good Program of SCM+FSA ;
let a be Int-Location ;
cluster while=0 a,I -> good ;
correctness
coherence
while=0 a,I is good ;

proof end;

end;

theorem Th37: :: SCMFSA_9:37

for a being Int-Location
for I being Program of SCM+FSA
for k being Element of NAT st k < 6 holds
k in dom (while>0 a,I)

proof end;

theorem Th38: :: SCMFSA_9:38

for a being Int-Location
for I being Program of SCM+FSA
for k being Element of NAT st k < 6 holds
(card I) + k in dom (while>0 a,I)

proof end;

theorem Th39: :: SCMFSA_9:39

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

proof end;

theorem Th40: :: SCMFSA_9:40

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

proof end;

theorem Th41: :: SCMFSA_9:41

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

proof end;

theorem :: SCMFSA_9:42

for a being Int-Location
for I being Program of SCM+FSA
for k being Element of NAT st k < (card I) + 6 holds
k in dom (while>0 a,I)

proof end;

theorem Th43: :: SCMFSA_9:43

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location st s . a <= 0 holds
( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )

proof end;

theorem Th44: :: SCMFSA_9:44

for a being Int-Location
for I being Program of SCM+FSA
for s being State of SCM+FSA
for k being Element of NAT st I is_closed_on s & I is_halting_on s & k < LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))) & IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k)) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + k)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),k) holds
( IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1))) + 4 & DataPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((1 + k) + 1)) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(k + 1)) )

proof end;

theorem Th45: :: SCMFSA_9:45

for a being Int-Location
for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s & I is_halting_on s & IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))))) = (IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))))) + 4 holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA ))))))),(Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(1 + (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))))) = goto ((card I) + 4)

proof end;

theorem Th46: :: SCMFSA_9:46

for a being Int-Location
for I being Program of SCM+FSA holds (while>0 a,I) . ((card I) + 4) = goto 0

proof end;

theorem Th47: :: SCMFSA_9:47

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location st I is_closed_on s & I is_halting_on s & s . a > 0 holds
( IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) = 0 & ( for k being Element of NAT st k <= (LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3 holds
IC (Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),k) in dom (while>0 a,I) ) )

proof end;

set sl0 = Start-At 0 ,SCM+FSA ;

definition

let s be State of SCM+FSA ;
let I be Program of SCM+FSA ;
let a be read-write Int-Location ;
deffunc H₁( Nat, Element of product the Object-Kind of SCM+FSA ) -> set = Comput (ProgramPart ($2 +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),($2 +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan ($2 +* (I +* (Start-At 0 ,SCM+FSA )))) + 3);
deffunc H₂( Nat, Element of product the Object-Kind of SCM+FSA ) -> Element of product the Object-Kind of SCM+FSA = down (Comput (ProgramPart ($2 +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),($2 +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan ($2 +* (I +* (Start-At 0 ,SCM+FSA )))) + 3));
func StepWhile>0 a,I,s -> Function of NAT ,(product the Object-Kind of SCM+FSA ) means :Def5: :: SCMFSA_9:def 5
( it . 0 = s & ( for i being Nat holds it . (i + 1) = Comput (ProgramPart ((it . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((it . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan ((it . i) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) ) );
existence
ex b₁ being Function of NAT ,(product the Object-Kind of SCM+FSA ) st
( b₁ . 0 = s & ( for i being Nat holds b₁ . (i + 1) = Comput (ProgramPart ((b₁ . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((b₁ . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan ((b₁ . i) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) ) )

proof end;

uniqueness
for b₁, b₂ being Function of NAT ,(product the Object-Kind of SCM+FSA ) st b₁ . 0 = s & ( for i being Nat holds b₁ . (i + 1) = Comput (ProgramPart ((b₁ . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((b₁ . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan ((b₁ . i) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) ) & b₂ . 0 = s & ( for i being Nat holds b₂ . (i + 1) = Comput (ProgramPart ((b₂ . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((b₂ . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan ((b₂ . i) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines StepWhile>0 SCMFSA_9:def 5 :

for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location
for b₄ being Function of NAT ,(product the Object-Kind of SCM+FSA ) holds
( b₄ = StepWhile>0 a,I,s iff ( b₄ . 0 = s & ( for i being Nat holds b₄ . (i + 1) = Comput (ProgramPart ((b₄ . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),((b₄ . i) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan ((b₄ . i) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3) ) ) );

theorem :: SCMFSA_9:48

canceled;

theorem :: SCMFSA_9:49

canceled;

theorem Th50: :: SCMFSA_9:50

for k being Element of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being read-write Int-Location holds (StepWhile>0 a,I,s) . (k + 1) = (StepWhile>0 a,I,((StepWhile>0 a,I,s) . k)) . 1

proof end;

theorem Th51: :: SCMFSA_9:51

for I being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA holds (StepWhile>0 a,I,s) . (0 + 1) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (s +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)

proof end;

theorem Th52: :: SCMFSA_9:52

for I being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA
for k, n being Element of NAT st IC ((StepWhile>0 a,I,s) . k) = 0 & (StepWhile>0 a,I,s) . k = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),n holds
( (StepWhile>0 a,I,s) . k = ((StepWhile>0 a,I,s) . k) +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )) & (StepWhile>0 a,I,s) . (k + 1) = Comput (ProgramPart (s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((while>0 a,I) +* (Start-At 0 ,SCM+FSA ))),(n + ((LifeSpan (((StepWhile>0 a,I,s) . k) +* (I +* (Start-At 0 ,SCM+FSA )))) + 3)) )

proof end;

theorem Th53: :: SCMFSA_9:53

for I being Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st ( for k being Nat holds
( I is_closed_on (StepWhile>0 a,I,s) . k & I is_halting_on (StepWhile>0 a,I,s) . k ) ) & ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
for k being Nat holds
( ( f . ((StepWhile>0 a,I,s) . (k + 1)) < f . ((StepWhile>0 a,I,s) . k) or f . ((StepWhile>0 a,I,s) . k) = 0 ) & ( f . ((StepWhile>0 a,I,s) . k) = 0 implies ((StepWhile>0 a,I,s) . k) . a <= 0 ) & ( ((StepWhile>0 a,I,s) . k) . a <= 0 implies f . ((StepWhile>0 a,I,s) . k) = 0 ) ) holds
( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )

proof end;

theorem Th54: :: SCMFSA_9:54

for I being parahalting Program of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
for k being Nat holds
( ( f . ((StepWhile>0 a,I,s) . (k + 1)) < f . ((StepWhile>0 a,I,s) . k) or f . ((StepWhile>0 a,I,s) . k) = 0 ) & ( f . ((StepWhile>0 a,I,s) . k) = 0 implies ((StepWhile>0 a,I,s) . k) . a <= 0 ) & ( ((StepWhile>0 a,I,s) . k) . a <= 0 implies f . ((StepWhile>0 a,I,s) . k) = 0 ) ) holds
( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )

proof end;

theorem :: SCMFSA_9:55

for I being parahalting Program of SCM+FSA
for a being read-write Int-Location st ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
for s being State of SCM+FSA holds
( ( f . ((StepWhile>0 a,I,s) . 1) < f . s or f . s = 0 ) & ( f . s = 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s = 0 ) ) holds
while>0 a,I is parahalting

proof end;

registration

let I, J be good Program of SCM+FSA ;
let a be Int-Location ;
cluster if>0 a,I,J -> good ;
coherence
if>0 a,I,J is good

proof end;

end;

registration

let I be good Program of SCM+FSA ;
let a be Int-Location ;
cluster while>0 a,I -> good ;
correctness
coherence
while>0 a,I is good ;

proof end;

end;