:: SFMASTR1 semantic presentation

definition

let c₁ be Instruction of SCM+FSA ;
attr a₁ is good means :Def1: :: SFMASTR1:def 1
Macro a₁ is good;

end;

:: deftheorem Def1 defines good SFMASTR1:def 1 :

registration

let c₁ be read-write Int-Location ;
let c₂ be Int-Location ;
cluster a₁ := a₂ -> good ;
coherence

proof end;

cluster AddTo a₁,a₂ -> good ;
coherence

proof end;

cluster SubFrom a₁,a₂ -> good ;
coherence

proof end;

cluster MultBy a₁,a₂ -> good ;
coherence

proof end;

end;

registration

cluster parahalting good Element of the Instructions of SCM+FSA ;
existence

proof end;

end;

registration

let c₁, c₂ be read-write Int-Location ;
cluster Divide a₁,a₂ -> good ;
coherence

proof end;

end;

registration

let c₁ be Instruction-Location of SCM+FSA ;
cluster goto a₁ -> good ;
coherence

proof end;

end;

registration

let c₁ be Int-Location ;
let c₂ be Instruction-Location of SCM+FSA ;
cluster a₁ =0_goto a₂ -> good ;
coherence

proof end;

cluster a₁ >0_goto a₂ -> good ;
coherence

proof end;

end;

registration

let c₁ be Int-Location ;
let c₂ be FinSeq-Location ;
let c₃ be read-write Int-Location ;
cluster a₃ := a₂,a₁ -> good ;
coherence

proof end;

end;

registration

let c₁ be FinSeq-Location ;
let c₂ be read-write Int-Location ;
cluster a₂ :=len a₁ -> good ;
coherence

proof end;

end;

registration

let c₁ be FinSeq-Location ;
let c₂ be Int-Location ;
cluster a₁ :=<0,...,0> a₂ -> good ;
coherence

proof end;

let c₃ be Int-Location ;
cluster a₁,a₂ := a₃ -> good ;
coherence

proof end;

end;

registration

cluster good Element of the Instructions of SCM+FSA ;
existence

proof end;

end;

registration

let c₁ be good Instruction of SCM+FSA ;
cluster Macro a₁ -> good ;
coherence by Def1;

end;

registration

let c₁, c₂ be good Instruction of SCM+FSA ;
cluster a₁ ';' a₂ -> good ;
coherence

proof end;

end;

registration

let c₁ be good Instruction of SCM+FSA ;
let c₂ be good Macro-Instruction;
cluster a₁ ';' a₂ -> good ;
coherence

proof end;

cluster a₂ ';' a₁ -> good ;
coherence

proof end;

end;

registration

let c₁, c₂ be read-write Int-Location ;
cluster swap a₁,a₂ -> good ;
coherence

proof end;

end;

registration

let c₁ be good Macro-Instruction;
let c₂ be read-write Int-Location ;
cluster Times a₂,a₁ -> good ;
coherence

proof end;

end;

theorem Th1: :: SFMASTR1:1

for b₁ being Int-Location
for b₂ being Macro-Instruction st not b₁ in UsedIntLoc b₂ holds
b₂ does_not_destroy b₁

proof end;

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

theorem Th2: :: SFMASTR1:2

for b₁ being Macro-Instruction holds (b₁ +* (Start-At (insloc 0))) | (Int-Locations \/ FinSeq-Locations ) = {}

proof end;

theorem Th3: :: SFMASTR1:3

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction st b₂ is_halting_on Initialize b₁ & b₂ is_closed_on Initialize b₁ & b₃ is_closed_on IExec b₂,b₁ holds
b₂ ';' b₃ is_closed_on Initialize b₁

proof end;

theorem Th4: :: SFMASTR1:4

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction st b₂ is_halting_on Initialize b₁ & b₃ is_halting_on IExec b₂,b₁ & b₂ is_closed_on Initialize b₁ & b₃ is_closed_on IExec b₂,b₁ holds
b₂ ';' b₃ is_halting_on Initialize b₁

proof end;

theorem Th5: :: SFMASTR1:5

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction st b₂ is_closed_on b₁ & b₂ +* (Start-At (insloc 0)) c= b₁ & b₁ is halting holds
for b₄ being Nat st b₄ <= LifeSpan b₁ holds
(Computation b₁) . b₄,(Computation (b₁ +* (b₂ ';' b₃))) . b₄ equal_outside the Instruction-Locations of SCM+FSA

proof end;

