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


begin

Lm1:  card (Stop SCM+FSA) = 1
by AFINSQ_1:33;

Lm2:  (Stop SCM+FSA) . 0 = halt SCM+FSA
by AFINSQ_1:34;

Lm3:  0 in dom (Stop SCM+FSA)
by COMPOS_1:3;

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

theorem Th1: :: SCMFSA_9:1
for I being Program of
for a being Int-Location holds card (if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) = (card I) + 6
proofend;

theorem Th2: :: SCMFSA_9:2
for I being Program of
for a being Int-Location holds card (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) = (card I) + 6
proofend;

definition
let a be Int-Location;
let I be Program of ;
func while=0 (a,I) ->  Program of  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 ;
proofend;
func while>0 (a,I) ->  Program of  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 ;
proofend;
end;

:: deftheorem  defines while=0 SCMFSA_9:def_1_:_
 for a being Int-Location
for I being Program of 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 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
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
proofend;

definition
let a be Int-Location;
let I be Program of ;
func while<0 (a,I) ->  Program of  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 ;
proofend;
end;

:: deftheorem  defines while<0 SCMFSA_9:def_3_:_
 for a being Int-Location
for I being Program of 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
for a being Int-Location holds card (while=0 (a,I)) = (card I) + 6
proofend;

theorem Th5: :: SCMFSA_9:5
for I being Program of
for a being Int-Location holds card (while>0 (a,I)) = (card I) + 6
proofend;

theorem :: SCMFSA_9:6
for I being Program of
for a being Int-Location holds card (while<0 (a,I)) = (card I) + 11
proofend;

theorem :: SCMFSA_9:7
canceled;

theorem :: SCMFSA_9:8
canceled;

theorem :: SCMFSA_9:9
canceled;

theorem Th10: :: SCMFSA_9:10
for a being Int-Location
for I being Program of holds
( 0 in dom (while=0 (a,I)) &amp; 1 in dom (while=0 (a,I)) &amp; 0 in dom (while>0 (a,I)) &amp; 1 in dom (while>0 (a,I)) )
proofend;

theorem Th11: :: SCMFSA_9:11
for a being Int-Location
for I being Program of holds
( (while=0 (a,I)) . 0 = a =0_goto 4 &amp; (while=0 (a,I)) . 1 = goto 2 &amp; (while>0 (a,I)) . 0 = a >0_goto 4 &amp; (while>0 (a,I)) . 1 = goto 2 )
proofend;

theorem Th12: :: SCMFSA_9:12
for a being Int-Location
for I being Program of
for k being Element of NAT st k < 6 holds
k in dom (while=0 (a,I))
proofend;

theorem Th13: :: SCMFSA_9:13
for a being Int-Location
for I being Program of
for k being Element of NAT st k < 6 holds
(card I) + k in dom (while=0 (a,I))
proofend;

theorem Th14: :: SCMFSA_9:14
for a being Int-Location
for I being Program of holds (while=0 (a,I)) . ((card I) + 5) = halt SCM+FSA
proofend;

theorem Th15: :: SCMFSA_9:15
for a being Int-Location
for I being Program of holds (while=0 (a,I)) . 3 = goto ((card I) + 5)
proofend;

theorem Th16: :: SCMFSA_9:16
for a being Int-Location
for I being Program of holds (while=0 (a,I)) . 2 = goto 3
proofend;

theorem :: SCMFSA_9:17
for a being Int-Location
for I being Program of
for k being Element of NAT st k < (card I) + 6 holds
k in dom (while=0 (a,I))
proofend;

theorem Th18: :: SCMFSA_9:18
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of
for a being read-write Int-Location st s . a <> 0 holds
( while=0 (a,I) is_halting_on s,P &amp; while=0 (a,I) is_closed_on s,P )
proofend;

