:: The { \bf while } macro instructions of SCM+FSA, Part { II }
:: by Piotr Rudnicki
::
:: Received June 3, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users


theorem Th1: :: SCMFSA9A:1
for l being Nat
for i being Instruction of SCM+FSA holds UsedILoc (l .--> i) = UsedIntLoc i
proof end;

theorem Th2: :: SCMFSA9A:2
for l being Nat
for i being Instruction of SCM+FSA holds UsedI*Loc (l .--> i) = UsedInt*Loc i
proof end;

theorem Th3: :: SCMFSA9A:3
UsedILoc (Stop SCM+FSA) = {} by Th1, SF_MASTR:13;

theorem Th4: :: SCMFSA9A:4
UsedI*Loc (Stop SCM+FSA) = {}
proof end;

theorem Th5: :: SCMFSA9A:5
for l being Nat holds UsedILoc (Goto l) = {}
proof end;

theorem Th6: :: SCMFSA9A:6
for l being Nat holds UsedI*Loc (Goto l) = {}
proof end;

set D = Int-Locations \/ FinSeq-Locations;

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

theorem :: SCMFSA9A:7
for b being Int-Location
for I, J being MacroInstruction of SCM+FSA holds UsedILoc (if=0 (b,I,J)) = ({b} \/ (UsedILoc I)) \/ (UsedILoc J)
proof end;

theorem :: SCMFSA9A:8
for I, J being MacroInstruction of SCM+FSA
for a being Int-Location holds UsedI*Loc (if=0 (a,I,J)) = (UsedI*Loc I) \/ (UsedI*Loc J)
proof end;

theorem :: SCMFSA9A:9
for b being Int-Location
for I, J being MacroInstruction of SCM+FSA holds UsedILoc (if>0 (b,I,J)) = ({b} \/ (UsedILoc I)) \/ (UsedILoc J)
proof end;

theorem :: SCMFSA9A:10
for b being Int-Location
for I, J being MacroInstruction of SCM+FSA holds UsedI*Loc (if>0 (b,I,J)) = (UsedI*Loc I) \/ (UsedI*Loc J)
proof end;

Lm1: for a being Int-Location
for I being MacroInstruction of SCM+FSA holds (if=0 (a,(I ';' (goto 0)))) . ((card (I ';' (goto 0))) + 1) = goto ((card (I ';' (goto 0))) + 1)
proof end;

Lm2: for a being Int-Location
for I being MacroInstruction of SCM+FSA holds (if>0 (a,(I ';' (goto 0)))) . ((card (I ';' (goto 0))) + 1) = goto ((card (I ';' (goto 0))) + 1)
proof end;

Lm3: for a being Int-Location
for I being MacroInstruction of SCM+FSA holds UsedILoc (if=0 (a,(I ';' (goto 0)))) = UsedILoc ((if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)))
proof end;

Lm4: for a being Int-Location
for I being MacroInstruction of SCM+FSA holds UsedI*Loc (if=0 (a,(I ';' (goto 0)))) = UsedI*Loc ((if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)))
proof end;

theorem :: SCMFSA9A:11
for b being Int-Location
for I being MacroInstruction of SCM+FSA holds UsedILoc (while=0 (b,I)) = {b} \/ (UsedILoc I)
proof end;

theorem :: SCMFSA9A:12
for b being Int-Location
for I being MacroInstruction of SCM+FSA holds UsedI*Loc (while=0 (b,I)) = UsedI*Loc I
proof end;

definition
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
let a be read-write Int-Location;
let I be MacroInstruction of SCM+FSA ;
pred ProperBodyWhile=0 a,I,s,p means :: SCMFSA9A:def 1
 for k being Nat st ((StepWhile=0 (a,I,p,s)) . k) . a = 0 holds
I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I));
pred WithVariantWhile=0 a,I,s,p means :: SCMFSA9A:def 2
 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 ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 );
end;