Lemma7: for b₁ being good Macro-Instruction
for b₂ being Macro-Instruction
for b₃ being State of SCM+FSA st b₃ . (intloc 0) = 1 & b₁ is_halting_on b₃ & b₂ is_halting_on IExec b₁,b₃ & b₁ is_closed_on b₃ & b₂ is_closed_on IExec b₁,b₃ & Initialized (b₁ ';' b₂) c= b₃ holds
( IC ((Computation b₃) . ((LifeSpan (b₃ +* b₁)) + 1)) = insloc (card b₁) & ((Computation b₃) . ((LifeSpan (b₃ +* b₁)) + 1)) | (Int-Locations \/ FinSeq-Locations ) = (((Computation (b₃ +* b₁)) . (LifeSpan (b₃ +* b₁))) +* (Initialized b₂)) | (Int-Locations \/ FinSeq-Locations ) & ProgramPart (Relocated b₂,(card b₁)) c= (Computation b₃) . ((LifeSpan (b₃ +* b₁)) + 1) & ((Computation b₃) . ((LifeSpan (b₃ +* b₁)) + 1)) . (intloc 0) = 1 & b₃ is halting & LifeSpan b₃ = ((LifeSpan (b₃ +* b₁)) + 1) + (LifeSpan ((Result (b₃ +* b₁)) +* (Initialized b₂))) & ( b₂ is good implies (Result b₃) . (intloc 0) = 1 ) )

proof end;

theorem Th6: :: SFMASTR1:6

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being good Macro-Instruction st b₃ is_halting_on Initialize b₁ & b₂ is_halting_on IExec b₃,b₁ & b₃ is_closed_on Initialize b₁ & b₂ is_closed_on IExec b₃,b₁ holds
LifeSpan (b₁ +* (Initialized (b₃ ';' b₂))) = ((LifeSpan (b₁ +* (Initialized b₃))) + 1) + (LifeSpan ((Result (b₁ +* (Initialized b₃))) +* (Initialized b₂)))

proof end;

theorem Th7: :: SFMASTR1:7

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being good Macro-Instruction st b₃ is_halting_on Initialize b₁ & b₂ is_halting_on IExec b₃,b₁ & b₃ is_closed_on Initialize b₁ & b₂ is_closed_on IExec b₃,b₁ holds
IExec (b₃ ';' b₂),b₁ = (IExec b₂,(IExec b₃,b₁)) +* (Start-At ((IC (IExec b₂,(IExec b₃,b₁))) + (card b₃)))

proof end;

E10: now

let c₂ be Macro-Instruction;
assume c₂ is parahalting ;
then reconsider c₃ = c₂ as parahalting Macro-Instruction ;
c₃ is paraclosed ;
hence c₂ is paraclosed ;

end;

theorem Th8: :: SFMASTR1:8

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being good Macro-Instruction
for b₄ being Int-Location st ( b₃ is parahalting or ( b₃ is_halting_on Initialize b₁ & b₃ is_closed_on Initialize b₁ ) ) & ( b₂ is parahalting or ( b₂ is_halting_on IExec b₃,b₁ & b₂ is_closed_on IExec b₃,b₁ ) ) holds
(IExec (b₃ ';' b₂),b₁) . b₄ = (IExec b₂,(IExec b₃,b₁)) . b₄

proof end;

theorem Th9: :: SFMASTR1:9

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being good Macro-Instruction
for b₄ being FinSeq-Location st ( b₃ is parahalting or ( b₃ is_halting_on Initialize b₁ & b₃ is_closed_on Initialize b₁ ) ) & ( b₂ is parahalting or ( b₂ is_halting_on IExec b₃,b₁ & b₂ is_closed_on IExec b₃,b₁ ) ) holds
(IExec (b₃ ';' b₂),b₁) . b₄ = (IExec b₂,(IExec b₃,b₁)) . b₄

proof end;

theorem Th10: :: SFMASTR1:10

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being good Macro-Instruction st ( b₃ is parahalting or ( b₃ is_halting_on Initialize b₁ & b₃ is_closed_on Initialize b₁ ) ) & ( b₂ is parahalting or ( b₂ is_halting_on IExec b₃,b₁ & b₂ is_closed_on IExec b₃,b₁ ) ) holds
(IExec (b₃ ';' b₂),b₁) | (Int-Locations \/ FinSeq-Locations ) = (IExec b₂,(IExec b₃,b₁)) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th11: :: SFMASTR1:11

for b₁ being State of SCM+FSA
for b₂ being good Macro-Instruction st ( b₂ is parahalting or ( b₂ is_closed_on Initialize b₁ & b₂ is_halting_on Initialize b₁ ) ) holds
(Initialize (IExec b₂,b₁)) | (Int-Locations \/ FinSeq-Locations ) = (IExec b₂,b₁) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th12: :: SFMASTR1:12

