:: by Jing-Chao Chen

::

:: Received December 10, 1997

:: Copyright (c) 1997-2019 Association of Mizar Users

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

canceled;

canceled;

canceled;

:: WHILE Statement

:: WHILE Statement

:: WHILE Statement

:: WHILE Statement

:: WHILE Statement

:: WHILE Statement

:: WHILE Statement

:: WHILE Statement

:: WHILE Statement

:: WHILE Statement

:: WHILE Statement

:: WHILE Statement

:: WHILE Statement

:: WHILE Statement

:: WHILE Statement

:: WHILE Statement

:: WHILE Statement

::$CD 3

::$CT 17

::$CT 17

theorem Th1: :: SCMFSA_9:18

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <> 0 holds

while=0 (a,I) is_halting_on s,P

for s being State of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <> 0 holds

while=0 (a,I) is_halting_on s,P

proof end;

theorem Th2: :: SCMFSA_9:19

for P being Instruction-Sequence of SCM+FSA

for a being Int-Location

for I being really-closed MacroInstruction of SCM+FSA

for s being State of SCM+FSA

for k being Nat st I is_halting_on s,P & k < LifeSpan ((P +* I),(Initialize s)) & IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 3 & 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)))) + 3 & DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) )

for a being Int-Location

for I being really-closed MacroInstruction of SCM+FSA

for s being State of SCM+FSA

for k being Nat st I is_halting_on s,P & k < LifeSpan ((P +* I),(Initialize s)) & IC (Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 3 & 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)))) + 3 & DataPart (Comput ((P +* (while=0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) )

proof end;

:: Twierdzeinie zmienia znaczenie, jezeli w oryginale mowilo

:: ze znajdziemy sie w miejscu "przed powrotem" i wykonujemy Next

:: to w tym miejscu jest teraz powrot i wykonujemy goto 0

:: ze znajdziemy sie w miejscu "przed powrotem" i wykonujemy Next

:: to w tym miejscu jest teraz powrot i wykonujemy goto 0

theorem Th3: :: SCMFSA_9:20

for P being Instruction-Sequence of SCM+FSA

for a being Int-Location

for I being really-closed MacroInstruction of SCM+FSA

for s being State of SCM+FSA st I is_halting_on s,P & 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)))))) + 3 holds

CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0

for a being Int-Location

for I being really-closed MacroInstruction of SCM+FSA

for s being State of SCM+FSA st I is_halting_on s,P & 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)))))) + 3 holds

CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0

proof end;

::$CT

theorem Th4: :: SCMFSA_9:22

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st I is_halting_on s,P & s . a = 0 holds

( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) )

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st I is_halting_on s,P & s . a = 0 holds

( IC (Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while=0 (a,I))),(Initialize s),k)) in dom (while=0 (a,I)) ) )

proof end;

definition

let s be State of SCM+FSA;

let I be MacroInstruction of SCM+FSA ;

let a be read-write Int-Location;

let P be Instruction-Sequence of SCM+FSA;

deffunc H_{1}( Nat, State of SCM+FSA) -> set = Comput ((P +* (while=0 (a,I))),(Initialize $2),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize $2))) + 2));

deffunc H_{2}( Nat, State of SCM+FSA) -> Element of product (the_Values_of SCM+FSA) = down H_{1}($1,$2);

ex b_{1} being sequence of (product (the_Values_of SCM+FSA)) st

( b_{1} . 0 = s & ( for i being Nat holds b_{1} . (i + 1) = Comput ((P +* (while=0 (a,I))),(Initialize (b_{1} . i)),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize (b_{1} . i)))) + 2)) ) )

for b_{1}, b_{2} being sequence of (product (the_Values_of SCM+FSA)) st b_{1} . 0 = s & ( for i being Nat holds b_{1} . (i + 1) = Comput ((P +* (while=0 (a,I))),(Initialize (b_{1} . i)),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize (b_{1} . i)))) + 2)) ) & b_{2} . 0 = s & ( for i being Nat holds b_{2} . (i + 1) = Comput ((P +* (while=0 (a,I))),(Initialize (b_{2} . i)),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize (b_{2} . i)))) + 2)) ) holds

b_{1} = b_{2}

end;
let I be MacroInstruction of SCM+FSA ;

let a be read-write Int-Location;

let P be Instruction-Sequence of SCM+FSA;

deffunc H

deffunc H

func StepWhile=0 (a,I,P,s) -> sequence of (product (the_Values_of SCM+FSA)) means :Def1: :: SCMFSA_9:def 1

