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

begin

theorem :: SCMFSA9A:1

canceled;

theorem :: SCMFSA9A:2

canceled;

theorem :: SCMFSA9A:3

canceled;

theorem :: SCMFSA9A:4

canceled;

theorem :: SCMFSA9A:5

canceled;

theorem :: SCMFSA9A:6

canceled;

theorem Th7: :: SCMFSA9A:7

for l being Instruction-Location of SCM+FSA
for i being Instruction of SCM+FSA holds UsedIntLoc (l .--> i) = UsedIntLoc i

proof end;

theorem Th8: :: SCMFSA9A:8

for l being Instruction-Location of SCM+FSA
for i being Instruction of SCM+FSA holds UsedInt*Loc (l .--> i) = UsedInt*Loc i

proof end;

theorem Th9: :: SCMFSA9A:9

UsedIntLoc (Stop SCM+FSA ) = {}

proof end;

theorem Th10: :: SCMFSA9A:10

UsedInt*Loc (Stop SCM+FSA ) = {}

proof end;

theorem Th11: :: SCMFSA9A:11

for l being Instruction-Location of SCM+FSA holds UsedIntLoc (Goto l) = {}

proof end;

theorem Th12: :: SCMFSA9A:12

for l being Instruction-Location of SCM+FSA holds UsedInt*Loc (Goto l) = {}

proof end;

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

set SAt = Start-At (insloc 0 );

theorem Th13: :: SCMFSA9A:13

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)

proof end;

theorem Th14: :: SCMFSA9A:14

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)

proof end;

theorem Th15: :: SCMFSA9A:15

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)

proof end;

theorem Th16: :: SCMFSA9A:16

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)

proof end;

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 (insloc 0 ))),(Stop SCM+FSA )) & (if=0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) . ((card I) + 4) = goto ((insloc 0 ) + ((card I) + 4)) )

proof end;

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

proof end;

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

proof end;

theorem :: SCMFSA9A:17

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

proof end;

theorem :: SCMFSA9A:18

for b being Int-Location
for I being Program of SCM+FSA holds UsedInt*Loc (while=0 b,I) = UsedInt*Loc I

proof end;

definition

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

end;

:: deftheorem Def1 defines ProperBodyWhile=0 SCMFSA9A:def 1 :

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 iff for k being Element of NAT st ((StepWhile=0 a,I,s) . k) . a = 0 holds
( I is_closed_on (StepWhile=0 a,I,s) . k & I is_halting_on (StepWhile=0 a,I,s) . k ) );

:: deftheorem Def2 defines WithVariantWhile=0 SCMFSA9A:def 2 :

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 iff ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
for k being Element of NAT holds
( f . ((StepWhile=0 a,I,s) . (k + 1)) < f . ((StepWhile=0 a,I,s) . k) or ((StepWhile=0 a,I,s) . k) . a <> 0 ) );

theorem Th19: :: SCMFSA9A:19

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

proof end;

theorem Th20: :: SCMFSA9A:20

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 & WithVariantWhile=0 a,I,s holds
( while=0 a,I is_halting_on s & while=0 a,I is_closed_on s )

proof end;

theorem Th21: :: SCMFSA9A:21

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 holds
( while=0 a,I is_halting_on s & while=0 a,I is_closed_on s )

proof end;

theorem Th22: :: SCMFSA9A:22

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Program of SCM+FSA st (while=0 a,I) +* (Start-At (insloc 0 )) c= s & s . a <> 0 holds
( LifeSpan s = 4 & ( for k being Element of NAT holds DataPart (Computation s,k) = DataPart s ) )

proof end;

theorem Th23: :: SCMFSA9A:23

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 & I is_halting_on s & s . a = 0 holds
DataPart (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 3)) = DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))))

proof end;

theorem Th24: :: SCMFSA9A:24

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,s) . k) . a <> 0 holds
DataPart ((StepWhile=0 a,I,s) . (k + 1)) = DataPart ((StepWhile=0 a,I,s) . k)

proof end;