theorem Th19: :: SCMFSA_9:19
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for I being Program of
for s being State of SCM+FSA
for k being Element of NAT st I is_closed_on s,P &amp; I is_halting_on s,P &amp; k < LifeSpan ((P +* I),(Initialize s)) &amp; IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 4 &amp; DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) holds
( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize s),(k + 1)))) + 4 &amp; DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) )
proofend;

theorem Th20: :: SCMFSA_9:20
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for I being Program of
for s being State of SCM+FSA st I is_closed_on s,P &amp; I is_halting_on s,P &amp; IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))) = (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) + 4 holds
CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto ((card I) + 4)
proofend;

theorem Th21: :: SCMFSA_9:21
for a being Int-Location
for I being Program of holds (while=0 (a,I)) . ((card I) + 4) = goto 0
proofend;

theorem Th22: :: SCMFSA_9:22
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of
for a being read-write Int-Location st I is_closed_on s,P &amp; I is_halting_on s,P &amp; s . a = 0 holds
( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 3))) = 0 &amp; ( for k being Element of NAT st k <= (LifeSpan ((P +* I),(Initialize s))) + 3 holds
IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) )
proofend;

definition
let s be State of SCM+FSA;
let I be Program of ;
let a be read-write Int-Location;
let P be Instruction-Sequence of SCM+FSA;
deffunc H1( Nat, State of SCM+FSA) ->  set = Comput ((P +* (while=0 (a,I))),($2 +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while=0 (a,I))) +* I),($2 +* (Start-At (0,SCM+FSA))))) + 3));
deffunc H2( Nat, State of SCM+FSA) ->  Element of product (the_Values_of SCM+FSA) = down H1($1,$2);
func StepWhile=0 (a,I,P,s) ->  Function of NAT,(product (the_Values_of SCM+FSA)) means :Def4: :: SCMFSA_9:def 4
( it . 0 = s &amp; ( for i being Nat holds it . (i + 1) = Comput ((P +* (while=0 (a,I))),((it . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while=0 (a,I))) +* I),((it . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) );
existence
 ex b1 being Function of NAT,(product (the_Values_of SCM+FSA)) st
( b1 . 0 = s &amp; ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while=0 (a,I))),((b1 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while=0 (a,I))) +* I),((b1 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) )
proofend;
uniqueness
 for b1, b2 being Function of NAT,(product (the_Values_of SCM+FSA)) st b1 . 0 = s &amp; ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while=0 (a,I))),((b1 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while=0 (a,I))) +* I),((b1 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) &amp; b2 . 0 = s &amp; ( for i being Nat holds b2 . (i + 1) = Comput ((P +* (while=0 (a,I))),((b2 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while=0 (a,I))) +* I),((b2 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines StepWhile=0 SCMFSA_9:def_4_:_
 for s being State of SCM+FSA
for I being Program of
for a being read-write Int-Location
for P being Instruction-Sequence of SCM+FSA
for b5 being Function of NAT,(product (the_Values_of SCM+FSA)) holds
( b5 = StepWhile=0 (a,I,P,s) iff ( b5 . 0 = s &amp; ( for i being Nat holds b5 . (i + 1) = Comput ((P +* (while=0 (a,I))),((b5 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while=0 (a,I))) +* I),((b5 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) ) );

theorem Th23: :: SCMFSA_9:23
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of
for a being read-write Int-Location
for k being Element of NAT holds (StepWhile=0 (a,I,P,s)) . (k + 1) = (StepWhile=0 (a,I,P,((StepWhile=0 (a,I,P,s)) . k))) . 1
proofend;

theorem :: SCMFSA_9:24
canceled;

theorem Th25: :: SCMFSA_9:25
for P being Instruction-Sequence of SCM+FSA
for I being Program of
for a being read-write Int-Location
for s being State of SCM+FSA holds (StepWhile=0 (a,I,P,s)) . (0 + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize s))) + 3))
proofend;

theorem Th26: :: SCMFSA_9:26
for P being Instruction-Sequence of SCM+FSA
for I being Program of
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,P,s)) . k) = 0 &amp; (StepWhile=0 (a,I,P,s)) . k = Comput ((P +* (while=0 (a,I))),(Initialize s),n) holds
( (StepWhile=0 (a,I,P,s)) . k = Initialize ((StepWhile=0 (a,I,P,s)) . k) &amp; (StepWhile=0 (a,I,P,s)) . (k + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),(n + ((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,P,s)) . k)))) + 3))) )
proofend;