:: deftheorem defines ProperBodyWhile=0 SCMFSA9A:def 1 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA holds
( ProperBodyWhile=0 a,I,s,p iff for k being Nat st ((StepWhile=0 (a,I,p,s)) . k) . a = 0 holds
I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) );

:: deftheorem defines WithVariantWhile=0 SCMFSA9A:def 2 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA holds
( WithVariantWhile=0 a,I,s,p iff 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 ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 ) );

theorem Th13: :: SCMFSA9A:13
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being parahalting MacroInstruction of SCM+FSA holds ProperBodyWhile=0 a,I,s,p by SCMFSA7B:19;

theorem Th14: :: SCMFSA9A:14
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile=0 a,I,s,p & WithVariantWhile=0 a,I,s,p holds
while=0 (a,I) is_halting_on s,p
proof end;

theorem Th15: :: SCMFSA9A:15
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed parahalting MacroInstruction of SCM+FSA st WithVariantWhile=0 a,I,s,p holds
while=0 (a,I) is_halting_on s,p
proof end;

theorem Th16: :: SCMFSA9A:16
for p being Instruction-Sequence of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA
for s being 0 -started State of SCM+FSA st while=0 (a,I) c= p & s . a <> 0 holds
( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) )
proof end;

theorem Th17: :: SCMFSA9A:17
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st I is_halting_on s,p & s . a = 0 holds
DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),((LifeSpan ((p +* I),(Initialize s))) + 2))) = DataPart (Comput ((p +* I),(Initialize s),(LifeSpan ((p +* I),(Initialize s)))))
proof end;

theorem Th18: :: SCMFSA9A:18
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA
for k being Nat st ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 holds
DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile=0 (a,I,p,s)) . k)
proof end;

theorem Th19: :: SCMFSA9A:19
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for k being Nat
for I being really-closed MacroInstruction of SCM+FSA st ( I is_halting_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I)) or I is parahalting ) & ((StepWhile=0 (a,I,p,s)) . k) . a = 0 & ((StepWhile=0 (a,I,p,s)) . k) . (intloc 0) = 1 holds
DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart (IExec (I,(p +* (while=0 (a,I))),((StepWhile=0 (a,I,p,s)) . k)))
proof end;

theorem :: SCMFSA9A:20
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for Ig being good really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile=0 a,Ig,s,p or Ig is parahalting ) & s . (intloc 0) = 1 holds
for k being Nat holds ((StepWhile=0 (a,Ig,p,s)) . k) . (intloc 0) = 1
proof end;

theorem :: SCMFSA9A:21
for p1, p2 being Instruction-Sequence of SCM+FSA
for s1, s2 being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile=0 a,I,s1,p1 & DataPart s1 = DataPart s2 holds
for k being Nat holds DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart ((StepWhile=0 (a,I,p2,s2)) . k)
proof end;

definition
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
let a be read-write Int-Location;
let I be really-closed MacroInstruction of SCM+FSA ;
assume that
A1: ( ProperBodyWhile=0 a,I,s,p or I is parahalting ) and
A2: WithVariantWhile=0 a,I,s,p ;
func ExitsAtWhile=0 (a,I,p,s) -> Nat means :Def3: :: SCMFSA9A:def 3
 ex k being Nat st
( it = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) );
existence
ex b1, k being Nat st
( b1 = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) )
proof end;
uniqueness
for b1, b2 being Nat st ex k being Nat st
( b1 = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) & ex k being Nat st
( b2 = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines ExitsAtWhile=0 SCMFSA9A:def 3 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile=0 a,I,s,p or I is parahalting ) & WithVariantWhile=0 a,I,s,p holds
for b5 being Nat holds
( b5 = ExitsAtWhile=0 (a,I,p,s) iff ex k being Nat st
( b5 = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) );

theorem :: SCMFSA9A:22
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & s . a <> 0 holds
DataPart (IExec ((while=0 (a,I)),p,s)) = DataPart s
proof end;