theorem Th25: :: SCMFSA9A:25

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 Initialize ((StepWhile=0 a,I,s) . k) & I is_closed_on Initialize ((StepWhile=0 a,I,s) . k) ) or I is parahalting ) & ((StepWhile=0 a,I,s) . k) . a = 0 & ((StepWhile=0 a,I,s) . k) . (intloc 0 ) = 1 holds
DataPart ((StepWhile=0 a,I,s) . (k + 1)) = DataPart (IExec I,((StepWhile=0 a,I,s) . k))

proof end;

theorem :: SCMFSA9A:26

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 or Ig is parahalting ) & s . (intloc 0 ) = 1 holds
for k being Element of NAT holds ((StepWhile=0 a,Ig,s) . k) . (intloc 0 ) = 1

proof end;

theorem :: SCMFSA9A:27

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 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds DataPart ((StepWhile=0 a,I,s1) . k) = DataPart ((StepWhile=0 a,I,s2) . k)

proof end;

definition

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 or I is parahalting ) and
A2: WithVariantWhile=0 a,I,s ;
func ExitsAtWhile=0 a,I,s -> Element of NAT means :Def3: :: SCMFSA9A:def 3
ex k being Element of NAT st
( it = k & ((StepWhile=0 a,I,s) . k) . a <> 0 & ( for i being Element of NAT st ((StepWhile=0 a,I,s) . i) . a <> 0 holds
k <= i ) & DataPart (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile=0 a,I,s) . k) );
existence
ex b₁, k being Element of NAT st
( b₁ = k & ((StepWhile=0 a,I,s) . k) . a <> 0 & ( for i being Element of NAT st ((StepWhile=0 a,I,s) . i) . a <> 0 holds
k <= i ) & DataPart (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile=0 a,I,s) . k) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ex k being Element of NAT st
( b₁ = k & ((StepWhile=0 a,I,s) . k) . a <> 0 & ( for i being Element of NAT st ((StepWhile=0 a,I,s) . i) . a <> 0 holds
k <= i ) & DataPart (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile=0 a,I,s) . k) ) & ex k being Element of NAT st
( b₂ = k & ((StepWhile=0 a,I,s) . k) . a <> 0 & ( for i being Element of NAT st ((StepWhile=0 a,I,s) . i) . a <> 0 holds
k <= i ) & DataPart (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile=0 a,I,s) . k) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines ExitsAtWhile=0 SCMFSA9A:def 3 :

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 or I is parahalting ) & WithVariantWhile=0 a,I,s holds
for b₄ being Element of NAT holds
( b₄ = ExitsAtWhile=0 a,I,s iff ex k being Element of NAT st
( b₄ = k & ((StepWhile=0 a,I,s) . k) . a <> 0 & ( for i being Element of NAT st ((StepWhile=0 a,I,s) . i) . a <> 0 holds
k <= i ) & DataPart (Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while=0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile=0 a,I,s) . k) ) );

theorem :: SCMFSA9A:28

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 & s . a <> 0 holds
DataPart (IExec (while=0 a,I),s) = DataPart s

proof end;

theorem :: SCMFSA9A:29

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, Initialize s or I is parahalting ) & WithVariantWhile=0 a,I, Initialize s holds
DataPart (IExec (while=0 a,I),s) = DataPart ((StepWhile=0 a,I,(Initialize s)) . (ExitsAtWhile=0 a,I,(Initialize s)))

proof end;

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 (insloc 0 ))),(Stop SCM+FSA )) & (if>0 a,(I ';' (Goto (insloc 0 ))),(Stop SCM+FSA )) . ((card I) + 4) = goto ((insloc 0 ) + ((card I) + 4)) )

proof end;

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

proof end;

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

proof end;

theorem :: SCMFSA9A:30

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

proof end;

theorem :: SCMFSA9A:31

for b being Int-Location
for I being Program of SCM+FSA holds UsedInt*Loc (while>0 b,I) = UsedInt*Loc I

proof end;