theorem Th27: :: SCMFSA_9:27
for P being Instruction-Sequence of SCM+FSA
for I being Program of
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,P,s)) . k,P +* (while=0 (a,I)) &amp; I is_halting_on (StepWhile=0 (a,I,P,s)) . k,P +* (while=0 (a,I)) ) ) &amp; ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for k being Nat holds
( ( f . ((StepWhile=0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,P,s)) . k) or f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) &amp; ( f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) &amp; ( ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 implies f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) ) holds
( while=0 (a,I) is_halting_on s,P &amp; while=0 (a,I) is_closed_on s,P )
proofend;

theorem Th28: :: SCMFSA_9:28
for P being Instruction-Sequence of SCM+FSA
for I being parahalting Program of
for a being read-write Int-Location
for s being State of SCM+FSA st ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for k being Nat holds
( ( f . ((StepWhile=0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,P,s)) . k) or f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) &amp; ( f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) &amp; ( ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 implies f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) ) holds
( while=0 (a,I) is_halting_on s,P &amp; while=0 (a,I) is_closed_on s,P )
proofend;

theorem :: SCMFSA_9:29
for I being parahalting Program of
for a being read-write Int-Location st ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( ( f . ((StepWhile=0 (a,I,P,s)) . 1) < f . s or f . s = 0 ) &amp; ( f . s = 0 implies s . a <> 0 ) &amp; ( s . a <> 0 implies f . s = 0 ) ) holds
while=0 (a,I) is parahalting
proofend;

theorem Th30: :: SCMFSA_9:30
for l1, l2 being Element of NAT
for a being Int-Location holds not l1 .--> (goto l2) destroys a
proofend;

theorem Th31: :: SCMFSA_9:31
for i being Instruction of SCM+FSA st not i destroys intloc 0 holds
Macro i is good
proofend;

registration
let I, J be good Program of ;
let a be Int-Location;
cluster if=0 (a,I,J) ->  good ;
correctness
coherence
if=0 (a,I,J) is good ;
proofend;
end;

registration
let I be good Program of ;
let a be Int-Location;
cluster while=0 (a,I) ->  good ;
correctness
coherence
while=0 (a,I) is good ;
proofend;
end;

:: -----------------------------------------------------------
:: WHILE>0 Statement
theorem Th32: :: SCMFSA_9:32
for a being Int-Location
for I being Program of
for k being Element of NAT st k < 6 holds
k in dom (while>0 (a,I))
proofend;

theorem Th33: :: SCMFSA_9:33
for a being Int-Location
for I being Program of
for k being Element of NAT st k < 6 holds
(card I) + k in dom (while>0 (a,I))
proofend;

theorem Th34: :: SCMFSA_9:34
for a being Int-Location
for I being Program of holds (while>0 (a,I)) . ((card I) + 5) = halt SCM+FSA
proofend;

theorem Th35: :: SCMFSA_9:35
for a being Int-Location
for I being Program of holds (while>0 (a,I)) . 3 = goto ((card I) + 5)
proofend;

theorem Th36: :: SCMFSA_9:36
for a being Int-Location
for I being Program of holds (while>0 (a,I)) . 2 = goto 3
proofend;

theorem :: SCMFSA_9:37
for a being Int-Location
for I being Program of
for k being Element of NAT st k < (card I) + 6 holds
k in dom (while>0 (a,I))
proofend;