for b₁ being State of SCM+FSA
for b₂ being good Macro-Instruction
for b₃ being parahalting Instruction of SCM+FSA
for b₄ being Int-Location st ( b₂ is parahalting or ( b₂ is_halting_on Initialize b₁ & b₂ is_closed_on Initialize b₁ ) ) holds
(IExec (b₂ ';' b₃),b₁) . b₄ = (Exec b₃,(IExec b₂,b₁)) . b₄

proof end;

theorem Th13: :: SFMASTR1:13

for b₁ being State of SCM+FSA
for b₂ being good Macro-Instruction
for b₃ being parahalting Instruction of SCM+FSA
for b₄ being FinSeq-Location st ( b₂ is parahalting or ( b₂ is_halting_on Initialize b₁ & b₂ is_closed_on Initialize b₁ ) ) holds
(IExec (b₂ ';' b₃),b₁) . b₄ = (Exec b₃,(IExec b₂,b₁)) . b₄

proof end;

theorem Th14: :: SFMASTR1:14

for b₁ being State of SCM+FSA
for b₂ being good Macro-Instruction
for b₃ being parahalting Instruction of SCM+FSA st ( b₂ is parahalting or ( b₂ is_halting_on Initialize b₁ & b₂ is_closed_on Initialize b₁ ) ) holds
(IExec (b₂ ';' b₃),b₁) | (Int-Locations \/ FinSeq-Locations ) = (Exec b₃,(IExec b₂,b₁)) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th15: :: SFMASTR1:15

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being parahalting good Instruction of SCM+FSA
for b₄ being Int-Location st ( b₂ is parahalting or ( b₂ is_halting_on Exec b₃,(Initialize b₁) & b₂ is_closed_on Exec b₃,(Initialize b₁) ) ) holds
(IExec (b₃ ';' b₂),b₁) . b₄ = (IExec b₂,(Exec b₃,(Initialize b₁))) . b₄

proof end;

theorem Th16: :: SFMASTR1:16

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being parahalting good Instruction of SCM+FSA
for b₄ being FinSeq-Location st ( b₂ is parahalting or ( b₂ is_halting_on Exec b₃,(Initialize b₁) & b₂ is_closed_on Exec b₃,(Initialize b₁) ) ) holds
(IExec (b₃ ';' b₂),b₁) . b₄ = (IExec b₂,(Exec b₃,(Initialize b₁))) . b₄

proof end;

theorem Th17: :: SFMASTR1:17

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being parahalting good Instruction of SCM+FSA st ( b₂ is parahalting or ( b₂ is_halting_on Exec b₃,(Initialize b₁) & b₂ is_closed_on Exec b₃,(Initialize b₁) ) ) holds
(IExec (b₃ ';' b₂),b₁) | (Int-Locations \/ FinSeq-Locations ) = (IExec b₂,(Exec b₃,(Initialize b₁))) | (Int-Locations \/ FinSeq-Locations )

proof end;

definition

