:: SFMASTR1 semantic presentation

definition

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

end;

:: deftheorem Def1 defines good SFMASTR1:def 1 :

registration

let a be read-write Int-Location ;
let b be Int-Location ;
cluster a := b -> good ;
coherence

proof end;

cluster AddTo a,b -> good ;
coherence

proof end;

cluster SubFrom a,b -> good ;
coherence

proof end;

cluster MultBy a,b -> good ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

let a, b be read-write Int-Location ;
cluster Divide a,b -> good ;
coherence

proof end;

end;

registration

let l be Instruction-Location of SCM+FSA ;
cluster goto l -> good ;
coherence

proof end;

end;

registration

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

proof end;

cluster a >0_goto l -> good ;
coherence

proof end;

end;

registration

let a be Int-Location ;
let f be FinSeq-Location ;
let b be read-write Int-Location ;
cluster b := f,a -> good ;
coherence

proof end;

end;

registration

let f be FinSeq-Location ;
let b be read-write Int-Location ;
cluster b :=len f -> good ;
coherence

proof end;

end;

registration

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

proof end;

let b be Int-Location ;
cluster f,a := b -> good ;
coherence

proof end;

end;

registration

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

proof end;

end;

registration

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

end;

registration

let i, j be good Instruction of SCM+FSA ;
cluster i ';' j -> good ;
coherence

proof end;

end;

registration

let i be good Instruction of SCM+FSA ;
let I be good Macro-Instruction;
cluster i ';' I -> good ;
coherence

proof end;

cluster I ';' i -> good ;
coherence

proof end;

end;

registration

let a, b be read-write Int-Location ;
cluster swap a,b -> good ;
coherence

proof end;

end;

registration

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

proof end;

end;

theorem Th1: :: SFMASTR1:1

for a being Int-Location
for I being Macro-Instruction st not a in UsedIntLoc I holds
I does_not_destroy a

proof end;

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

theorem Th2: :: SFMASTR1:2

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

proof end;

theorem Th3: :: SFMASTR1:3

for S being State of SCM+FSA
for I, J being Macro-Instruction st I is_halting_on Initialize S & I is_closed_on Initialize S & J is_closed_on IExec I,S holds
I ';' J is_closed_on Initialize S

proof end;

theorem Th4: :: SFMASTR1:4

for S being State of SCM+FSA
for I, J being Macro-Instruction st I is_halting_on Initialize S & J is_halting_on IExec I,S & I is_closed_on Initialize S & J is_closed_on IExec I,S holds
I ';' J is_halting_on Initialize S

proof end;

theorem Th5: :: SFMASTR1:5

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

proof end;

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

proof end;

theorem Th6: :: SFMASTR1:6

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

proof end;

theorem Th7: :: SFMASTR1:7

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

proof end;

Lm2: now

let I be Macro-Instruction; :: thesis:
assume I is parahalting ; :: thesis:
then reconsider I' = I as parahalting Macro-Instruction ;
I' is paraclosed ;
hence I is paraclosed ; :: thesis:

end;

theorem Th8: :: SFMASTR1:8

for s being State of SCM+FSA
for J being Macro-Instruction
for Ig being good Macro-Instruction
for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialize s & Ig is_closed_on Initialize s ) ) & ( J is parahalting or ( J is_halting_on IExec Ig,s & J is_closed_on IExec Ig,s ) ) holds
(IExec (Ig ';' J),s) . a = (IExec J,(IExec Ig,s)) . a

proof end;

theorem Th9: :: SFMASTR1:9

for s being State of SCM+FSA
for J being Macro-Instruction
for Ig being good Macro-Instruction
for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialize s & Ig is_closed_on Initialize s ) ) & ( J is parahalting or ( J is_halting_on IExec Ig,s & J is_closed_on IExec Ig,s ) ) holds
(IExec (Ig ';' J),s) . f = (IExec J,(IExec Ig,s)) . f

proof end;

theorem :: SFMASTR1:10

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

proof end;

theorem Th11: :: SFMASTR1:11

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

proof end;

theorem Th12: :: SFMASTR1:12

for s being State of SCM+FSA
for Ig being good Macro-Instruction
for j being parahalting Instruction of SCM+FSA
for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialize s & Ig is_closed_on Initialize s ) ) holds
(IExec (Ig ';' j),s) . a = (Exec j,(IExec Ig,s)) . a

proof end;

theorem Th13: :: SFMASTR1:13

for s being State of SCM+FSA
for Ig being good Macro-Instruction
for j being parahalting Instruction of SCM+FSA
for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialize s & Ig is_closed_on Initialize s ) ) holds
(IExec (Ig ';' j),s) . f = (Exec j,(IExec Ig,s)) . f

proof end;

theorem :: SFMASTR1:14

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

proof end;

theorem Th15: :: SFMASTR1:15

