:: On the compositions of macro instructions, Part III
:: by Noriko Asamoto , Yatsuka Nakamura , Piotr Rudnicki and Andrzej Trybulec
::
:: Received July 22, 1996
:: Copyright (c) 1996-2011 Association of Mizar Users

begin

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

theorem :: SCMFSA6C:1

for a being Int-Location
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds (IExec ((I ';' J),P,s)) . a = (IExec (J,P,(IExec (I,P,s)))) . a

proof end;

theorem :: SCMFSA6C:2

for f being FinSeq-Location
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA holds (IExec ((I ';' J),P,s)) . f = (IExec (J,P,(IExec (I,P,s)))) . f

proof end;

begin

definition

let i be Instruction of SCM+FSA;
attr i is parahalting means :Def1: :: SCMFSA6C:def 1
Macro i is parahalting ;
attr i is keeping_0 means :Def2: :: SCMFSA6C:def 2
Macro i is keeping_0 ;

end;

:: deftheorem Def1 defines parahalting SCMFSA6C:def 1 :
for i being Instruction of SCM+FSA holds
( i is parahalting iff Macro i is parahalting );

:: deftheorem Def2 defines keeping_0 SCMFSA6C:def 2 :
for i being Instruction of SCM+FSA holds
( i is keeping_0 iff Macro i is keeping_0 );

Lm1: Macro (halt SCM+FSA) is parahalting

proof end;

Lm2: Macro (halt SCM+FSA) is keeping_0

proof end;

registration

cluster halt SCM+FSA -> parahalting keeping_0 ;
coherence
( halt SCM+FSA is keeping_0 & halt SCM+FSA is parahalting )

proof end;

end;

registration

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

proof end;

end;

registration

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

end;

registration

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

end;

registration

let a, b be Int-Location ;
cluster a := b -> parahalting ;
coherence
a := b is parahalting

proof end;

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

proof end;

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

proof end;

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

proof end;

cluster Divide (a,b) -> parahalting ;
coherence
Divide (a,b) is parahalting

proof end;

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

proof end;

cluster (f,a) := b -> parahalting keeping_0 ;
coherence
( (f,a) := b is parahalting & (f,a) := b is keeping_0 )

proof end;

end;

registration

let a be Int-Location ;
let f be FinSeq-Location ;
cluster a :=len f -> parahalting ;
coherence
a :=len f is parahalting

proof end;

cluster f :=<0,...,0> a -> parahalting keeping_0 ;
coherence
( f :=<0,...,0> a is parahalting & f :=<0,...,0> a is keeping_0 )

proof end;

end;

registration

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

proof end;

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

proof end;

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

proof end;

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

proof end;

end;

registration

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

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

proof end;

end;

registration

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

proof end;

end;

registration

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

end;

registration

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

end;

registration

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

end;

registration

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

end;

registration

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

end;

registration

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

end;

begin

registration

let s be State of SCM+FSA;
cluster Initialized s -> total ;
coherence
Initialized s is total

proof end;

end;

theorem Th3: :: SCMFSA6C:3

for s being State of SCM+FSA holds
( IC (Initialized s) = 0 & (Initialized s) . (intloc 0) = 1 & ( for a being read-write Int-Location holds (Initialized s) . a = s . a ) & ( for f being FinSeq-Location holds (Initialized s) . f = s . f ) & ( for l being Element of NAT holds (Initialized s) . l = s . l ) )

proof end;

theorem :: SCMFSA6C:4

canceled;

theorem Th5: :: SCMFSA6C:5

for i being Instruction of SCM+FSA
for s1, s2 being State of SCM+FSA st DataPart s1 = DataPart s2 holds
DataPart (Exec (i,s1)) = DataPart (Exec (i,s2))

proof end;

Lm3: now

set IF = Data-Locations SCM+FSA;
let I be parahalting keeping_0 Program of SCM+FSA; :: thesis: for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))
let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))
set IE = IExec (I,P,s);

now

A1: dom (Initialized (IExec (I,P,s))) = the carrier of SCM+FSA by PARTFUN1:def 4;
A2: the carrier of SCM+FSA = ({(IC )} \/ (Data-Locations SCM+FSA)) \/ NAT by COMPOS_1:160
.= ({(IC )} \/ NAT) \/ (Data-Locations SCM+FSA) by XBOOLE_1:4 ;
A3: dom (IExec (I,P,s)) = the carrier of SCM+FSA by PARTFUN1:def 4;
hence dom (DataPart (Initialized (IExec (I,P,s)))) = (dom (IExec (I,P,s))) /\ (Data-Locations SCM+FSA) by A1, RELAT_1:90; :: thesis: for x being set st x in dom (DataPart (Initialized (IExec (I,P,s)))) holds
(DataPart (Initialized (IExec (I,P,s)))) . b₂ = (IExec (I,P,s)) . b₂
then A4: dom (DataPart (Initialized (IExec (I,P,s)))) = Data-Locations SCM+FSA by A3, XBOOLE_1:21, A2;
let x be set ; :: thesis: ( x in dom (DataPart (Initialized (IExec (I,P,s)))) implies (DataPart (Initialized (IExec (I,P,s)))) . b₁ = (IExec (I,P,s)) . b₁ )
assume A5: x in dom (DataPart (Initialized (IExec (I,P,s)))) ; :: thesis: (DataPart (Initialized (IExec (I,P,s)))) . b₁ = (IExec (I,P,s)) . b₁