theorem :: SCMFSA9A:23
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile=0 a,I, Initialized s,p or I is parahalting ) & WithVariantWhile=0 a,I, Initialized s,p holds
DataPart (IExec ((while=0 (a,I)),p,s)) = DataPart ((StepWhile=0 (a,I,p,(Initialized s))) . (ExitsAtWhile=0 (a,I,p,(Initialized s))))
proof end;

Lm5: for a being Int-Location
for I being MacroInstruction of SCM+FSA holds UsedILoc (if>0 (a,(I ';' (goto 0)))) = UsedILoc ((if>0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)))
proof end;

Lm6: for a being Int-Location
for I being MacroInstruction of SCM+FSA holds UsedI*Loc (if>0 (a,(I ';' (goto 0)))) = UsedI*Loc ((if>0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)))
proof end;

theorem Th24: :: SCMFSA9A:24
for b being Int-Location
for I being MacroInstruction of SCM+FSA holds UsedILoc (while>0 (b,I)) = {b} \/ (UsedILoc I)
proof end;

theorem Th25: :: SCMFSA9A:25
for b being Int-Location
for I being MacroInstruction of SCM+FSA holds UsedI*Loc (while>0 (b,I)) = UsedI*Loc I
proof end;

definition
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
let a be read-write Int-Location;
let I be MacroInstruction of SCM+FSA ;
pred ProperBodyWhile>0 a,I,s,p means :: SCMFSA9A:def 4
 for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a > 0 holds
I is_halting_on (StepWhile>0 (a,I,p,s)) . k,p +* (while>0 (a,I));
pred WithVariantWhile>0 a,I,s,p means :: SCMFSA9A:def 5
 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 ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 );
end;

:: deftheorem defines ProperBodyWhile>0 SCMFSA9A:def 4 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA holds
( ProperBodyWhile>0 a,I,s,p iff for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a > 0 holds
I is_halting_on (StepWhile>0 (a,I,p,s)) . k,p +* (while>0 (a,I)) );

:: deftheorem defines WithVariantWhile>0 SCMFSA9A:def 5 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA holds
( WithVariantWhile>0 a,I,s,p iff 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 ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 ) );

theorem Th26: :: SCMFSA9A:26
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being parahalting MacroInstruction of SCM+FSA holds ProperBodyWhile>0 a,I,s,p by SCMFSA7B:19;

theorem Th27: :: SCMFSA9A:27
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile>0 a,I,s,p & WithVariantWhile>0 a,I,s,p holds
while>0 (a,I) is_halting_on s,p
proof end;

theorem Th28: :: SCMFSA9A:28
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed parahalting MacroInstruction of SCM+FSA st WithVariantWhile>0 a,I,s,p holds
while>0 (a,I) is_halting_on s,p
proof end;

theorem Th29: :: SCMFSA9A:29
for p being Instruction-Sequence of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA
for s being 0 -started State of SCM+FSA st while>0 (a,I) c= p & s . a <= 0 holds
( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) )
proof end;

theorem Th30: :: SCMFSA9A:30
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st I is_halting_on s,p & s . a > 0 holds
DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),((LifeSpan ((p +* I),(Initialize s))) + 2))) = DataPart (Comput ((p +* I),(Initialize s),(LifeSpan ((p +* I),(Initialize s)))))
proof end;

theorem Th31: :: SCMFSA9A:31
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA
for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 holds
DataPart ((StepWhile>0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile>0 (a,I,p,s)) . k)
proof end;

theorem Th32: :: SCMFSA9A:32
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for k being Nat
for I being really-closed MacroInstruction of SCM+FSA st ( I is_halting_on Initialized ((StepWhile>0 (a,I,p,s)) . k),p +* (while>0 (a,I)) or I is parahalting ) & ((StepWhile>0 (a,I,p,s)) . k) . a > 0 & ((StepWhile>0 (a,I,p,s)) . k) . (intloc 0) = 1 holds
DataPart ((StepWhile>0 (a,I,p,s)) . (k + 1)) = DataPart (IExec (I,(p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . k)))
proof end;