theorem Th38: :: SCMFSA_9:38
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of
for a being read-write Int-Location st s . a <= 0 holds
( while>0 (a,I) is_halting_on s,P &amp; while>0 (a,I) is_closed_on s,P )
proofend;

theorem Th39: :: SCMFSA_9:39
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for I being Program of
for s being State of SCM+FSA
for k being Element of NAT st I is_closed_on s,P &amp; I is_halting_on s,P &amp; k < LifeSpan ((P +* I),(Initialize s)) &amp; IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 4 &amp; DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = DataPart (Comput ((P +* I),(Initialize s),k)) holds
( IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize s),(k + 1)))) + 4 &amp; DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(s +* (Start-At (0,SCM+FSA))),(k + 1))) )
proofend;

theorem Th40: :: SCMFSA_9:40
for P being Instruction-Sequence of SCM+FSA
for a being Int-Location
for I being Program of
for s being State of SCM+FSA st I is_closed_on s,P &amp; I is_halting_on s,P &amp; IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s)))))) = (IC (Comput ((P +* I),(Initialize s),(LifeSpan ((P +* I),(Initialize s)))))) + 4 holds
CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto ((card I) + 4)
proofend;

theorem Th41: :: SCMFSA_9:41
for a being Int-Location
for I being Program of holds (while>0 (a,I)) . ((card I) + 4) = goto 0
proofend;

theorem Th42: :: SCMFSA_9:42
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of
for a being read-write Int-Location st I is_closed_on s,P &amp; I is_halting_on s,P &amp; s . a > 0 holds
( IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 3))) = 0 &amp; ( for k being Element of NAT st k <= (LifeSpan ((P +* I),(Initialize s))) + 3 holds
IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) ) )
proofend;

definition
let s be State of SCM+FSA;
let I be Program of ;
let a be read-write Int-Location;
let P be Instruction-Sequence of SCM+FSA;
deffunc H1( Nat, State of SCM+FSA) ->  set = Comput ((P +* (while>0 (a,I))),($2 +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while>0 (a,I))) +* I),($2 +* (Start-At (0,SCM+FSA))))) + 3));
deffunc H2( Nat, State of SCM+FSA) ->  Element of product (the_Values_of SCM+FSA) = down H1($1,$2);
func StepWhile>0 (a,I,P,s) ->  Function of NAT,(product (the_Values_of SCM+FSA)) means :Def5: :: SCMFSA_9:def 5
( it . 0 = s &amp; ( for i being Nat holds it . (i + 1) = Comput ((P +* (while>0 (a,I))),((it . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while>0 (a,I))) +* I),((it . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) );
existence
 ex b1 being Function of NAT,(product (the_Values_of SCM+FSA)) st
( b1 . 0 = s &amp; ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while>0 (a,I))),((b1 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while>0 (a,I))) +* I),((b1 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) )
proofend;
uniqueness
 for b1, b2 being Function of NAT,(product (the_Values_of SCM+FSA)) st b1 . 0 = s &amp; ( for i being Nat holds b1 . (i + 1) = Comput ((P +* (while>0 (a,I))),((b1 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while>0 (a,I))) +* I),((b1 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) &amp; b2 . 0 = s &amp; ( for i being Nat holds b2 . (i + 1) = Comput ((P +* (while>0 (a,I))),((b2 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while>0 (a,I))) +* I),((b2 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines StepWhile>0 SCMFSA_9:def_5_:_
 for s being State of SCM+FSA
for I being Program of
for a being read-write Int-Location
for P being Instruction-Sequence of SCM+FSA
for b5 being Function of NAT,(product (the_Values_of SCM+FSA)) holds
( b5 = StepWhile>0 (a,I,P,s) iff ( b5 . 0 = s &amp; ( for i being Nat holds b5 . (i + 1) = Comput ((P +* (while>0 (a,I))),((b5 . i) +* (Start-At (0,SCM+FSA))),((LifeSpan (((P +* (while>0 (a,I))) +* I),((b5 . i) +* (Start-At (0,SCM+FSA))))) + 3)) ) ) );

theorem Th43: :: SCMFSA_9:43
for P being Instruction-Sequence of SCM+FSA
for k being Element of NAT
for s being State of SCM+FSA
for I being Program of
for a being read-write Int-Location holds (StepWhile>0 (a,I,P,s)) . (k + 1) = (StepWhile>0 (a,I,P,((StepWhile>0 (a,I,P,s)) . k))) . 1
proofend;

theorem Th44: :: SCMFSA_9:44
for P being Instruction-Sequence of SCM+FSA
for I being Program of
for a being read-write Int-Location
for s being State of SCM+FSA holds (StepWhile>0 (a,I,P,s)) . (0 + 1) = Comput ((P +* (while>0 (a,I))),(Initialize s),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize s))) + 3))
proofend;

theorem Th45: :: SCMFSA_9:45
for P being Instruction-Sequence of SCM+FSA
for I being Program of
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,P,s)) . k) = 0 &amp; (StepWhile>0 (a,I,P,s)) . k = Comput ((P +* (while>0 (a,I))),(Initialize s),n) holds
( (StepWhile>0 (a,I,P,s)) . k = Initialize ((StepWhile>0 (a,I,P,s)) . k) &amp; (StepWhile>0 (a,I,P,s)) . (k + 1) = Comput ((P +* (while>0 (a,I))),(Initialize s),(n + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,P,s)) . k)))) + 3))) )
proofend;

