:: On the Composition of non-parahalting Macro Instructions
:: by Piotr Rudnicki
::
:: Received June 3, 1998
:: Copyright (c) 1998-2011 Association of Mizar Users

begin

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 :
for i being Instruction of SCM+FSA holds
( i is good iff Macro i is good );

registration

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

proof end;

cluster AddTo (a,b) -> good ;
coherence
AddTo (a,b) is good

proof end;

cluster SubFrom (a,b) -> good ;
coherence
SubFrom (a,b) is good

proof end;

cluster MultBy (a,b) -> good ;
coherence
MultBy (a,b) is good

proof end;

end;

registration

cluster parahalting with_explicit_jumps IC-relocable Exec-preserving good Element of the Instructions of SCM+FSA;
existence
ex b₁ being Instruction of SCM+FSA st
( b₁ is good & b₁ is parahalting )

proof end;

end;

registration

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

proof end;

end;

registration

let l be Element of NAT ;
cluster goto l -> good ;
coherence
goto l is good

proof end;

end;

registration

let a be Int-Location ;
let l be Element of NAT ;
cluster a =0_goto l -> good ;
coherence
a =0_goto l is good

proof end;

cluster a >0_goto l -> good ;
coherence
a >0_goto l is good

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
b := (f,a) is good

proof end;

end;

registration

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

proof end;

end;

registration

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

proof end;

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

proof end;

end;

registration

cluster with_explicit_jumps IC-relocable Exec-preserving good Element of the Instructions of SCM+FSA;
existence
ex b₁ being Instruction of SCM+FSA st b₁ is good

proof end;

end;

registration

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

end;

registration

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

end;

registration

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

end;

registration

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

proof end;

end;

registration

let I be good Program of SCM+FSA;
let a be read-write Int-Location ;
cluster Times (a,I) -> good ;
coherence
Times (a,I) is good

proof end;

end;

theorem Th1: :: SFMASTR1:1

for a being Int-Location
for I being Program of SCM+FSA st not a in UsedIntLoc I holds
not I destroys a

proof end;

begin

set D = Data-Locations SCM+FSA;

set SAt = Start-At (0,SCM+FSA);

theorem Th2: :: SFMASTR1:2

DataPart (Start-At (0,SCM+FSA)) = {}

proof end;

theorem Th3: :: SFMASTR1:3

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for S being State of SCM+FSA
for I, J being Program of SCM+FSA st I is_halting_on Initialized S,P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P holds
I ';' J is_closed_on Initialized S,P

proof end;

theorem Th4: :: SFMASTR1:4

for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for S being State of SCM+FSA
for I, J being Program of SCM+FSA st I is_halting_on Initialized S,P & J is_halting_on IExec (I,P,S),P & I is_closed_on Initialized S,P & J is_closed_on IExec (I,P,S),P holds
I ';' J is_halting_on Initialized S,P

proof end;

theorem Th5: :: SFMASTR1:5

for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I, J being Program of SCM+FSA st I is_closed_on s,p & Start-At (0,SCM+FSA) c= s & I c= p & p halts_on s holds
for m being Element of NAT st m <= LifeSpan (p,s) holds
NPP (Comput (p,s,m)) = NPP (Comput ((p +* (I ';' J)),s,m))

proof end;

LmY: for I being Program of SCM+FSA holds
( (Initialize ((intloc 0) .--> 1)) . (intloc 0) = 1 & (Initialize ((intloc 0) .--> 1)) . (IC ) = 0 )

proof end;

Lm1: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being good Program of SCM+FSA
for J being Program of SCM+FSA
for s being State of SCM+FSA st s . (intloc 0) = 1 & I is_halting_on s,p & J is_halting_on IExec (I,p,s),p & I is_closed_on s,p & J is_closed_on IExec (I,p,s),p & Initialize ((intloc 0) .--> 1) c= s & I ';' J c= p holds
( IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I & DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) & Reloc (J,(card I)) c= p & (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) . (intloc 0) = 1 & p halts_on s & LifeSpan (p,s) = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Result ((p +* I),s))))) & ( J is good implies (Result (p,s)) . (intloc 0) = 1 ) )

proof end;

theorem Th6: :: SFMASTR1:6

for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p holds
LifeSpan ((p +* (Ig ';' J)),(s +* (Initialize ((intloc 0) .--> 1)))) = ((LifeSpan ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) + 1) + (LifeSpan (((p +* Ig) +* J),((Result ((p +* Ig),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Initialize ((intloc 0) .--> 1)))))

proof end;

theorem Th7: :: SFMASTR1:7

for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p & Ig is_closed_on Initialized s,p & J is_closed_on IExec (Ig,p,s),p holds
IExec ((Ig ';' J),p,s) = (IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))

proof end;

theorem Th8: :: SFMASTR1:8

for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA
for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
(IExec ((Ig ';' J),p,s)) . a = (IExec (J,p,(IExec (Ig,p,s)))) . a

proof end;

theorem Th9: :: SFMASTR1:9

for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA
for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
(IExec ((Ig ';' J),p,s)) . f = (IExec (J,p,(IExec (Ig,p,s)))) . f

proof end;

theorem :: SFMASTR1:10

for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for J being Program of SCM+FSA
for Ig being good Program of SCM+FSA st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) & ( J is parahalting or ( J is_halting_on IExec (Ig,p,s),p & J is_closed_on IExec (Ig,p,s),p ) ) holds
DataPart (IExec ((Ig ';' J),p,s)) = DataPart (IExec (J,p,(IExec (Ig,p,s))))