definition

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 means :Def4: :: SCMFSA9A:def 4
for k being Element of NAT st ((StepWhile>0 a,I,s) . k) . a > 0 holds
( I is_closed_on (StepWhile>0 a,I,s) . k & I is_halting_on (StepWhile>0 a,I,s) . k );
pred WithVariantWhile>0 a,I,s means :Def5: :: SCMFSA9A:def 5
ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
for k being Element of NAT holds
( f . ((StepWhile>0 a,I,s) . (k + 1)) < f . ((StepWhile>0 a,I,s) . k) or ((StepWhile>0 a,I,s) . k) . a <= 0 );

end;

:: deftheorem Def4 defines ProperBodyWhile>0 SCMFSA9A:def 4 :

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 iff for k being Element of NAT st ((StepWhile>0 a,I,s) . k) . a > 0 holds
( I is_closed_on (StepWhile>0 a,I,s) . k & I is_halting_on (StepWhile>0 a,I,s) . k ) );

:: deftheorem Def5 defines WithVariantWhile>0 SCMFSA9A:def 5 :

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 iff ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
for k being Element of NAT holds
( f . ((StepWhile>0 a,I,s) . (k + 1)) < f . ((StepWhile>0 a,I,s) . k) or ((StepWhile>0 a,I,s) . k) . a <= 0 ) );

theorem Th32: :: SCMFSA9A:32

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

proof end;

theorem Th33: :: SCMFSA9A:33

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 & WithVariantWhile>0 a,I,s holds
( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )

proof end;

theorem Th34: :: SCMFSA9A:34

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 holds
( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )

proof end;

theorem Th35: :: SCMFSA9A:35

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Program of SCM+FSA st (while>0 a,I) +* (Start-At (insloc 0 )) c= s & s . a <= 0 holds
( LifeSpan s = 4 & ( for k being Element of NAT holds DataPart (Computation s,k) = DataPart s ) )

proof end;

theorem Th36: :: SCMFSA9A:36

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 & I is_halting_on s & s . a > 0 holds
DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),((LifeSpan (s +* (I +* (Start-At (insloc 0 ))))) + 3)) = DataPart (Computation (s +* (I +* (Start-At (insloc 0 )))),(LifeSpan (s +* (I +* (Start-At (insloc 0 ))))))

proof end;

theorem Th37: :: SCMFSA9A:37

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,s) . k) . a <= 0 holds
DataPart ((StepWhile>0 a,I,s) . (k + 1)) = DataPart ((StepWhile>0 a,I,s) . k)

proof end;

theorem Th38: :: SCMFSA9A:38

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 Initialize ((StepWhile>0 a,I,s) . k) & I is_closed_on Initialize ((StepWhile>0 a,I,s) . k) ) or I is parahalting ) & ((StepWhile>0 a,I,s) . k) . a > 0 & ((StepWhile>0 a,I,s) . k) . (intloc 0 ) = 1 holds
DataPart ((StepWhile>0 a,I,s) . (k + 1)) = DataPart (IExec I,((StepWhile>0 a,I,s) . k))

proof end;

theorem Th39: :: SCMFSA9A:39

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 or Ig is parahalting ) & s . (intloc 0 ) = 1 holds
for k being Element of NAT holds ((StepWhile>0 a,Ig,s) . k) . (intloc 0 ) = 1

proof end;

theorem Th40: :: SCMFSA9A:40

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 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds DataPart ((StepWhile>0 a,I,s1) . k) = DataPart ((StepWhile>0 a,I,s2) . k)

proof end;

definition

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 or I is parahalting ) and
A2: WithVariantWhile>0 a,I,s ;
func ExitsAtWhile>0 a,I,s -> Element of NAT means :Def6: :: SCMFSA9A:def 6
ex k being Element of NAT st
( it = k & ((StepWhile>0 a,I,s) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 a,I,s) . i) . a <= 0 holds
k <= i ) & DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile>0 a,I,s) . k) );
existence
ex b₁, k being Element of NAT st
( b₁ = k & ((StepWhile>0 a,I,s) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 a,I,s) . i) . a <= 0 holds
k <= i ) & DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile>0 a,I,s) . k) )

