:: SCMFSA9A semantic presentation

scheme :: SCMFSA9A:sch 1
s1{ F₁( Nat) -> Nat, P₁[ set ] } :

ex b₁ being Nat st
( P₁[b₁] & ( for b₂ being Nat st P₁[b₂] holds
b₁ <= b₂ ) )

provided

E1: for b₁ being Nat holds
( F₁((b₁ + 1)) < F₁(b₁) or P₁[b₁] )

proof end;

theorem Th1: :: SCMFSA9A:1

for b₁ being natural number holds
( not b₁ is even iff ex b₂ being Nat st b₁ = (2 * b₂) + 1 )

proof end;

theorem Th2: :: SCMFSA9A:2

canceled;

theorem Th3: :: SCMFSA9A:3

canceled;

theorem Th4: :: SCMFSA9A:4

for b₁, b₂ being Integer st 0 < b₁ & 1 < b₂ holds
b₁ div b₂ < b₁

proof end;

theorem Th5: :: SCMFSA9A:5

canceled;

theorem Th6: :: SCMFSA9A:6

for b₁ being non empty with_non-empty_elements set
for b₂ being non empty non void halting IC-Ins-separated definite AMI-Struct of b₁
for b₃ being State of b₂
for b₄ being Nat st CurInstr ((Computation b₃) . b₄) = halt b₂ holds
(Computation b₃) . (LifeSpan b₃) = (Computation b₃) . b₄

proof end;

theorem Th7: :: SCMFSA9A:7

for b₁ being Instruction-Location of SCM+FSA
for b₂ being Instruction of SCM+FSA holds UsedIntLoc (b₁ .--> b₂) = UsedIntLoc b₂

proof end;

theorem Th8: :: SCMFSA9A:8

for b₁ being Instruction-Location of SCM+FSA
for b₂ being Instruction of SCM+FSA holds UsedInt*Loc (b₁ .--> b₂) = UsedInt*Loc b₂

proof end;

theorem Th9: :: SCMFSA9A:9

UsedIntLoc SCM+FSA-Stop = {} by Th7, SCMFSA_4:def 5, SF_MASTR:17;

theorem Th10: :: SCMFSA9A:10

UsedInt*Loc SCM+FSA-Stop = {}

proof end;

theorem Th11: :: SCMFSA9A:11

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

proof end;

theorem Th12: :: SCMFSA9A:12

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

proof end;

set c₁ = Int-Locations \/ FinSeq-Locations ;

set c₂ = Start-At (insloc 0);

set c₃ = the Instruction-Locations of SCM+FSA ;

theorem Th13: :: SCMFSA9A:13

for b₁ being Int-Location
for b₂, b₃ being Macro-Instruction holds UsedIntLoc (if=0 b₁,b₂,b₃) = ({b₁} \/ (UsedIntLoc b₂)) \/ (UsedIntLoc b₃)

proof end;

theorem Th14: :: SCMFSA9A:14

for b₁, b₂ being Macro-Instruction
for b₃ being Int-Location holds UsedInt*Loc (if=0 b₃,b₁,b₂) = (UsedInt*Loc b₁) \/ (UsedInt*Loc b₂)

proof end;

theorem Th15: :: SCMFSA9A:15

for b₁ being Int-Location
for b₂, b₃ being Macro-Instruction holds UsedIntLoc (if>0 b₁,b₂,b₃) = ({b₁} \/ (UsedIntLoc b₂)) \/ (UsedIntLoc b₃)

proof end;

theorem Th16: :: SCMFSA9A:16

for b₁ being Int-Location
for b₂, b₃ being Macro-Instruction holds UsedInt*Loc (if>0 b₁,b₂,b₃) = (UsedInt*Loc b₂) \/ (UsedInt*Loc b₃)

proof end;

Lemma14: for b₁ being Int-Location
for b₂ being Macro-Instruction holds
( insloc ((card b₂) + 4) in dom (if=0 b₁,(b₂ ';' (Goto (insloc 0))),SCM+FSA-Stop ) & (if=0 b₁,(b₂ ';' (Goto (insloc 0))),SCM+FSA-Stop ) . (insloc ((card b₂) + 4)) = goto ((insloc 0) + ((card b₂) + 4)) )

proof end;