let c₂ be Int-Location ;
redefine func { as {c₁} -> Subset of Int-Locations ;
coherence

proof end;

let c₃ be Int-Location ;
redefine func { as {c₁,c₂} -> Subset of Int-Locations ;
coherence

proof end;

let c₄ be Int-Location ;
redefine func { as {c₁,c₂,c₃} -> Subset of Int-Locations ;
coherence

proof end;

let c₅ be Int-Location ;
redefine func { as {c₁,c₂,c₃,c₄} -> Subset of Int-Locations ;
coherence

proof end;

end;

Lemma18: for b₁ being set st not b₁ is finite holds
not b₁ is empty

proof end;

definition

let c₂ be finite Subset of Int-Locations ;
func RWNotIn-seq c₁ -> Function of NAT , bool NAT means :Def2: :: SFMASTR1:def 2
( a₂ . 0 = { b₁ where B is Nat : ( not intloc b₁ in a₁ & b₁ <> 0 ) } & ( for b₁ being Nat
for b₂ being non empty Subset of NAT st a₂ . b₁ = b₂ holds
a₂ . (b₁ + 1) = b₂ \ {(min b₂)} ) & ( for b₁ being Nat holds not a₂ . b₁ is finite ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines RWNotIn-seq SFMASTR1:def 2 :

registration

let c₂ be finite Subset of Int-Locations ;
let c₃ be Nat;
cluster (RWNotIn-seq a₁) . a₂ -> non empty ;
coherence by Def2;

end;

theorem Th18: :: SFMASTR1:18

for b₁ being finite Subset of Int-Locations
for b₂ being Nat holds
( not 0 in (RWNotIn-seq b₁) . b₂ & ( for b₃ being Nat st b₃ in (RWNotIn-seq b₁) . b₂ holds
not intloc b₃ in b₁ ) )

proof end;

theorem Th19: :: SFMASTR1:19

for b₁ being finite Subset of Int-Locations
for b₂ being Nat holds min ((RWNotIn-seq b₁) . b₂) < min ((RWNotIn-seq b₁) . (b₂ + 1))

proof end;

theorem Th20: :: SFMASTR1:20

for b₁ being finite Subset of Int-Locations
for b₂, b₃ being Nat st b₂ < b₃ holds
min ((RWNotIn-seq b₁) . b₂) < min ((RWNotIn-seq b₁) . b₃)

proof end;

definition

let c₂ be Nat;
let c₃ be finite Subset of Int-Locations ;
func c₁ -thRWNotIn c₂ -> Int-Location equals :: SFMASTR1:def 3
intloc (min ((RWNotIn-seq a₂) . a₁));
correctness ;

end;

:: deftheorem Def3 defines -thRWNotIn SFMASTR1:def 3 :

notation

let c₂ be Nat;
let c₃ be finite Subset of Int-Locations ;
synonym c₁ -stRWNotIn c₂ for c₁ -thRWNotIn c₂;
synonym c₁ -ndRWNotIn c₂ for c₁ -thRWNotIn c₂;
synonym c₁ -rdRWNotIn c₂ for c₁ -thRWNotIn c₂;

end;

registration

let c₂ be Nat;
let c₃ be finite Subset of Int-Locations ;
cluster a₁ -thRWNotIn a₂ -> read-write ;
coherence

proof end;

end;

theorem Th21: :: SFMASTR1:21

for b₁ being finite Subset of Int-Locations
for b₂ being Nat holds not b₂ -thRWNotIn b₁ in b₁

proof end;

theorem Th22: :: SFMASTR1:22

for b₁ being finite Subset of Int-Locations
for b₂, b₃ being Nat st b₂ <> b₃ holds
b₂ -thRWNotIn b₁ <> b₃ -thRWNotIn b₁

proof end;

definition

let c₂ be Nat;
let c₃ be programmed FinPartState of SCM+FSA ;
func c₁ -thNotUsed c₂ -> Int-Location equals :: SFMASTR1:def 4
a₁ -thRWNotIn (UsedIntLoc a₂);
correctness ;

end;

:: deftheorem Def4 defines -thNotUsed SFMASTR1:def 4 :

notation

let c₂ be Nat;
let c₃ be programmed FinPartState of SCM+FSA ;
synonym c₁ -stNotUsed c₂ for c₁ -thNotUsed c₂;
synonym c₁ -ndNotUsed c₂ for c₁ -thNotUsed c₂;
synonym c₁ -rdNotUsed c₂ for c₁ -thNotUsed c₂;

end;

registration

let c₂ be Nat;
let c₃ be programmed FinPartState of SCM+FSA ;
cluster a₁ -thNotUsed a₂ -> read-write ;
coherence ;

end;

theorem Th23: :: SFMASTR1:23

for b₁, b₂ being Int-Location holds
( b₁ in UsedIntLoc (swap b₁,b₂) & b₂ in UsedIntLoc (swap b₁,b₂) )

proof end;

definition

let c₂, c₃ be Int-Location ;
set c₄ = 1 -stRWNotIn {c₂,c₃};
set c₅ = 1 -stRWNotIn (UsedIntLoc (swap c₃,(1 -stRWNotIn {c₂,c₃})));
set c₆ = 2 -ndRWNotIn (UsedIntLoc (swap c₃,(1 -stRWNotIn {c₂,c₃})));
func Fib_macro c₁,c₂ -> Macro-Instruction equals :: SFMASTR1:def 5
((((((2 -ndRWNotIn (UsedIntLoc (swap a₂,(1 -stRWNotIn {a₁,a₂})))) := a₁) ';' (SubFrom a₂,a₂)) ';' ((1 -stRWNotIn {a₁,a₂}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap a₂,(1 -stRWNotIn {a₁,a₂})))) := (2 -ndRWNotIn (UsedIntLoc (swap a₂,(1 -stRWNotIn {a₁,a₂})))))) ';' (Times (1 -stRWNotIn (UsedIntLoc (swap a₂,(1 -stRWNotIn {a₁,a₂})))),((AddTo a₂,(1 -stRWNotIn {a₁,a₂})) ';' (swap a₂,(1 -stRWNotIn {a₁,a₂}))))) ';' (a₁ := (2 -ndRWNotIn (UsedIntLoc (swap a₂,(1 -stRWNotIn {a₁,a₂})))));
correctness ;

end;

:: deftheorem Def5 defines Fib_macro SFMASTR1:def 5 :

theorem Th24: :: SFMASTR1:24

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;