:: SFMASTR2 semantic presentation

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

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

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

theorem Th1: :: SFMASTR2:1

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being Macro-Instruction st b₃ is_closed_on Initialize b₁ & b₃ is_halting_on Initialize b₁ & not b₂ in UsedIntLoc b₃ holds
(IExec b₃,b₁) . b₂ = (Initialize b₁) . b₂

proof end;

theorem Th2: :: SFMASTR2:2

for b₁ being State of SCM+FSA
for b₂ being FinSeq-Location
for b₃ being Macro-Instruction st b₃ is_closed_on Initialize b₁ & b₃ is_halting_on Initialize b₁ & not b₂ in UsedInt*Loc b₃ holds
(IExec b₃,b₁) . b₂ = (Initialize b₁) . b₂

proof end;

theorem Th3: :: SFMASTR2:3

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being Macro-Instruction st ( ( b₃ is_closed_on Initialize b₁ & b₃ is_halting_on Initialize b₁ ) or b₃ is parahalting ) & ( b₁ . (intloc 0) = 1 or not b₂ is read-only ) & not b₂ in UsedIntLoc b₃ holds
(IExec b₃,b₁) . b₂ = b₁ . b₂

proof end;

theorem Th4: :: SFMASTR2:4

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;

theorem Th5: :: SFMASTR2:5

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 Th6: :: SFMASTR2:6

for b₁, b₂ being State of SCM+FSA
for b₃ being Subset of Int-Locations
for b₄ being Subset of FinSeq-Locations holds
( b₁ | (b₃ \/ b₄) = b₂ | (b₃ \/ b₄) iff ( ( for b₅ being Int-Location st b₅ in b₃ holds
b₁ . b₅ = b₂ . b₅ ) & ( for b₅ being FinSeq-Location st b₅ in b₄ holds
b₁ . b₅ = b₂ . b₅ ) ) )

proof end;

theorem Th7: :: SFMASTR2:7

for b₁, b₂ being State of SCM+FSA
for b₃ being Subset of Int-Locations holds
( b₁ | (b₃ \/ FinSeq-Locations ) = b₂ | (b₃ \/ FinSeq-Locations ) iff ( ( for b₄ being Int-Location st b₄ in b₃ holds
b₁ . b₄ = b₂ . b₄ ) & ( for b₄ being FinSeq-Location holds b₁ . b₄ = b₂ . b₄ ) ) )

proof end;

definition

let c₄ be Int-Location ;
let c₅ be Macro-Instruction;
set c₆ = 1 -stRWNotIn ({c₄} \/ (UsedIntLoc c₅));
func times c₁,c₂ -> Macro-Instruction equals :: SFMASTR2:def 1
((1 -stRWNotIn ({a₁} \/ (UsedIntLoc a₂))) := a₁) ';' (while>0 (1 -stRWNotIn ({a₁} \/ (UsedIntLoc a₂))),(a₂ ';' (SubFrom (1 -stRWNotIn ({a₁} \/ (UsedIntLoc a₂))),(intloc 0))));
correctness ;

end;

:: deftheorem Def1 defines times SFMASTR2:def 1 :

notation

let c₄ be Int-Location ;
let c₅ be Macro-Instruction;
synonym c₁ times c₂ for times c₁,c₂;

end;

theorem Th8: :: SFMASTR2:8

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

proof end;

theorem Th9: :: SFMASTR2:9

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

proof end;

registration

let c₄ be good Macro-Instruction;
let c₅ be Int-Location ;
cluster times a₂,a₁ -> good ;
coherence ;

end;

definition

let c₄ be State of SCM+FSA ;
let c₅ be Macro-Instruction;
let c₆ be Int-Location ;
set c₇ = 1 -stRWNotIn ({c₆} \/ (UsedIntLoc c₅));
func StepTimes c₃,c₂,c₁ -> Function of NAT , product the Object-Kind of SCM+FSA equals :: SFMASTR2:def 2
StepWhile>0 (1 -stRWNotIn ({a₃} \/ (UsedIntLoc a₂))),(a₂ ';' (SubFrom (1 -stRWNotIn ({a₃} \/ (UsedIntLoc a₂))),(intloc 0))),(Exec ((1 -stRWNotIn ({a₃} \/ (UsedIntLoc a₂))) := a₃),(Initialize a₁));
correctness ;

end;

:: deftheorem Def2 defines StepTimes SFMASTR2:def 2 :

theorem Th10: :: SFMASTR2:10

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being good Macro-Instruction holds ((StepTimes b₂,b₃,b₁) . 0) . (intloc 0) = 1