Lemma15: for b₁ being Int-Location
for b₂ being Macro-Instruction holds UsedIntLoc (if=0 b₁,(b₂ ';' (Goto (insloc 0))),SCM+FSA-Stop ) = UsedIntLoc ((if=0 b₁,(b₂ ';' (Goto (insloc 0))),SCM+FSA-Stop ) +* ((insloc ((card b₂) + 4)) .--> (goto (insloc 0))))

proof end;

Lemma16: for b₁ being Int-Location
for b₂ being Macro-Instruction holds UsedInt*Loc (if=0 b₁,(b₂ ';' (Goto (insloc 0))),SCM+FSA-Stop ) = UsedInt*Loc ((if=0 b₁,(b₂ ';' (Goto (insloc 0))),SCM+FSA-Stop ) +* ((insloc ((card b₂) + 4)) .--> (goto (insloc 0))))

proof end;

theorem Th17: :: SCMFSA9A:17

for b₁ being Int-Location
for b₂ being Macro-Instruction holds UsedIntLoc (while=0 b₁,b₂) = {b₁} \/ (UsedIntLoc b₂)

proof end;

theorem Th18: :: SCMFSA9A:18

for b₁ being Int-Location
for b₂ being Macro-Instruction holds UsedInt*Loc (while=0 b₁,b₂) = UsedInt*Loc b₂

proof end;

definition

let c₄ be State of SCM+FSA ;
let c₅ be read-write Int-Location ;
let c₆ be Macro-Instruction;
pred ProperBodyWhile=0 c₂,c₃,c₁ means :Def1: :: SCMFSA9A:def 1
for b₁ being Nat st ((StepWhile=0 a₂,a₃,a₁) . b₁) . a₂ = 0 holds
( a₃ is_closed_on (StepWhile=0 a₂,a₃,a₁) . b₁ & a₃ is_halting_on (StepWhile=0 a₂,a₃,a₁) . b₁ );
pred WithVariantWhile=0 c₂,c₃,c₁ means :Def2: :: SCMFSA9A:def 2
ex b₁ being Function of product the Object-Kind of SCM+FSA , NAT st
for b₂ being Nat holds
( b₁ . ((StepWhile=0 a₂,a₃,a₁) . (b₂ + 1)) < b₁ . ((StepWhile=0 a₂,a₃,a₁) . b₂) or ((StepWhile=0 a₂,a₃,a₁) . b₂) . a₂ <> 0 );

end;

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

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

theorem Th19: :: SCMFSA9A:19

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being parahalting Macro-Instruction holds ProperBodyWhile=0 b₂,b₃,b₁

proof end;

theorem Th20: :: SCMFSA9A:20

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Macro-Instruction st ProperBodyWhile=0 b₂,b₃,b₁ & WithVariantWhile=0 b₂,b₃,b₁ holds
( while=0 b₂,b₃ is_halting_on b₁ & while=0 b₂,b₃ is_closed_on b₁ )

proof end;

theorem Th21: :: SCMFSA9A:21

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being parahalting Macro-Instruction st WithVariantWhile=0 b₂,b₃,b₁ holds
( while=0 b₂,b₃ is_halting_on b₁ & while=0 b₂,b₃ is_closed_on b₁ )

proof end;

theorem Th22: :: SCMFSA9A:22

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Macro-Instruction st (while=0 b₂,b₃) +* (Start-At (insloc 0)) c= b₁ & b₁ . b₂ <> 0 holds
( LifeSpan b₁ = 4 & ( for b₄ being Nat holds ((Computation b₁) . b₄) | (Int-Locations \/ FinSeq-Locations ) = b₁ | (Int-Locations \/ FinSeq-Locations ) ) )

proof end;