theorem Th33: :: SCMFSA9A:33
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for Ig being good really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile>0 a,Ig,s,p or Ig is parahalting ) & s . (intloc 0) = 1 holds
for k being Nat holds ((StepWhile>0 (a,Ig,p,s)) . k) . (intloc 0) = 1
proof end;

theorem Th34: :: SCMFSA9A:34
for p1, p2 being Instruction-Sequence of SCM+FSA
for s1, s2 being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile>0 a,I,s1,p1 & DataPart s1 = DataPart s2 holds
for k being Nat holds DataPart ((StepWhile>0 (a,I,p1,s1)) . k) = DataPart ((StepWhile>0 (a,I,p2,s2)) . k)
proof end;

definition
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
let a be read-write Int-Location;
let I be really-closed MacroInstruction of SCM+FSA ;
assume that
A1: ( ProperBodyWhile>0 a,I,s,p or I is parahalting ) and
A2: WithVariantWhile>0 a,I,s,p ;
func ExitsAtWhile>0 (a,I,p,s) -> Nat means :Def6: :: SCMFSA9A:def 6
 ex k being Nat st
( it = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Nat st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) );
existence
ex b1, k being Nat st
( b1 = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Nat st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) )
proof end;
uniqueness
for b1, b2 being Nat st ex k being Nat st
( b1 = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Nat st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ) & ex k being Nat st
( b2 = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Nat st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines ExitsAtWhile>0 SCMFSA9A:def 6 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile>0 a,I,s,p or I is parahalting ) & WithVariantWhile>0 a,I,s,p holds
for b5 being Nat holds
( b5 = ExitsAtWhile>0 (a,I,p,s) iff ex k being Nat st
( b5 = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Nat st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ) );

theorem Th35: :: SCMFSA9A:35
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & s . a <= 0 holds
DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart s
proof end;

theorem Th36: :: SCMFSA9A:36
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile>0 a,I, Initialized s,p or I is parahalting ) & WithVariantWhile>0 a,I, Initialized s,p holds
DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart ((StepWhile>0 (a,I,p,(Initialized s))) . (ExitsAtWhile>0 (a,I,p,(Initialized s))))
proof end;

theorem Th37: :: SCMFSA9A:37
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA
for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 holds
for n being Nat st k <= n holds
DataPart ((StepWhile>0 (a,I,p,s)) . n) = DataPart ((StepWhile>0 (a,I,p,s)) . k)
proof end;

theorem :: SCMFSA9A:38
for p1, p2 being Instruction-Sequence of SCM+FSA
for s1, s2 being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,I,s1,p1 holds
ProperBodyWhile>0 a,I,s2,p2
proof end;

Lm7: for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed Program of st s . (intloc 0) = 1 holds
( I is_halting_on s,p iff I is_halting_on Initialized s,p )
proof end;

theorem Th39: :: SCMFSA9A:39
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for Ig being good really-closed MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperBodyWhile>0 a,Ig,s,p & WithVariantWhile>0 a,Ig,s,p holds
for i, j being Nat st i <> j & i <= ExitsAtWhile>0 (a,Ig,p,s) & j <= ExitsAtWhile>0 (a,Ig,p,s) holds
( (StepWhile>0 (a,Ig,p,s)) . i <> (StepWhile>0 (a,Ig,p,s)) . j & DataPart ((StepWhile>0 (a,Ig,p,s)) . i) <> DataPart ((StepWhile>0 (a,Ig,p,s)) . j) )
proof end;

canceled;

::$CD
theorem Th40: :: SCMFSA9A:40
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for Ig being good really-closed MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperBodyWhile>0 a,Ig,s,p & WithVariantWhile>0 a,Ig,s,p holds
ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
( f is on_data_only & ( for k being Nat holds
( f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p,s)) . k) or ((StepWhile>0 (a,Ig,p,s)) . k) . a <= 0 ) ) )
proof end;

