:: 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 b₁, k being Nat st
( b₁ = 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 b₁, b₂ being Nat st ex k being Nat st
( b₁ = 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
( b₂ = 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
b₁ = b₂

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 b₅ being Nat holds
( b₅ = ExitsAtWhile=0 (a,I,p,s) iff ex k being Nat st
( b₅ = 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 b₁, k being Nat st
( b₁ = 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 b₁, b₂ being Nat st ex k being Nat st
( b₁ = 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
( b₂ = 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
b₁ = b₂

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 b₅ being Nat holds
( b₅ = ExitsAtWhile>0 (a,I,p,s) iff ex k being Nat st
( b₅ = 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;