theorem Th23: :: SCMFSA9A:23

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Macro-Instruction st b₃ is_closed_on b₁ & b₃ is_halting_on b₁ & b₁ . b₂ = 0 holds
((Computation (b₁ +* ((while=0 b₂,b₃) +* (Start-At (insloc 0))))) . ((LifeSpan (b₁ +* (b₃ +* (Start-At (insloc 0))))) + 3)) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b₁ +* (b₃ +* (Start-At (insloc 0))))) . (LifeSpan (b₁ +* (b₃ +* (Start-At (insloc 0)))))) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th24: :: SCMFSA9A:24

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Macro-Instruction
for b₄ being Nat st ((StepWhile=0 b₂,b₃,b₁) . b₄) . b₂ <> 0 holds
((StepWhile=0 b₂,b₃,b₁) . (b₄ + 1)) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile=0 b₂,b₃,b₁) . b₄) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th25: :: SCMFSA9A:25

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Macro-Instruction
for b₄ being Nat st ( ( b₃ is_halting_on Initialize ((StepWhile=0 b₂,b₃,b₁) . b₄) & b₃ is_closed_on Initialize ((StepWhile=0 b₂,b₃,b₁) . b₄) ) or b₃ is parahalting ) & ((StepWhile=0 b₂,b₃,b₁) . b₄) . b₂ = 0 & ((StepWhile=0 b₂,b₃,b₁) . b₄) . (intloc 0) = 1 holds
((StepWhile=0 b₂,b₃,b₁) . (b₄ + 1)) | (Int-Locations \/ FinSeq-Locations ) = (IExec b₃,((StepWhile=0 b₂,b₃,b₁) . b₄)) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th26: :: SCMFSA9A:26

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being good Macro-Instruction st ( ProperBodyWhile=0 b₂,b₃,b₁ or b₃ is parahalting ) & b₁ . (intloc 0) = 1 holds
for b₄ being Nat holds ((StepWhile=0 b₂,b₃,b₁) . b₄) . (intloc 0) = 1

proof end;

theorem Th27: :: SCMFSA9A:27

for b₁, b₂ being State of SCM+FSA
for b₃ being read-write Int-Location
for b₄ being Macro-Instruction st ProperBodyWhile=0 b₃,b₄,b₁ & b₁ | (Int-Locations \/ FinSeq-Locations ) = b₂ | (Int-Locations \/ FinSeq-Locations ) holds
for b₅ being Nat holds ((StepWhile=0 b₃,b₄,b₁) . b₅) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile=0 b₃,b₄,b₂) . b₅) | (Int-Locations \/ FinSeq-Locations )

proof end;

definition

let c₄ be State of SCM+FSA ;
let c₅ be read-write Int-Location ;
let c₆ be Macro-Instruction;
assume that
E26: ( ProperBodyWhile=0 c₅,c₆,c₄ or c₆ is parahalting ) and
E27: WithVariantWhile=0 c₅,c₆,c₄ ;
func ExitsAtWhile=0 c₂,c₃,c₁ -> Nat means :Def3: :: SCMFSA9A:def 3
ex b₁ being Nat st
( a₄ = b₁ & ((StepWhile=0 a₂,a₃,a₁) . b₁) . a₂ <> 0 & ( for b₂ being Nat st ((StepWhile=0 a₂,a₃,a₁) . b₂) . a₂ <> 0 holds
b₁ <= b₂ ) & ((Computation (a₁ +* ((while=0 a₂,a₃) +* (Start-At (insloc 0))))) . (LifeSpan (a₁ +* ((while=0 a₂,a₃) +* (Start-At (insloc 0)))))) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile=0 a₂,a₃,a₁) . b₁) | (Int-Locations \/ FinSeq-Locations ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th28: :: SCMFSA9A:28

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Macro-Instruction st b₁ . (intloc 0) = 1 & b₁ . b₂ <> 0 holds
(IExec (while=0 b₂,b₃),b₁) | (Int-Locations \/ FinSeq-Locations ) = b₁ | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th29: :: SCMFSA9A:29

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Macro-Instruction st ( ProperBodyWhile=0 b₂,b₃, Initialize b₁ or b₃ is parahalting ) & WithVariantWhile=0 b₂,b₃, Initialize b₁ holds
(IExec (while=0 b₂,b₃),b₁) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile=0 b₂,b₃,(Initialize b₁)) . (ExitsAtWhile=0 b₂,b₃,(Initialize b₁))) | (Int-Locations \/ FinSeq-Locations )

proof end;

Lemma27: for b₁ being Int-Location
for b₂ being Macro-Instruction holds
( insloc ((card b₂) + 4) in dom (if>0 b₁,(b₂ ';' (Goto (insloc 0))),SCM+FSA-Stop ) & (if>0 b₁,(b₂ ';' (Goto (insloc 0))),SCM+FSA-Stop ) . (insloc ((card b₂) + 4)) = goto ((insloc 0) + ((card b₂) + 4)) )

proof end;

Lemma28: for b₁ being Int-Location
for b₂ being Macro-Instruction holds UsedIntLoc (if>0 b₁,(b₂ ';' (Goto (insloc 0))),SCM+FSA-Stop ) = UsedIntLoc ((if>0 b₁,(b₂ ';' (Goto (insloc 0))),SCM+FSA-Stop ) +* ((insloc ((card b₂) + 4)) .--> (goto (insloc 0))))

