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


begin

theorem Th1: :: SCMFSA9A:1
for l being Element of NAT
for i being Instruction of SCM+FSA holds UsedIntLoc (l .--> i) = UsedIntLoc i
proofend;

theorem Th2: :: SCMFSA9A:2
for l being Element of NAT
for i being Instruction of SCM+FSA holds UsedInt*Loc (l .--> i) = UsedInt*Loc i
proofend;

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

theorem Th4: :: SCMFSA9A:4
UsedInt*Loc (Stop SCM+FSA) = {}
proofend;

theorem Th5: :: SCMFSA9A:5
for l being Element of NAT holds UsedIntLoc (Goto l) = {}
proofend;

theorem Th6: :: SCMFSA9A:6
for l being Element of NAT holds UsedInt*Loc (Goto l) = {}
proofend;

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

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

theorem Th7: :: SCMFSA9A:7
for b being Int-Location
for I, J being Program of SCM+FSA holds UsedIntLoc (if=0 (b,I,J)) = ({b} \/ (UsedIntLoc I)) \/ (UsedIntLoc J)
proofend;

theorem Th8: :: SCMFSA9A:8
for I, J being Program of SCM+FSA
for a being Int-Location holds UsedInt*Loc (if=0 (a,I,J)) = (UsedInt*Loc I) \/ (UsedInt*Loc J)
proofend;

theorem Th9: :: SCMFSA9A:9
for b being Int-Location
for I, J being Program of SCM+FSA holds UsedIntLoc (if>0 (b,I,J)) = ({b} \/ (UsedIntLoc I)) \/ (UsedIntLoc J)
proofend;

theorem Th10: :: SCMFSA9A:10
for b being Int-Location
for I, J being Program of SCM+FSA holds UsedInt*Loc (if>0 (b,I,J)) = (UsedInt*Loc I) \/ (UsedInt*Loc J)
proofend;

begin

Lm1:  for a being Int-Location
for I being Program of SCM+FSA holds
( (card I) + 4 in dom (if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) & (if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) . ((card I) + 4) = goto (0 + ((card I) + 4)) )
proofend;

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

Lm3:  for a being Int-Location
for I being Program of SCM+FSA holds UsedInt*Loc (if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) = UsedInt*Loc ((if=0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0)))
proofend;

theorem :: SCMFSA9A:11
for b being Int-Location
for I being Program of SCM+FSA holds UsedIntLoc (while=0 (b,I)) = {b} \/ (UsedIntLoc I)
proofend;

theorem :: SCMFSA9A:12
for b being Int-Location
for I being Program of SCM+FSA holds UsedInt*Loc (while=0 (b,I)) = UsedInt*Loc I
proofend;

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 Program of SCM+FSA;
pred ProperBodyWhile=0 a,I,s,p means :Def1: :: SCMFSA9A:def 1
 for k being Element of NAT st ((StepWhile=0 (a,I,p,s)) . k) . a = 0 holds
( I is_closed_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) & I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) );
pred WithVariantWhile=0 a,I,s,p means :Def2: :: SCMFSA9A:def 2
 ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for k being Element of 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 Def1 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 Program of SCM+FSA holds
( ProperBodyWhile=0 a,I,s,p iff for k being Element of NAT st ((StepWhile=0 (a,I,p,s)) . k) . a = 0 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)) ) );

:: deftheorem Def2 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 Program 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 Element of 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 Program of SCM+FSA holds ProperBodyWhile=0 a,I,s,p
proofend;

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 Program of SCM+FSA st ProperBodyWhile=0 a,I,s,p &amp; WithVariantWhile=0 a,I,s,p holds
( while=0 (a,I) is_halting_on s,p &amp; while=0 (a,I) is_closed_on s,p )
proofend;

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 parahalting Program of SCM+FSA st WithVariantWhile=0 a,I,s,p holds
( while=0 (a,I) is_halting_on s,p &amp; while=0 (a,I) is_closed_on s,p )
proofend;

theorem Th16: :: SCMFSA9A:16
for p being Instruction-Sequence of SCM+FSA
for a being read-write Int-Location
for I being Program of SCM+FSA
for s being 0 -started State of SCM+FSA st while=0 (a,I) c= p &amp; s . a <> 0 holds
( LifeSpan (p,s) = 4 &amp; ( for k being Element of NAT holds DataPart (Comput (p,s,k)) = DataPart s ) )
proofend;

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 Program of SCM+FSA st I is_closed_on s,p &amp; I is_halting_on s,p &amp; s . a = 0 holds
DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),((LifeSpan ((p +* I),(Initialize s))) + 3))) = DataPart (Comput ((p +* I),(Initialize s),(LifeSpan ((p +* I),(Initialize s)))))
proofend;

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 Program of SCM+FSA
for k being Element of 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)
proofend;

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 I being Program of SCM+FSA
for k being Element of NAT st ( ( I is_halting_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I)) &amp; I is_closed_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I)) ) or I is parahalting ) &amp; ((StepWhile=0 (a,I,p,s)) . k) . a = 0 &amp; ((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)))
proofend;

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 Program of SCM+FSA st ( ProperBodyWhile=0 a,Ig,s,p or Ig is parahalting ) &amp; s . (intloc 0) = 1 holds
for k being Element of NAT holds ((StepWhile=0 (a,Ig,p,s)) . k) . (intloc 0) = 1
proofend;

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 Program of SCM+FSA st ProperBodyWhile=0 a,I,s1,p1 &amp; DataPart s1 = DataPart s2 holds
for k being Element of NAT holds DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart ((StepWhile=0 (a,I,p2,s2)) . k)
proofend;

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 Program 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) ->  Element of NAT  means :Def3: :: SCMFSA9A:def 3
 ex k being Element of NAT st