proof end;

theorem Th11: :: SFMASTR2:11

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being good Macro-Instruction st ( b₁ . (intloc 0) = 1 or not b₂ is read-only ) holds
((StepTimes b₂,b₃,b₁) . 0) . (1 -stRWNotIn ({b₂} \/ (UsedIntLoc b₃))) = b₁ . b₂

proof end;

theorem Th12: :: SFMASTR2:12

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being good Macro-Instruction
for b₄ being Nat st ((StepTimes b₂,b₃,b₁) . b₄) . (intloc 0) = 1 & b₃ is_closed_on (StepTimes b₂,b₃,b₁) . b₄ & b₃ is_halting_on (StepTimes b₂,b₃,b₁) . b₄ holds
( ((StepTimes b₂,b₃,b₁) . (b₄ + 1)) . (intloc 0) = 1 & ( ((StepTimes b₂,b₃,b₁) . b₄) . (1 -stRWNotIn ({b₂} \/ (UsedIntLoc b₃))) > 0 implies ((StepTimes b₂,b₃,b₁) . (b₄ + 1)) . (1 -stRWNotIn ({b₂} \/ (UsedIntLoc b₃))) = (((StepTimes b₂,b₃,b₁) . b₄) . (1 -stRWNotIn ({b₂} \/ (UsedIntLoc b₃)))) - 1 ) )

proof end;

theorem Th13: :: SFMASTR2:13

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being Macro-Instruction st ( b₁ . (intloc 0) = 1 or not b₂ is read-only ) holds
((StepTimes b₂,b₃,b₁) . 0) . b₂ = b₁ . b₂

proof end;

theorem Th14: :: SFMASTR2:14

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being FinSeq-Location
for b₄ being Macro-Instruction holds ((StepTimes b₂,b₄,b₁) . 0) . b₃ = b₁ . b₃

proof end;

definition

let c₄ be State of SCM+FSA ;
let c₅ be Int-Location ;
let c₆ be Macro-Instruction;
pred ProperTimesBody c₂,c₃,c₁ means :Def3: :: SFMASTR2:def 3
for b₁ being Nat st b₁ < a₁ . a₂ holds
( a₃ is_closed_on (StepTimes a₂,a₃,a₁) . b₁ & a₃ is_halting_on (StepTimes a₂,a₃,a₁) . b₁ );

end;

:: deftheorem Def3 defines ProperTimesBody SFMASTR2:def 3 :

theorem Th15: :: SFMASTR2:15

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being Macro-Instruction st b₃ is parahalting holds
ProperTimesBody b₂,b₃,b₁

proof end;

theorem Th16: :: SFMASTR2:16

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being good Macro-Instruction st ProperTimesBody b₂,b₃,b₁ holds
for b₄ being Nat st b₄ <= b₁ . b₂ holds
((StepTimes b₂,b₃,b₁) . b₄) . (intloc 0) = 1

proof end;

theorem Th17: :: SFMASTR2:17

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being good Macro-Instruction st ( b₁ . (intloc 0) = 1 or not b₂ is read-only ) & ProperTimesBody b₂,b₃,b₁ holds
for b₄ being Nat st b₄ <= b₁ . b₂ holds
(((StepTimes b₂,b₃,b₁) . b₄) . (1 -stRWNotIn ({b₂} \/ (UsedIntLoc b₃)))) + b₄ = b₁ . b₂

proof end;

theorem Th18: :: SFMASTR2:18

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being good Macro-Instruction st ProperTimesBody b₂,b₃,b₁ & 0 <= b₁ . b₂ & ( b₁ . (intloc 0) = 1 or not b₂ is read-only ) holds
for b₄ being Nat st b₄ >= b₁ . b₂ holds
( ((StepTimes b₂,b₃,b₁) . b₄) . (1 -stRWNotIn ({b₂} \/ (UsedIntLoc b₃))) = 0 & ((StepTimes b₂,b₃,b₁) . b₄) . (intloc 0) = 1 )

proof end;

theorem Th19: :: SFMASTR2:19

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being Macro-Instruction st b₁ . (intloc 0) = 1 holds
((StepTimes b₂,b₃,b₁) . 0) | ((UsedIntLoc b₃) \/ FinSeq-Locations ) = b₁ | ((UsedIntLoc b₃) \/ FinSeq-Locations )

proof end;