proof end;

Lemma29: for b₁ being Int-Location
for b₂ being Macro-Instruction holds UsedInt*Loc (if>0 b₁,(b₂ ';' (Goto (insloc 0))),SCM+FSA-Stop ) = UsedInt*Loc ((if>0 b₁,(b₂ ';' (Goto (insloc 0))),SCM+FSA-Stop ) +* ((insloc ((card b₂) + 4)) .--> (goto (insloc 0))))

proof end;

theorem Th30: :: SCMFSA9A:30

for b₁ being Int-Location
for b₂ being Macro-Instruction holds UsedIntLoc (while>0 b₁,b₂) = {b₁} \/ (UsedIntLoc b₂)

proof end;

theorem Th31: :: SCMFSA9A:31

for b₁ being Int-Location
for b₂ being Macro-Instruction holds UsedInt*Loc (while>0 b₁,b₂) = UsedInt*Loc b₂

proof end;

definition

let c₄ be State of SCM+FSA ;
let c₅ be read-write Int-Location ;
let c₆ be Macro-Instruction;
pred ProperBodyWhile>0 c₂,c₃,c₁ means :Def4: :: SCMFSA9A:def 4
for b₁ being Nat st ((StepWhile>0 a₂,a₃,a₁) . b₁) . a₂ > 0 holds
( a₃ is_closed_on (StepWhile>0 a₂,a₃,a₁) . b₁ & a₃ is_halting_on (StepWhile>0 a₂,a₃,a₁) . b₁ );
pred WithVariantWhile>0 c₂,c₃,c₁ means :Def5: :: SCMFSA9A:def 5
ex b₁ being Function of product the Object-Kind of SCM+FSA , NAT st
for b₂ being Nat holds
( b₁ . ((StepWhile>0 a₂,a₃,a₁) . (b₂ + 1)) < b₁ . ((StepWhile>0 a₂,a₃,a₁) . b₂) or ((StepWhile>0 a₂,a₃,a₁) . b₂) . a₂ <= 0 );

end;

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

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

theorem Th32: :: SCMFSA9A:32

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being parahalting Macro-Instruction holds ProperBodyWhile>0 b₂,b₃,b₁

proof end;

theorem Th33: :: SCMFSA9A:33

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Macro-Instruction st ProperBodyWhile>0 b₂,b₃,b₁ & WithVariantWhile>0 b₂,b₃,b₁ holds
( while>0 b₂,b₃ is_halting_on b₁ & while>0 b₂,b₃ is_closed_on b₁ )

proof end;

theorem Th34: :: SCMFSA9A:34

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being parahalting Macro-Instruction st WithVariantWhile>0 b₂,b₃,b₁ holds
( while>0 b₂,b₃ is_halting_on b₁ & while>0 b₂,b₃ is_closed_on b₁ )

proof end;

theorem Th35: :: SCMFSA9A:35

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Macro-Instruction st (while>0 b₂,b₃) +* (Start-At (insloc 0)) c= b₁ & b₁ . b₂ <= 0 holds
( LifeSpan b₁ = 4 & ( for b₄ being Nat holds ((Computation b₁) . b₄) | (Int-Locations \/ FinSeq-Locations ) = b₁ | (Int-Locations \/ FinSeq-Locations ) ) )

proof end;

theorem Th36: :: SCMFSA9A:36

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Macro-Instruction st b₃ is_closed_on b₁ & b₃ is_halting_on b₁ & b₁ . b₂ > 0 holds
((Computation (b₁ +* ((while>0 b₂,b₃) +* (Start-At (insloc 0))))) . ((LifeSpan (b₁ +* (b₃ +* (Start-At (insloc 0))))) + 3)) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b₁ +* (b₃ +* (Start-At (insloc 0))))) . (LifeSpan (b₁ +* (b₃ +* (Start-At (insloc 0)))))) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th37: :: SCMFSA9A:37

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Macro-Instruction
for b₄ being Nat st ((StepWhile>0 b₂,b₃,b₁) . b₄) . b₂ <= 0 holds
((StepWhile>0 b₂,b₃,b₁) . (b₄ + 1)) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 b₂,b₃,b₁) . b₄) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th38: :: SCMFSA9A:38

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Macro-Instruction
for b₄ being Nat st ( ( b₃ is_halting_on Initialize ((StepWhile>0 b₂,b₃,b₁) . b₄) & b₃ is_closed_on Initialize ((StepWhile>0 b₂,b₃,b₁) . b₄) ) or b₃ is parahalting ) & ((StepWhile>0 b₂,b₃,b₁) . b₄) . b₂ > 0 & ((StepWhile>0 b₂,b₃,b₁) . b₄) . (intloc 0) = 1 holds
((StepWhile>0 b₂,b₃,b₁) . (b₄ + 1)) | (Int-Locations \/ FinSeq-Locations ) = (IExec b₃,((StepWhile>0 b₂,b₃,b₁) . b₄)) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th39: :: SCMFSA9A:39

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being good Macro-Instruction st ( ProperBodyWhile>0 b₂,b₃,b₁ or b₃ is parahalting ) & b₁ . (intloc 0) = 1 holds
for b₄ being Nat holds ((StepWhile>0 b₂,b₃,b₁) . b₄) . (intloc 0) = 1