proof end;

uniqueness
for b₁, b₂ being Element of NAT st ex k being Element of NAT st
( b₁ = k & ((StepWhile>0 a,I,s) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 a,I,s) . i) . a <= 0 holds
k <= i ) & DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile>0 a,I,s) . k) ) & ex k being Element of NAT st
( b₂ = k & ((StepWhile>0 a,I,s) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 a,I,s) . i) . a <= 0 holds
k <= i ) & DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile>0 a,I,s) . k) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines ExitsAtWhile>0 SCMFSA9A:def 6 :

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 or I is parahalting ) & WithVariantWhile>0 a,I,s holds
for b₄ being Element of NAT holds
( b₄ = ExitsAtWhile>0 a,I,s iff ex k being Element of NAT st
( b₄ = k & ((StepWhile>0 a,I,s) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 a,I,s) . i) . a <= 0 holds
k <= i ) & DataPart (Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))),(LifeSpan (s +* ((while>0 a,I) +* (Start-At (insloc 0 )))))) = DataPart ((StepWhile>0 a,I,s) . k) ) );

theorem :: SCMFSA9A:41

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 & s . a <= 0 holds
DataPart (IExec (while>0 a,I),s) = DataPart s

proof end;

theorem Th42: :: SCMFSA9A:42

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, Initialize s or I is parahalting ) & WithVariantWhile>0 a,I, Initialize s holds
DataPart (IExec (while>0 a,I),s) = DataPart ((StepWhile>0 a,I,(Initialize s)) . (ExitsAtWhile>0 a,I,(Initialize s)))

proof end;

theorem Th43: :: SCMFSA9A:43

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

proof end;

theorem :: SCMFSA9A:44

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 & ProperBodyWhile>0 a,I,s1 holds
ProperBodyWhile>0 a,I,s2

proof end;

Lm7: 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 iff I is_closed_on Initialize s )

proof end;

Lm8: 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 & I is_halting_on s iff ( I is_closed_on Initialize s & I is_halting_on Initialize s ) )

proof end;

theorem Th45: :: SCMFSA9A:45

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 & ProperBodyWhile>0 a,Ig,s & WithVariantWhile>0 a,Ig,s holds
for i, j being Element of NAT st i <> j & i <= ExitsAtWhile>0 a,Ig,s & j <= ExitsAtWhile>0 a,Ig,s holds
( (StepWhile>0 a,Ig,s) . i <> (StepWhile>0 a,Ig,s) . j & DataPart ((StepWhile>0 a,Ig,s) . i) <> DataPart ((StepWhile>0 a,Ig,s) . j) )

proof end;

definition

let f be Function of (product the Object-Kind of SCM+FSA ),NAT ;
attr f is on_data_only means :Def7: :: SCMFSA9A:def 7
for s1, s2 being State of SCM+FSA st DataPart s1 = DataPart s2 holds
f . s1 = f . s2;

end;

:: deftheorem Def7 defines on_data_only SCMFSA9A:def 7 :

for f being Function of (product the Object-Kind of SCM+FSA ),NAT holds
( f is on_data_only iff for s1, s2 being State of SCM+FSA st DataPart s1 = DataPart s2 holds
f . s1 = f . s2 );

theorem Th46: :: SCMFSA9A:46

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 & ProperBodyWhile>0 a,Ig,s & WithVariantWhile>0 a,Ig,s holds
ex f being Function of (product the Object-Kind of SCM+FSA ),NAT st
( f is on_data_only & ( for k being Element of NAT holds
( f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) or ((StepWhile>0 a,Ig,s) . k) . a <= 0 ) ) )

proof end;

theorem :: SCMFSA9A:47

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 & DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,Ig,s1 & WithVariantWhile>0 a,Ig,s1 holds
WithVariantWhile>0 a,Ig,s2

proof end;

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}))))));

theorem :: SCMFSA9A:48

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),s) . result = Fusc n & (IExec (Fusc_macro N,result),s) . N = n )

proof end;