theorem Th46: :: SCMFSA_9:46
for P being Instruction-Sequence of SCM+FSA
for I being Program of
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,P,s)) . k,P +* (while>0 (a,I)) &amp; I is_halting_on (StepWhile>0 (a,I,P,s)) . k,P +* (while>0 (a,I)) ) ) &amp; ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for k being Nat holds
( ( f . ((StepWhile>0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,P,s)) . k) or f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) &amp; ( f . ((StepWhile>0 (a,I,P,s)) . k) = 0 implies ((StepWhile>0 (a,I,P,s)) . k) . a <= 0 ) &amp; ( ((StepWhile>0 (a,I,P,s)) . k) . a <= 0 implies f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) ) holds
( while>0 (a,I) is_halting_on s,P &amp; while>0 (a,I) is_closed_on s,P )
proofend;

theorem Th47: :: SCMFSA_9:47
for P being Instruction-Sequence of SCM+FSA
for I being parahalting Program of
for a being read-write Int-Location
for s being State of SCM+FSA st ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for k being Nat holds
( ( f . ((StepWhile>0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,P,s)) . k) or f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) &amp; ( f . ((StepWhile>0 (a,I,P,s)) . k) = 0 implies ((StepWhile>0 (a,I,P,s)) . k) . a <= 0 ) &amp; ( ((StepWhile>0 (a,I,P,s)) . k) . a <= 0 implies f . ((StepWhile>0 (a,I,P,s)) . k) = 0 ) ) holds
( while>0 (a,I) is_halting_on s,P &amp; while>0 (a,I) is_closed_on s,P )
proofend;

theorem :: SCMFSA_9:48
for I being parahalting Program of
for a being read-write Int-Location st ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( ( f . ((StepWhile>0 (a,I,P,s)) . 1) < f . s or f . s = 0 ) &amp; ( f . s = 0 implies s . a <= 0 ) &amp; ( s . a <= 0 implies f . s = 0 ) ) holds
while>0 (a,I) is parahalting
proofend;

registration
let I, J be good Program of ;
let a be Int-Location;
cluster if>0 (a,I,J) ->  good ;
coherence
 if>0 (a,I,J) is good
proofend;
end;

registration
let I be good Program of ;
let a be Int-Location;
cluster while>0 (a,I) ->  good ;
correctness
coherence
while>0 (a,I) is good ;
proofend;
end;