proof end;

theorem Th40: :: SCMFSA9A:40

for b₁, b₂ being State of SCM+FSA
for b₃ being read-write Int-Location
for b₄ being Macro-Instruction st ProperBodyWhile>0 b₃,b₄,b₁ & b₁ | (Int-Locations \/ FinSeq-Locations ) = b₂ | (Int-Locations \/ FinSeq-Locations ) holds
for b₅ being Nat holds ((StepWhile>0 b₃,b₄,b₁) . b₅) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 b₃,b₄,b₂) . b₅) | (Int-Locations \/ FinSeq-Locations )

proof end;

definition

let c₄ be State of SCM+FSA ;
let c₅ be read-write Int-Location ;
let c₆ be Macro-Instruction;
assume that
E41: ( ProperBodyWhile>0 c₅,c₆,c₄ or c₆ is parahalting ) and
E42: WithVariantWhile>0 c₅,c₆,c₄ ;
func ExitsAtWhile>0 c₂,c₃,c₁ -> Nat means :Def6: :: SCMFSA9A:def 6
ex b₁ being Nat st
( a₄ = b₁ & ((StepWhile>0 a₂,a₃,a₁) . b₁) . a₂ <= 0 & ( for b₂ being Nat st ((StepWhile>0 a₂,a₃,a₁) . b₂) . a₂ <= 0 holds
b₁ <= b₂ ) & ((Computation (a₁ +* ((while>0 a₂,a₃) +* (Start-At (insloc 0))))) . (LifeSpan (a₁ +* ((while>0 a₂,a₃) +* (Start-At (insloc 0)))))) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 a₂,a₃,a₁) . b₁) | (Int-Locations \/ FinSeq-Locations ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th41: :: SCMFSA9A:41

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Macro-Instruction st b₁ . (intloc 0) = 1 & b₁ . b₂ <= 0 holds
(IExec (while>0 b₂,b₃),b₁) | (Int-Locations \/ FinSeq-Locations ) = b₁ | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th42: :: SCMFSA9A:42

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Macro-Instruction st ( ProperBodyWhile>0 b₂,b₃, Initialize b₁ or b₃ is parahalting ) & WithVariantWhile>0 b₂,b₃, Initialize b₁ holds
(IExec (while>0 b₂,b₃),b₁) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 b₂,b₃,(Initialize b₁)) . (ExitsAtWhile>0 b₂,b₃,(Initialize b₁))) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th43: :: SCMFSA9A:43

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Macro-Instruction
for b₄ being Nat st ((StepWhile>0 b₂,b₃,b₁) . b₄) . b₂ <= 0 holds
for b₅ being Nat st b₄ <= b₅ holds
((StepWhile>0 b₂,b₃,b₁) . b₅) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 b₂,b₃,b₁) . b₄) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th44: :: SCMFSA9A:44

for b₁, b₂ being State of SCM+FSA
for b₃ being read-write Int-Location
for b₄ being Macro-Instruction st b₁ | (Int-Locations \/ FinSeq-Locations ) = b₂ | (Int-Locations \/ FinSeq-Locations ) & ProperBodyWhile>0 b₃,b₄,b₁ holds
ProperBodyWhile>0 b₃,b₄,b₂

proof end;

Lemma44: for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction st b₁ . (intloc 0) = 1 holds
( b₂ is_closed_on b₁ iff b₂ is_closed_on Initialize b₁ )

proof end;

Lemma45: for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction st b₁ . (intloc 0) = 1 holds
( b₂ is_closed_on b₁ & b₂ is_halting_on b₁ iff ( b₂ is_closed_on Initialize b₁ & b₂ is_halting_on Initialize b₁ ) )