theorem :: SCMFSA9A:41
for p1, p2 being Instruction-Sequence of SCM+FSA
for s1, s2 being State of SCM+FSA
for a being read-write Int-Location
for Ig being good really-closed MacroInstruction of SCM+FSA st s1 . (intloc 0) = 1 & DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,Ig,s1,p1 & WithVariantWhile>0 a,Ig,s1,p1 holds
WithVariantWhile>0 a,Ig,s2,p2
proof end;

definition
let N, result be Int-Location;
func Fusc_macro (N,result) -> MacroInstruction of SCM+FSA equals :: SCMFSA9A:def 7
(((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)) ";" (while>0 ((2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ";" (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))) ";" (if=0 ((3 -rdRWNotIn {N,result}),(Macro (AddTo ((1 -stRWNotIn {N,result}),result))),(Macro (AddTo (result,(1 -stRWNotIn {N,result})))))))));
correctness
coherence
(((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)) ";" (while>0 ((2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ";" (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))) ";" (if=0 ((3 -rdRWNotIn {N,result}),(Macro (AddTo ((1 -stRWNotIn {N,result}),result))),(Macro (AddTo (result,(1 -stRWNotIn {N,result}))))))))) is MacroInstruction of SCM+FSA ;
;
end;

:: deftheorem defines Fusc_macro SCMFSA9A:def 7 :
for N, result being Int-Location holds Fusc_macro (N,result) = (((SubFrom (result,result)) ";" ((1 -stRWNotIn {N,result}) := (intloc 0))) ";" ((2 -ndRWNotIn {N,result}) := N)) ";" (while>0 ((2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ";" (Divide ((2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result})))) ";" (if=0 ((3 -rdRWNotIn {N,result}),(Macro (AddTo ((1 -stRWNotIn {N,result}),result))),(Macro (AddTo (result,(1 -stRWNotIn {N,result})))))))));

:: set next = 1-stRWNotIn {N, result};
:: set aux = 2-ndRWNotIn {N, result};
:: set rem2 = 3-rdRWNotIn {N, result};
:: while and if do not allocate memory, no need to save anything
registration
let N, R be read-write Int-Location;
cluster Fusc_macro (N,R) -> really-closed ;
coherence
Fusc_macro (N,R) is really-closed ;
end;

theorem :: SCMFSA9A:42
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for N, result being read-write Int-Location st N <> result holds
for n being Element of NAT st n = s . N holds
( (IExec ((Fusc_macro (N,result)),p,s)) . result = Fusc n & (IExec ((Fusc_macro (N,result)),p,s)) . N = n )
proof end;

theorem :: SCMFSA9A:43
for I, J being MacroInstruction of SCM+FSA
for a being Int-Location holds
( UsedILoc (if=0 (a,I,J)) = ({a} \/ (UsedILoc I)) \/ (UsedILoc J) & UsedILoc (if>0 (a,I,J)) = ({a} \/ (UsedILoc I)) \/ (UsedILoc J) )
proof end;

theorem :: SCMFSA9A:44
for b being Int-Location
for I being MacroInstruction of SCM+FSA holds UsedILoc (Times (b,I)) = {b,(intloc 0)} \/ (UsedILoc I)
proof end;

theorem :: SCMFSA9A:45
for b being Int-Location
for I being MacroInstruction of SCM+FSA holds UsedI*Loc (Times (b,I)) = UsedI*Loc I
proof end;

set D = Data-Locations ;

:: registration
:: let I be good Program of SCM+FSA, a be Int-Location;
:: cluster Times(a, I) -> good;
:: coherence;
:: end;
definition
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
let I be MacroInstruction of SCM+FSA ;
let a be read-write Int-Location;
func StepTimes (a,I,p,s) -> sequence of (product (the_Values_of SCM+FSA)) equals :: SCMFSA9A:def 8
 StepWhile>0 (a,(I ";" (SubFrom (a,(intloc 0)))),p,(Initialized s));
correctness
coherence
StepWhile>0 (a,(I ";" (SubFrom (a,(intloc 0)))),p,(Initialized s)) is sequence of (product (the_Values_of SCM+FSA));
;
end;