( it = k &amp; ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 &amp; ( for i being Element of NAT st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) &amp; 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 Element of NAT st
( b1 = k &amp; ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 &amp; ( for i being Element of NAT st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) &amp; 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) )
proofend;
uniqueness
 for b1, b2 being Element of NAT st ex k being Element of NAT st
( b1 = k &amp; ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 &amp; ( for i being Element of NAT st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) &amp; 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) ) &amp; ex k being Element of NAT st
( b2 = k &amp; ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 &amp; ( for i being Element of NAT st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) &amp; 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
proofend;
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 Program of SCM+FSA st ( ProperBodyWhile=0 a,I,s,p or I is parahalting ) &amp; WithVariantWhile=0 a,I,s,p holds
for b5 being Element of NAT holds
( b5 = ExitsAtWhile=0 (a,I,p,s) iff ex k being Element of NAT st
( b5 = k &amp; ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 &amp; ( for i being Element of NAT st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds
k <= i ) &amp; 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 Program of SCM+FSA st s . (intloc 0) = 1 &amp; s . a <> 0 holds
DataPart (IExec ((while=0 (a,I)),p,s)) = DataPart s
proofend;

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 Program of SCM+FSA st ( ProperBodyWhile=0 a,I, Initialized s,p or I is parahalting ) &amp; 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))))
proofend;

begin

Lm4:  for a being Int-Location
for I being Program of SCM+FSA holds
( (card I) + 4 in dom (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) &amp; (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) . ((card I) + 4) = goto (0 + ((card I) + 4)) )
proofend;

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

Lm6:  for a being Int-Location
for I being Program of SCM+FSA holds UsedInt*Loc (if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) = UsedInt*Loc ((if>0 (a,(I ";" (Goto 0)),(Stop SCM+FSA))) +* (((card I) + 4) .--> (goto 0)))
proofend;

theorem :: SCMFSA9A:24
for b being Int-Location
for I being Program of SCM+FSA holds UsedIntLoc (while>0 (b,I)) = {b} \/ (UsedIntLoc I)
proofend;

theorem :: SCMFSA9A:25
for b being Int-Location
for I being Program of SCM+FSA holds UsedInt*Loc (while>0 (b,I)) = UsedInt*Loc I
proofend;

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 Program of SCM+FSA;
pred ProperBodyWhile>0 a,I,s,p means :Def4: :: SCMFSA9A:def 4
 for k being Element of NAT st ((StepWhile>0 (a,I,p,s)) . k) . a > 0 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)) );
pred WithVariantWhile>0 a,I,s,p means :Def5: :: SCMFSA9A:def 5
 ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for k being Element of 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 Def4 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 Program of SCM+FSA holds
( ProperBodyWhile>0 a,I,s,p iff for k being Element of NAT st ((StepWhile>0 (a,I,p,s)) . k) . a > 0 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)) ) );

:: deftheorem Def5 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 Program 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 Element of 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 Program of SCM+FSA holds ProperBodyWhile>0 a,I,s,p
proofend;

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 Program of SCM+FSA st ProperBodyWhile>0 a,I,s,p &amp; WithVariantWhile>0 a,I,s,p holds
( while>0 (a,I) is_halting_on s,p &amp; while>0 (a,I) is_closed_on s,p )
proofend;

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 parahalting Program of SCM+FSA st WithVariantWhile>0 a,I,s,p holds
( while>0 (a,I) is_halting_on s,p &amp; while>0 (a,I) is_closed_on s,p )
proofend;