proof end;

theorem Th11: :: SFMASTR1:11

for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for Ig being good Program of SCM+FSA st ( Ig is parahalting or ( Ig is_closed_on Initialized s,p & Ig is_halting_on Initialized s,p ) ) holds
DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s))

proof end;

theorem Th12: :: SFMASTR1:12

for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for Ig being good Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA
for a being Int-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
(IExec ((Ig ';' j),p,s)) . a = (Exec (j,(IExec (Ig,p,s)))) . a

proof end;

theorem Th13: :: SFMASTR1:13

for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for Ig being good Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA
for f being FinSeq-Location st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
(IExec ((Ig ';' j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f

proof end;

theorem :: SFMASTR1:14

for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for Ig being good Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA st ( Ig is parahalting or ( Ig is_halting_on Initialized s,p & Ig is_closed_on Initialized s,p ) ) holds
DataPart (IExec ((Ig ';' j),p,s)) = DataPart (Exec (j,(IExec (Ig,p,s))))

proof end;

theorem :: SFMASTR1:15

canceled;

theorem :: SFMASTR1:16

canceled;

theorem :: SFMASTR1:17

canceled;

begin

definition

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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 Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Element of NAT
for sn being non empty Subset of NAT st it . i = sn holds
it . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds not it . i is finite ) );
existence
ex b₁ being Function of NAT,(bool NAT) st
( b₁ . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Element of NAT
for sn being non empty Subset of NAT st b₁ . i = sn holds
b₁ . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds not b₁ . i is finite ) )

proof end;

uniqueness
for b₁, b₂ being Function of NAT,(bool NAT) st b₁ . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Element of NAT
for sn being non empty Subset of NAT st b₁ . i = sn holds
b₁ . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds not b₁ . i is finite ) & b₂ . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Element of NAT
for sn being non empty Subset of NAT st b₂ . i = sn holds
b₂ . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds not b₂ . i is finite ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines RWNotIn-seq SFMASTR1:def 2 :
for L being finite Subset of Int-Locations
for b₂ being Function of NAT,(bool NAT) holds
( b₂ = RWNotIn-seq L iff ( b₂ . 0 = { k where k is Element of NAT : ( not intloc k in L & k <> 0 ) } & ( for i being Element of NAT
for sn being non empty Subset of NAT st b₂ . i = sn holds
b₂ . (i + 1) = sn \ {(min sn)} ) & ( for i being Element of NAT holds not b₂ . i is finite ) ) );

registration

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

end;

theorem Th18: :: SFMASTR1:18

for L being finite Subset of Int-Locations
for n being Element of NAT holds
( not 0 in (RWNotIn-seq L) . n & ( for m being Element of 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 Element of 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 Element of NAT st n < m holds
min ((RWNotIn-seq L) . n) < min ((RWNotIn-seq L) . m)

proof end;

definition

let n be Element of 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
coherence
intloc (min ((RWNotIn-seq L) . n)) is Int-Location ;
;

end;

:: deftheorem defines -thRWNotIn SFMASTR1:def 3 :
for n being Element of NAT
for L being finite Subset of Int-Locations holds n -thRWNotIn L = intloc (min ((RWNotIn-seq L) . n));

notation

let n be Element of 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 Element of NAT ;
let L be finite Subset of Int-Locations;
cluster n -thRWNotIn L -> read-write ;
coherence
not n -thRWNotIn L is read-only

proof end;

end;

theorem Th21: :: SFMASTR1:21

for L being finite Subset of Int-Locations
for n being Element of 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 Element of NAT st n <> m holds
n -thRWNotIn L <> m -thRWNotIn L

proof end;

definition

let n be Element of NAT ;
let p be preProgram of SCM+FSA;
func n -thNotUsed p -> Int-Location equals :: SFMASTR1:def 4
n -thRWNotIn (UsedIntLoc p);
correctness
coherence
n -thRWNotIn (UsedIntLoc p) is Int-Location ;
;

end;

:: deftheorem defines -thNotUsed SFMASTR1:def 4 :
for n being Element of NAT
for p being preProgram of SCM+FSA holds n -thNotUsed p = n -thRWNotIn (UsedIntLoc p);

notation

let n be Element of NAT ;
let p be preProgram 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 Element of NAT ;
let p be preProgram of SCM+FSA;
cluster n -thNotUsed p -> read-write ;
coherence
not n -thNotUsed p is read-only ;

end;

begin

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 ;
func Fib_macro (N,result) -> Program of SCM+FSA 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
coherence
((((((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})))))) is Program of SCM+FSA;
;

end;

:: deftheorem defines Fib_macro SFMASTR1:def 5 :
for N, result being Int-Location holds Fib_macro (N,result) = ((((((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}))))));

theorem :: SFMASTR1:24

for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 ((Fib_macro (N,result)),p,s)) . result = Fib n & (IExec ((Fib_macro (N,result)),p,s)) . N = s . N )

proof end;

theorem :: SFMASTR1:25

for I being Program of SCM+FSA holds intloc 0 in dom (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:86;

theorem :: SFMASTR1:26

for I being Program of SCM+FSA holds
( (Initialize ((intloc 0) .--> 1)) . (intloc 0) = 1 & (Initialize ((intloc 0) .--> 1)) . (IC ) = 0 ) by LmY;