theorem Th20: :: SFMASTR2:20

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being good Macro-Instruction
for b₄ being Nat st ((StepTimes b₂,b₃,b₁) . b₄) . (intloc 0) = 1 & b₃ is_halting_on Initialize ((StepTimes b₂,b₃,b₁) . b₄) & b₃ is_closed_on Initialize ((StepTimes b₂,b₃,b₁) . b₄) & ((StepTimes b₂,b₃,b₁) . b₄) . (1 -stRWNotIn ({b₂} \/ (UsedIntLoc b₃))) > 0 holds
((StepTimes b₂,b₃,b₁) . (b₄ + 1)) | ((UsedIntLoc b₃) \/ FinSeq-Locations ) = (IExec b₃,((StepTimes b₂,b₃,b₁) . b₄)) | ((UsedIntLoc b₃) \/ FinSeq-Locations )

proof end;

theorem Th21: :: SFMASTR2:21

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being good Macro-Instruction
for b₄ being Nat st ( ProperTimesBody b₂,b₃,b₁ or b₃ is parahalting ) & b₄ < b₁ . b₂ & ( b₁ . (intloc 0) = 1 or not b₂ is read-only ) holds
((StepTimes b₂,b₃,b₁) . (b₄ + 1)) | ((UsedIntLoc b₃) \/ FinSeq-Locations ) = (IExec b₃,((StepTimes b₂,b₃,b₁) . b₄)) | ((UsedIntLoc b₃) \/ FinSeq-Locations )

proof end;

theorem Th22: :: SFMASTR2:22

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

proof end;

theorem Th23: :: SFMASTR2:23

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being good Macro-Instruction
for b₄ being Nat st b₁ . b₂ = b₄ & ( ProperTimesBody b₂,b₃,b₁ or b₃ is parahalting ) & ( b₁ . (intloc 0) = 1 or not b₂ is read-only ) holds
(IExec (times b₂,b₃),b₁) | (Int-Locations \/ FinSeq-Locations ) = ((StepTimes b₂,b₃,b₁) . b₄) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th24: :: SFMASTR2:24

for b₁ being State of SCM+FSA
for b₂ being Int-Location
for b₃ being good Macro-Instruction st b₁ . (intloc 0) = 1 & ( ProperTimesBody b₂,b₃,b₁ or b₃ is parahalting ) holds
( times b₂,b₃ is_closed_on b₁ & times b₂,b₃ is_halting_on b₁ )

proof end;

definition

let c₄ be read-write Int-Location ;
func triv-times c₁ -> Macro-Instruction equals :: SFMASTR2:def 4
times a₁,((while=0 a₁,(Macro (a₁ := a₁))) ';' (SubFrom a₁,(intloc 0)));
correctness ;

end;

:: deftheorem Def4 defines triv-times SFMASTR2:def 4 :

theorem Th25: :: SFMASTR2:25

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location st b₁ . b₂ <= 0 holds
(IExec (triv-times b₂),b₁) . b₂ = b₁ . b₂

proof end;

theorem Th26: :: SFMASTR2:26

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location st 0 <= b₁ . b₂ holds
(IExec (triv-times b₂),b₁) . b₂ = 0

proof end;

definition

let c₄, c₅ be Int-Location ;
set c₆ = 1 -stRWNotIn {c₄,c₅};
set c₇ = 1 -stNotUsed (times c₄,((AddTo c₅,(1 -stRWNotIn {c₄,c₅})) ';' (swap c₅,(1 -stRWNotIn {c₄,c₅}))));
func Fib-macro c₁,c₂ -> Macro-Instruction equals :: SFMASTR2:def 5
(((((1 -stNotUsed (times a₁,((AddTo a₂,(1 -stRWNotIn {a₁,a₂})) ';' (swap a₂,(1 -stRWNotIn {a₁,a₂}))))) := a₁) ';' (SubFrom a₂,a₂)) ';' ((1 -stRWNotIn {a₁,a₂}) := (intloc 0))) ';' (times a₁,((AddTo a₂,(1 -stRWNotIn {a₁,a₂})) ';' (swap a₂,(1 -stRWNotIn {a₁,a₂}))))) ';' (a₁ := (1 -stNotUsed (times a₁,((AddTo a₂,(1 -stRWNotIn {a₁,a₂})) ';' (swap a₂,(1 -stRWNotIn {a₁,a₂}))))));
correctness ;

end;

:: deftheorem Def5 defines Fib-macro SFMASTR2:def 5 :

theorem Th27: :: SFMASTR2:27

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 (Fib-macro b₂,b₃),b₁) . b₃ = Fib b₄ & (IExec (Fib-macro b₂,b₃),b₁) . b₂ = b₁ . b₂ )

proof end;