( it . 0 = s & ( for i being Nat holds it . (i + 1) = Comput ((P +* (while=0 (a,I))),(Initialize (it . i)),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize (it . i)))) + 2)) ) );

existence ( it . 0 = s & ( for i being Nat holds it . (i + 1) = Comput ((P +* (while=0 (a,I))),(Initialize (it . i)),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize (it . i)))) + 2)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines StepWhile=0 SCMFSA_9:def 1 :

for s being State of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location

for P being Instruction-Sequence of SCM+FSA

for b_{5} being sequence of (product (the_Values_of SCM+FSA)) holds

( b_{5} = StepWhile=0 (a,I,P,s) iff ( b_{5} . 0 = s & ( for i being Nat holds b_{5} . (i + 1) = Comput ((P +* (while=0 (a,I))),(Initialize (b_{5} . i)),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize (b_{5} . i)))) + 2)) ) ) );

for s being State of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location

for P being Instruction-Sequence of SCM+FSA

for b

( b

theorem Th5: :: SCMFSA_9:23

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location

for k being Nat holds (StepWhile=0 (a,I,P,s)) . (k + 1) = (StepWhile=0 (a,I,P,((StepWhile=0 (a,I,P,s)) . k))) . 1

for s being State of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location

for k being Nat holds (StepWhile=0 (a,I,P,s)) . (k + 1) = (StepWhile=0 (a,I,P,((StepWhile=0 (a,I,P,s)) . k))) . 1

proof end;

::$CT

theorem Th6: :: SCMFSA_9:25

for P being Instruction-Sequence of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA holds (StepWhile=0 (a,I,P,s)) . 1 = Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize s))) + 2))

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA holds (StepWhile=0 (a,I,P,s)) . 1 = Comput ((P +* (while=0 (a,I))),(Initialize s),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize s))) + 2))

proof end;

theorem Th7: :: SCMFSA_9:26

for P being Instruction-Sequence of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA

for k, n being Nat st IC ((StepWhile=0 (a,I,P,s)) . k) = 0 & (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) & (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)))) + 2))) )

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA

for k, n being Nat st IC ((StepWhile=0 (a,I,P,s)) . k) = 0 & (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) & (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)))) + 2))) )

proof end;

theorem Th8: :: SCMFSA_9:27

for P being Instruction-Sequence of SCM+FSA

for I being really-closed MacroInstruction 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_halting_on (StepWhile=0 (a,I,P,s)) . k,P +* (while=0 (a,I)) ) & 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 ) & ( f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) & ( ((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

for I being really-closed MacroInstruction 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_halting_on (StepWhile=0 (a,I,P,s)) . k,P +* (while=0 (a,I)) ) & 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 ) & ( f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) & ( ((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

proof end;

theorem Th9: :: SCMFSA_9:28

for P being Instruction-Sequence of SCM+FSA

for I being really-closed parahalting MacroInstruction 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_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 ) & ( f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) & ( ((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

for I being really-closed parahalting MacroInstruction 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_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 ) & ( f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) & ( ((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

proof end;

theorem :: SCMFSA_9:29

for I being really-closed parahalting MacroInstruction of SCM+FSA

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 ) & ( f . s = 0 implies s . a <> 0 ) & ( s . a <> 0 implies f . s = 0 ) ) holds

while=0 (a,I) is parahalting

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 ) & ( f . s = 0 implies s . a <> 0 ) & ( s . a <> 0 implies f . s = 0 ) ) holds

while=0 (a,I) is parahalting

proof end;

::$CT

registration

let I, J be good MacroInstruction of SCM+FSA ;

let a be Int-Location;

correctness

coherence

if=0 (a,I,J) is good ;

end;
let a be Int-Location;

correctness

coherence

if=0 (a,I,J) is good ;

proof end;

registration

let I be good MacroInstruction of SCM+FSA ;

let a be Int-Location;

correctness

coherence

if=0 (a,I) is good ;

end;
let a be Int-Location;

correctness

coherence

if=0 (a,I) is good ;

proof end;

registration

let I be good MacroInstruction of SCM+FSA ;

let a be Int-Location;

correctness

coherence

while=0 (a,I) is good ;

end;
let a be Int-Location;

correctness

coherence

while=0 (a,I) is good ;

proof end;

:: -----------------------------------------------------------

:: WHILE>0 Statement

::$CT 6

:: WHILE>0 Statement

::$CT 6

theorem Th12: :: SCMFSA_9:38

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <= 0 holds

while>0 (a,I) is_halting_on s,P

for s being State of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <= 0 holds

while>0 (a,I) is_halting_on s,P

proof end;

theorem Th13: :: SCMFSA_9:39

for P being Instruction-Sequence of SCM+FSA

for a being Int-Location

for I being really-closed MacroInstruction of SCM+FSA

for s being State of SCM+FSA

for k being Nat st I is_halting_on s,P & k < LifeSpan ((P +* I),(Initialize s)) & IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 3 & 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)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) )

for a being Int-Location

for I being really-closed MacroInstruction of SCM+FSA

for s being State of SCM+FSA

for k being Nat st I is_halting_on s,P & k < LifeSpan ((P +* I),(Initialize s)) & IC (Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + k))) = (IC (Comput ((P +* I),(Initialize s),k))) + 3 & 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)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize s),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize s),(k + 1))) )