theorem Th29: :: SCMFSA9A:29
for p being Instruction-Sequence of SCM+FSA
for a being read-write Int-Location
for I being Program of SCM+FSA
for s being 0 -started State of SCM+FSA st while>0 (a,I) c= p &amp; s . a <= 0 holds
( LifeSpan (p,s) = 4 &amp; ( for k being Element of NAT holds DataPart (Comput (p,s,k)) = DataPart s ) )
proofend;

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 Program of SCM+FSA st I is_closed_on s,p &amp; I is_halting_on s,p &amp; s . a > 0 holds
DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),((LifeSpan ((p +* I),(Initialize s))) + 3))) = DataPart (Comput ((p +* I),(Initialize s),(LifeSpan ((p +* I),(Initialize s)))))
proofend;

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 Program of SCM+FSA
for k being Element of 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)
proofend;

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 I being Program of SCM+FSA
for k being Element of NAT st ( ( I is_halting_on Initialized ((StepWhile>0 (a,I,p,s)) . k),p +* (while>0 (a,I)) &amp; I is_closed_on Initialized ((StepWhile>0 (a,I,p,s)) . k),p +* (while>0 (a,I)) ) or I is parahalting ) &amp; ((StepWhile>0 (a,I,p,s)) . k) . a > 0 &amp; ((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)))
proofend;

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 Program of SCM+FSA st ( ProperBodyWhile>0 a,Ig,s,p or Ig is parahalting ) &amp; s . (intloc 0) = 1 holds
for k being Element of NAT holds ((StepWhile>0 (a,Ig,p,s)) . k) . (intloc 0) = 1
proofend;

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 Program of SCM+FSA st ProperBodyWhile>0 a,I,s1,p1 &amp; DataPart s1 = DataPart s2 holds
for k being Element of NAT holds DataPart ((StepWhile>0 (a,I,p1,s1)) . k) = DataPart ((StepWhile>0 (a,I,p2,s2)) . k)
proofend;

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 Program 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) ->  Element of NAT  means :Def6: :: SCMFSA9A:def 6
 ex k being Element of NAT st
( it = k &amp; ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 &amp; ( for i being Element of NAT st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) &amp; 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 Element of NAT st
( b1 = k &amp; ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 &amp; ( for i being Element of NAT st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) &amp; 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) )
proofend;
uniqueness
 for b1, b2 being Element of NAT st ex k being Element of NAT st
( b1 = k &amp; ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 &amp; ( for i being Element of NAT st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) &amp; 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) ) &amp; ex k being Element of NAT st
( b2 = k &amp; ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 &amp; ( for i being Element of NAT st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) &amp; 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
proofend;
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 Program of SCM+FSA st ( ProperBodyWhile>0 a,I,s,p or I is parahalting ) &amp; WithVariantWhile>0 a,I,s,p holds
for b5 being Element of NAT holds
( b5 = ExitsAtWhile>0 (a,I,p,s) iff ex k being Element of NAT st
( b5 = k &amp; ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 &amp; ( for i being Element of NAT st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) &amp; 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: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 Program of SCM+FSA st s . (intloc 0) = 1 &amp; s . a <= 0 holds
DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart s
proofend;

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 Program of SCM+FSA st ( ProperBodyWhile>0 a,I, Initialized s,p or I is parahalting ) &amp; 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))))
proofend;

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 Program of SCM+FSA
for k being Element of NAT st ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 holds
for n being Element of NAT st k <= n holds
DataPart ((StepWhile>0 (a,I,p,s)) . n) = DataPart ((StepWhile>0 (a,I,p,s)) . k)
proofend;

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 Program of SCM+FSA st DataPart s1 = DataPart s2 &amp; ProperBodyWhile>0 a,I,s1,p1 holds
ProperBodyWhile>0 a,I,s2,p2
proofend;

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

Lm8:  for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of SCM+FSA st s . (intloc 0) = 1 holds
( I is_closed_on s,p &amp; I is_halting_on s,p iff ( I is_closed_on Initialized s,p &amp; I is_halting_on Initialized s,p ) )
proofend;

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 Program of SCM+FSA st s . (intloc 0) = 1 &amp; ProperBodyWhile>0 a,Ig,s,p &amp; WithVariantWhile>0 a,Ig,s,p holds
for i, j being Element of NAT st i <> j &amp; i <= ExitsAtWhile>0 (a,Ig,p,s) &amp; j <= ExitsAtWhile>0 (a,Ig,p,s) holds
( (StepWhile>0 (a,Ig,p,s)) . i <> (StepWhile>0 (a,Ig,p,s)) . j &amp; DataPart ((StepWhile>0 (a,Ig,p,s)) . i) <> DataPart ((StepWhile>0 (a,Ig,p,s)) . j) )
proofend;

definition
canceled;
end;

:: deftheorem  SCMFSA9A:def_7_:_
canceled;

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 Program of SCM+FSA st s . (intloc 0) = 1 &amp; ProperBodyWhile>0 a,Ig,s,p &amp; 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 &amp; ( for k being Element of 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 ) ) )
proofend;

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 Program of SCM+FSA st s1 . (intloc 0) = 1 &amp; DataPart s1 = DataPart s2 &amp; ProperBodyWhile>0 a,Ig,s1,p1 &amp; WithVariantWhile>0 a,Ig,s1,p1 holds
WithVariantWhile>0 a,Ig,s2,p2
proofend;

begin

definition
let N, result be Int-Location;
func Fusc_macro (N,result) ->  Program of SCM+FSA equals :: SCMFSA9A:def 8
(((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 Program of SCM+FSA;
;
end;

:: deftheorem  defines Fusc_macro SCMFSA9A:def_8_:_
 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
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 &amp; (IExec ((Fusc_macro (N,result)),p,s)) . N = n )
proofend;