:: deftheorem defines StepTimes SCMFSA9A:def 8 :
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 holds StepTimes (a,I,p,s) = StepWhile>0 (a,(I ";" (SubFrom (a,(intloc 0)))),p,(Initialized s));

theorem :: SCMFSA9A:46
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for J being good MacroInstruction of SCM+FSA
for a being read-write Int-Location holds ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1
proof end;

theorem :: SCMFSA9A:47
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for J being good MacroInstruction of SCM+FSA
for a being read-write Int-Location holds ((StepTimes (a,J,p,s)) . 0) . a = s . a
proof end;

registration
let I be really-closed MacroInstruction of SCM+FSA ;
let a be Int-Location;
cluster Times (a,I) -> really-closed ;
coherence
Times (a,I) is really-closed ;
end;

theorem Th48: :: SCMFSA9A:48
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for k being Nat
for a being read-write Int-Location
for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (Times (a,J)) holds
( ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 & ( ((StepTimes (a,J,p,s)) . k) . a > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) . a = (((StepTimes (a,J,p,s)) . k) . a) - 1 ) )
proof end;

theorem :: SCMFSA9A:49
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for f being FinSeq-Location
for I being MacroInstruction of SCM+FSA
for a being read-write Int-Location holds ((StepTimes (a,I,p,s)) . 0) . f = s . f
proof end;

definition
let p be Instruction-Sequence of SCM+FSA;
let s be State of SCM+FSA;
let a be read-write Int-Location;
let I be MacroInstruction of SCM+FSA ;
pred ProperTimesBody a,I,s,p means :: SCMFSA9A:def 9
 for k being Nat st k < s . a holds
I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (Times (a,I));
end;

:: deftheorem defines ProperTimesBody SCMFSA9A:def 9 :
for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA holds
( ProperTimesBody a,I,s,p iff for k being Nat st k < s . a holds
I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (Times (a,I)) );

theorem Th50: :: SCMFSA9A:50
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for I being MacroInstruction of SCM+FSA
for a being read-write Int-Location st I is parahalting holds
ProperTimesBody a,I,s,p by SCMFSA7B:19;

theorem Th51: :: SCMFSA9A:51
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being read-write Int-Location
for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & ProperTimesBody a,J,s,p holds
for k being Nat st k <= s . a holds
((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1
proof end;

theorem Th52: :: SCMFSA9A:52
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being read-write Int-Location
for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & ProperTimesBody a,J,s,p holds
for k being Nat st k <= s . a holds
(((StepTimes (a,J,p,s)) . k) . a) + k = s . a
proof end;

theorem Th53: :: SCMFSA9A:53
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being read-write Int-Location
for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & ProperTimesBody a,J,s,p & 0 <= s . a holds
for k being Nat st k >= s . a holds
( ((StepTimes (a,J,p,s)) . k) . a = 0 & ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 )
proof end;

theorem :: SCMFSA9A:54
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for k being Nat
for a being read-write Int-Location
for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
DataPart (IExec ((Times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)
proof end;

theorem Th55: :: SCMFSA9A:55
for s being State of SCM+FSA
for p being Instruction-Sequence of SCM+FSA
for a being read-write Int-Location
for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
Times (a,J) is_halting_on s,p
proof end;

theorem Th56: :: SCMFSA9A:56
for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being good really-closed parahalting MacroInstruction of SCM+FSA
for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 holds
Times (a,I) is_halting_on s,P by Th55;

theorem :: SCMFSA9A:57
for I being good really-closed parahalting MacroInstruction of SCM+FSA
for a being read-write Int-Location st not I destroys a holds
Initialize ((intloc 0) .--> 1) is Times (a,I) -halted
proof end;

theorem :: SCMFSA9A:58
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 . (intloc 0) = 1 & s . a <= 0 holds
DataPart (IExec ((Times (a,I)),P,s)) = DataPart s by Th35;