proof end;

theorem Th14: :: SCMFSA_9:40

for P being Instruction-Sequence of SCM+FSA

for a being Int-Location

for I being really-closed MacroInstruction of SCM+FSA

for s being State of SCM+FSA st I is_halting_on s,P & 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)))))) + 3 holds

CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0

for a being Int-Location

for I being really-closed MacroInstruction of SCM+FSA

for s being State of SCM+FSA st I is_halting_on s,P & 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)))))) + 3 holds

CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize s),(1 + (LifeSpan ((P +* I),(Initialize s))))))) = goto 0

proof end;

::$CT

theorem Th15: :: SCMFSA_9:42

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st I is_halting_on s,P & s . a > 0 holds

( IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) ) )

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st I is_halting_on s,P & s . a > 0 holds

( IC (Comput ((P +* (while>0 (a,I))),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),(Initialize s))) + 2 holds

IC (Comput ((P +* (while>0 (a,I))),(Initialize s),k)) in dom (while>0 (a,I)) ) )

proof end;

definition

let s be State of SCM+FSA;

let I be MacroInstruction of SCM+FSA ;

let a be read-write Int-Location;

let P be Instruction-Sequence of SCM+FSA;

deffunc H_{1}( Nat, State of SCM+FSA) -> set = Comput ((P +* (while>0 (a,I))),(Initialize $2),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize $2))) + 2));

deffunc H_{2}( Nat, State of SCM+FSA) -> Element of product (the_Values_of SCM+FSA) = down H_{1}($1,$2);

ex b_{1} being sequence of (product (the_Values_of SCM+FSA)) st

( b_{1} . 0 = s & ( for i being Nat holds b_{1} . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialize (b_{1} . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize (b_{1} . i)))) + 2)) ) )

for b_{1}, b_{2} being sequence of (product (the_Values_of SCM+FSA)) st b_{1} . 0 = s & ( for i being Nat holds b_{1} . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialize (b_{1} . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize (b_{1} . i)))) + 2)) ) & b_{2} . 0 = s & ( for i being Nat holds b_{2} . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialize (b_{2} . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize (b_{2} . i)))) + 2)) ) holds

b_{1} = b_{2}

end;
let I be MacroInstruction of SCM+FSA ;

let a be read-write Int-Location;

let P be Instruction-Sequence of SCM+FSA;

deffunc H

deffunc H

func StepWhile>0 (a,I,P,s) -> sequence of (product (the_Values_of SCM+FSA)) means :Def2: :: SCMFSA_9:def 2

( it . 0 = s & ( for i being Nat holds it . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialize (it . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize (it . i)))) + 2)) ) );

existence ( it . 0 = s & ( for i being Nat holds it . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialize (it . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize (it . i)))) + 2)) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines StepWhile>0 SCMFSA_9:def 2 :

for s being State of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location

for P being Instruction-Sequence of SCM+FSA

for b_{5} being sequence of (product (the_Values_of SCM+FSA)) holds

( b_{5} = StepWhile>0 (a,I,P,s) iff ( b_{5} . 0 = s & ( for i being Nat holds b_{5} . (i + 1) = Comput ((P +* (while>0 (a,I))),(Initialize (b_{5} . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize (b_{5} . i)))) + 2)) ) ) );

for s being State of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location

for P being Instruction-Sequence of SCM+FSA

for b