proof end;

theorem Th45: :: SCMFSA9A:45

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being good Macro-Instruction st b₁ . (intloc 0) = 1 & ProperBodyWhile>0 b₂,b₃,b₁ & WithVariantWhile>0 b₂,b₃,b₁ holds
for b₄, b₅ being Nat st b₄ <> b₅ & b₄ <= ExitsAtWhile>0 b₂,b₃,b₁ & b₅ <= ExitsAtWhile>0 b₂,b₃,b₁ holds
( (StepWhile>0 b₂,b₃,b₁) . b₄ <> (StepWhile>0 b₂,b₃,b₁) . b₅ & ((StepWhile>0 b₂,b₃,b₁) . b₄) | (Int-Locations \/ FinSeq-Locations ) <> ((StepWhile>0 b₂,b₃,b₁) . b₅) | (Int-Locations \/ FinSeq-Locations ) )

proof end;

definition

let c₄ be Function of product the Object-Kind of SCM+FSA , NAT ;
attr a₁ is on_data_only means :Def7: :: SCMFSA9A:def 7
for b₁, b₂ being State of SCM+FSA st b₁ | (Int-Locations \/ FinSeq-Locations ) = b₂ | (Int-Locations \/ FinSeq-Locations ) holds
a₁ . b₁ = a₁ . b₂;

end;

:: deftheorem Def7 defines on_data_only SCMFSA9A:def 7 :

theorem Th46: :: SCMFSA9A:46

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being good Macro-Instruction st b₁ . (intloc 0) = 1 & ProperBodyWhile>0 b₂,b₃,b₁ & WithVariantWhile>0 b₂,b₃,b₁ holds
ex b₄ being Function of product the Object-Kind of SCM+FSA , NAT st
( b₄ is on_data_only & ( for b₅ being Nat holds
( b₄ . ((StepWhile>0 b₂,b₃,b₁) . (b₅ + 1)) < b₄ . ((StepWhile>0 b₂,b₃,b₁) . b₅) or ((StepWhile>0 b₂,b₃,b₁) . b₅) . b₂ <= 0 ) ) )

proof end;

theorem Th47: :: SCMFSA9A:47

for b₁, b₂ being State of SCM+FSA
for b₃ being read-write Int-Location
for b₄ being good Macro-Instruction st b₁ . (intloc 0) = 1 & b₁ | (Int-Locations \/ FinSeq-Locations ) = b₂ | (Int-Locations \/ FinSeq-Locations ) & ProperBodyWhile>0 b₃,b₄,b₁ & WithVariantWhile>0 b₃,b₄,b₁ holds
WithVariantWhile>0 b₃,b₄,b₂

proof end;

definition

let c₄, c₅ be Int-Location ;
set c₆ = 1 -stRWNotIn {c₄,c₅};
set c₇ = 2 -ndRWNotIn {c₄,c₅};
set c₈ = 3 -rdRWNotIn {c₄,c₅};
func Fusc_macro c₁,c₂ -> Macro-Instruction equals :: SCMFSA9A:def 8
(((SubFrom a₂,a₂) ';' ((1 -stRWNotIn {a₁,a₂}) := (intloc 0))) ';' ((2 -ndRWNotIn {a₁,a₂}) := a₁)) ';' (while>0 (2 -ndRWNotIn {a₁,a₂}),((((3 -rdRWNotIn {a₁,a₂}) := 2) ';' (Divide (2 -ndRWNotIn {a₁,a₂}),(3 -rdRWNotIn {a₁,a₂}))) ';' (if=0 (3 -rdRWNotIn {a₁,a₂}),(Macro (AddTo (1 -stRWNotIn {a₁,a₂}),a₂)),(Macro (AddTo a₂,(1 -stRWNotIn {a₁,a₂}))))));
correctness ;

end;

:: deftheorem Def8 defines Fusc_macro SCMFSA9A:def 8 :

theorem Th48: :: SCMFSA9A:48

for b₁ being State of SCM+FSA
for b₂, b₃ being read-write Int-Location st b₂ <> b₃ holds
for b₄ being Nat st b₄ = b₁ . b₂ holds
( (IExec (Fusc_macro b₂,b₃),b₁) . b₃ = Fusc b₄ & (IExec (Fusc_macro b₂,b₃),b₁) . b₂ = b₄ )

proof end;