per cases ( x in Int-Locations or x in FinSeq-Locations ) by A5, A4, XBOOLE_0:def 3, SCMFSA_2:127;

suppose x in Int-Locations ; :: thesis: (DataPart (Initialized (IExec (I,P,s)))) . b₁ = (IExec (I,P,s)) . b₁

then reconsider x9 = x as Int-Location by SCMFSA_2:11;

hereby :: thesis: verum

per cases ( not x9 is read-only or x9 is read-only ) ;

suppose A6: not x9 is read-only ; :: thesis: (DataPart (Initialized (IExec (I,P,s)))) . x = (IExec (I,P,s)) . x

thus (DataPart (Initialized (IExec (I,P,s)))) . x = (Initialized (IExec (I,P,s))) . x by A5, A4, FUNCT_1:72
.= (IExec (I,P,s)) . x by A6, Th3 ; :: thesis: verum

end;

suppose x9 is read-only ; :: thesis: (DataPart (Initialized (IExec (I,P,s)))) . x = (IExec (I,P,s)) . x

then A7: x9 = intloc 0 by SF_MASTR:def 5;
thus (DataPart (Initialized (IExec (I,P,s)))) . x = (Initialized (IExec (I,P,s))) . x9 by A5, A4, FUNCT_1:72
.= 1 by A7, Th3
.= (IExec (I,P,s)) . x by A7, SCMFSA6B:35 ; :: thesis: verum

end;

end;

end;

end;

suppose x in FinSeq-Locations ; :: thesis: (DataPart (Initialized (IExec (I,P,s)))) . b₁ = (IExec (I,P,s)) . b₁

then reconsider x9 = x as FinSeq-Location by SCMFSA_2:12;
thus (DataPart (Initialized (IExec (I,P,s)))) . x = (Initialized (IExec (I,P,s))) . x9 by A5, A4, FUNCT_1:72
.= (IExec (I,P,s)) . x by Th3 ; :: thesis: verum

end;

end;

end;

hence DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s)) by FUNCT_1:68; :: thesis: verum

end;

theorem Th6: :: SCMFSA6C:6

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for i being parahalting Instruction of SCM+FSA holds NPP (Exec (i,(Initialized s))) = NPP (IExec ((Macro i),P,s))

proof end;

Lm4: for a being Int-Location
for s being State of SCM+FSA holds s . a = (NPP s) . a

proof end;

Lm5: for f being FinSeq-Location
for s being State of SCM+FSA holds (NPP s) . f = s . f

proof end;

theorem Th7: :: SCMFSA6C:7

for a being Int-Location
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting keeping_0 Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((I ';' j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a

proof end;

theorem Th8: :: SCMFSA6C:8

for f being FinSeq-Location
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting keeping_0 Program of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((I ';' j),P,s)) . f = (Exec (j,(IExec (I,P,s)))) . f

proof end;

theorem Th9: :: SCMFSA6C:9

for a being Int-Location
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((i ';' j),P,s)) . a = (Exec (j,(Exec (i,(Initialized s))))) . a

proof end;

theorem :: SCMFSA6C:10

for f being FinSeq-Location
for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for i being parahalting keeping_0 Instruction of SCM+FSA
for j being parahalting Instruction of SCM+FSA holds (IExec ((i ';' j),P,s)) . f = (Exec (j,(Exec (i,(Initialized s))))) . f

proof end;

begin

definition

canceled;
let a, b be Int-Location ;
func swap (a,b) -> Program of SCM+FSA equals :: SCMFSA6C:def 4
(((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)) ';' (b := (FirstNotUsed (Macro (a := b))));
correctness
coherence
(((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)) ';' (b := (FirstNotUsed (Macro (a := b)))) is Program of SCM+FSA;
;

end;

:: deftheorem SCMFSA6C:def 3 :
canceled;

:: deftheorem defines swap SCMFSA6C:def 4 :
for a, b being Int-Location holds swap (a,b) = (((FirstNotUsed (Macro (a := b))) := a) ';' (a := b)) ';' (b := (FirstNotUsed (Macro (a := b))));

registration

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

end;

registration

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

end;

theorem :: SCMFSA6C:11

for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for a, b being read-write Int-Location holds
( (IExec ((swap (a,b)),P,s)) . a = s . b & (IExec ((swap (a,b)),P,s)) . b = s . a )

proof end;

theorem :: SCMFSA6C:12

for a, b being Int-Location holds UsedInt*Loc (swap (a,b)) = {}

proof end;

theorem :: SCMFSA6C:13

for a being Int-Location
for s being State of SCM+FSA holds s . a = (NPP s) . a by Lm4;

theorem :: SCMFSA6C:14

for f being FinSeq-Location
for s being State of SCM+FSA holds (NPP s) . f = s . f by Lm5;