for s being State of SCM+FSA
for J being Macro-Instruction
for i being parahalting good Instruction of SCM+FSA
for a being Int-Location st ( J is parahalting or ( J is_halting_on Exec i,(Initialize s) & J is_closed_on Exec i,(Initialize s) ) ) holds
(IExec (i ';' J),s) . a = (IExec J,(Exec i,(Initialize s))) . a

proof end;

theorem Th16: :: SFMASTR1:16

for s being State of SCM+FSA
for J being Macro-Instruction
for i being parahalting good Instruction of SCM+FSA
for f being FinSeq-Location st ( J is parahalting or ( J is_halting_on Exec i,(Initialize s) & J is_closed_on Exec i,(Initialize s) ) ) holds
(IExec (i ';' J),s) . f = (IExec J,(Exec i,(Initialize s))) . f

proof end;

theorem :: SFMASTR1:17

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

proof end;

definition

let d be Int-Location ;
:: original: {
redefine func {d} -> Subset of Int-Locations ;
coherence

proof end;

let e be Int-Location ;
:: original: {
redefine func {d,e} -> Subset of Int-Locations ;
coherence

proof end;

let f be Int-Location ;
:: original: {
redefine func {d,e,f} -> Subset of Int-Locations ;
coherence

proof end;

let g be Int-Location ;
:: original: {
redefine func {d,e,f,g} -> Subset of Int-Locations ;
coherence

proof end;

end;

Lm3: for X being set st not X is finite holds
not X is empty

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

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

registration

let L be finite Subset of Int-Locations ;
let n be Nat;
cluster (RWNotIn-seq L) . n -> non empty ;
coherence by Def2;

end;

theorem Th18: :: SFMASTR1:18

for L being finite Subset of Int-Locations
for n being Nat holds
( not 0 in (RWNotIn-seq L) . n & ( for m being Nat st m in (RWNotIn-seq L) . n holds
not intloc m in L ) )

proof end;

theorem Th19: :: SFMASTR1:19

for L being finite Subset of Int-Locations
for n being Nat holds min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . (n + 1))

proof end;

theorem Th20: :: SFMASTR1:20

for L being finite Subset of Int-Locations
for n, m being Nat st n < m holds
min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m)

proof end;

definition

let n be Nat;
let L be finite Subset of Int-Locations ;
func n -thRWNotIn L -> Int-Location equals :: SFMASTR1:def 3
intloc (min ((RWNotIn-seq L) . n));
correctness ;

end;

:: deftheorem defines -thRWNotIn SFMASTR1:def 3 :

notation

let n be Nat;
let L be finite Subset of Int-Locations ;
synonym n -stRWNotIn L for n -thRWNotIn L;
synonym n -ndRWNotIn L for n -thRWNotIn L;
synonym n -rdRWNotIn L for n -thRWNotIn L;

end;

registration

let n be Nat;
let L be finite Subset of Int-Locations ;
cluster n -thRWNotIn L -> read-write ;
coherence

proof end;

end;

theorem Th21: :: SFMASTR1:21

for L being finite Subset of Int-Locations
for n being Nat holds not n -thRWNotIn L in L

proof end;

theorem Th22: :: SFMASTR1:22

for L being finite Subset of Int-Locations
for n, m being Nat st n <> m holds
n -thRWNotIn L <> m -thRWNotIn L

proof end;

definition

let n be Nat;
let p be programmed FinPartState of SCM+FSA ;
func n -thNotUsed p -> Int-Location equals :: SFMASTR1:def 4
n -thRWNotIn (UsedIntLoc p);
correctness ;

end;

:: deftheorem defines -thNotUsed SFMASTR1:def 4 :

notation

let n be Nat;
let p be programmed FinPartState of SCM+FSA ;
synonym n -stNotUsed p for n -thNotUsed p;
synonym n -ndNotUsed p for n -thNotUsed p;
synonym n -rdNotUsed p for n -thNotUsed p;

end;

registration

let n be Nat;
let p be programmed FinPartState of SCM+FSA ;
cluster n -thNotUsed p -> read-write ;
coherence ;

end;

theorem Th23: :: SFMASTR1:23

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

proof end;

definition

let N, result be Int-Location ;
set next = 1 -stRWNotIn {N,result};
set aux = 1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})));
set Nsave = 2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})));
func Fib_macro N,result -> Macro-Instruction equals :: SFMASTR1:def 5
((((((2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := N) ';' (SubFrom result,result)) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))) := (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))))) ';' (Times (1 -stRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))),((AddTo result,(1 -stRWNotIn {N,result})) ';' (swap result,(1 -stRWNotIn {N,result}))))) ';' (N := (2 -ndRWNotIn (UsedIntLoc (swap result,(1 -stRWNotIn {N,result})))));
correctness ;

end;

:: deftheorem defines Fib_macro SFMASTR1:def 5 :

theorem :: SFMASTR1:24

for s being State of SCM+FSA
for N, result being read-write Int-Location st N <> result holds
for n being Nat st n = s . N holds
( (IExec (Fib_macro N,result),s) . result = Fib n & (IExec (Fib_macro N,result),s) . N = s . N )

proof end;