( b

theorem Th16: :: SCMFSA_9:43

for P being Instruction-Sequence of SCM+FSA

for k being Nat

for s being State of SCM+FSA

for I being MacroInstruction of SCM+FSA

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

for k being Nat

for s being State of SCM+FSA

for I being MacroInstruction of SCM+FSA

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

proof end;

theorem Th17: :: SCMFSA_9:44

for P being Instruction-Sequence of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA holds (StepWhile>0 (a,I,P,s)) . 1 = Comput ((P +* (while>0 (a,I))),(Initialize s),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize s))) + 2))

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA holds (StepWhile>0 (a,I,P,s)) . 1 = Comput ((P +* (while>0 (a,I))),(Initialize s),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialize s))) + 2))

proof end;

theorem Th18: :: SCMFSA_9:45

for P being Instruction-Sequence of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA

for k, n being Nat st IC ((StepWhile>0 (a,I,P,s)) . k) = 0 & (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) & (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)))) + 2))) )

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA

for k, n being Nat st IC ((StepWhile>0 (a,I,P,s)) . k) = 0 & (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) & (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)))) + 2))) )

proof end;

theorem Th19: :: SCMFSA_9:46

for P being Instruction-Sequence of SCM+FSA

for I being really-closed MacroInstruction 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_halting_on (StepWhile>0 (a,I,P,s)) . k,P +* (while>0 (a,I)) ) & 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 ) & ( f . ((StepWhile>0 (a,I,P,s)) . k) = 0 implies ((StepWhile>0 (a,I,P,s)) . k) . a <= 0 ) & ( ((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

for I being really-closed MacroInstruction 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_halting_on (StepWhile>0 (a,I,P,s)) . k,P +* (while>0 (a,I)) ) & 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 ) & ( f . ((StepWhile>0 (a,I,P,s)) . k) = 0 implies ((StepWhile>0 (a,I,P,s)) . k) . a <= 0 ) & ( ((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

proof end;

theorem Th20: :: SCMFSA_9:47

for P being Instruction-Sequence of SCM+FSA

for I being really-closed parahalting MacroInstruction 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_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 ) & ( f . ((StepWhile>0 (a,I,P,s)) . k) = 0 implies ((StepWhile>0 (a,I,P,s)) . k) . a <= 0 ) & ( ((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

for I being really-closed parahalting MacroInstruction 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_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 ) & ( f . ((StepWhile>0 (a,I,P,s)) . k) = 0 implies ((StepWhile>0 (a,I,P,s)) . k) . a <= 0 ) & ( ((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

proof end;

theorem :: SCMFSA_9:48

for I being really-closed parahalting MacroInstruction of SCM+FSA

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 ) & ( f . s = 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s = 0 ) ) holds

while>0 (a,I) is parahalting

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 ) & ( 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 MacroInstruction of SCM+FSA ;

let a be Int-Location;

coherence

if>0 (a,I,J) is good

end;
let a be Int-Location;

coherence

if>0 (a,I,J) is good

proof end;

registration

let I be good MacroInstruction of SCM+FSA ;

let a be Int-Location;

correctness

coherence

if>0 (a,I) is good ;

end;
let a be Int-Location;

correctness

coherence

if>0 (a,I) is good ;

proof end;

registration

let I be good MacroInstruction of SCM+FSA ;

let a be Int-Location;

correctness

coherence

while>0 (a,I) is good ;

end;
let a be Int-Location;

correctness

coherence

while>0 (a,I) is good ;

proof end;

theorem :: SCMFSA_9:49

for p being preProgram of SCM+FSA

for l being Nat

for ic being Instruction of SCM+FSA st ex pc being Instruction of SCM+FSA st

( pc = p . l & UsedIntLoc pc = UsedIntLoc ic ) holds

UsedILoc p = UsedILoc (p +* (l,ic))

for l being Nat

for ic being Instruction of SCM+FSA st ex pc being Instruction of SCM+FSA st

( pc = p . l & UsedIntLoc pc = UsedIntLoc ic ) holds

UsedILoc p = UsedILoc (p +* (l,ic))

proof end;

theorem :: SCMFSA_9:50

for p being preProgram of SCM+FSA

for l being Nat

for ic being Instruction of SCM+FSA st ex pc being Instruction of SCM+FSA st

( pc = p . l & UsedInt*Loc pc = UsedInt*Loc ic ) holds

UsedI*Loc p = UsedI*Loc (p +* (l,ic))

for l being Nat

for ic being Instruction of SCM+FSA st ex pc being Instruction of SCM+FSA st

( pc = p . l & UsedInt*Loc pc = UsedInt*Loc ic ) holds

UsedI*Loc p = UsedI*Loc (p +* (l,ic))

proof end;