:: 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-2012 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 Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting 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
proofend;

theorem :: SCMFSA6C:2
for f being FinSeq-Location
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting 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
proofend;

begin

definition
let i be Instruction of SCM+FSA;
attri is parahalting  means :Def1: :: SCMFSA6C:def 1
 Macro i is parahalting ;
attri 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
proofend;

Lm2:  Macro (halt SCM+FSA) is keeping_0
proofend;

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

registration
cluster with_explicit_jumps IC-relocable parahalting keeping_0 for Element of the InstructionsF of SCM+FSA;
existence
 ex b1 being Instruction of SCM+FSA st
( b1 is keeping_0 & b1 is parahalting )
proofend;
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;
clustera := b ->  parahalting ;
coherence
 a := b is parahalting
proofend;
cluster AddTo (a,b) ->  parahalting ;
coherence
 AddTo (a,b) is parahalting
proofend;
cluster SubFrom (a,b) ->  parahalting ;
coherence
 SubFrom (a,b) is parahalting
proofend;
cluster MultBy (a,b) ->  parahalting ;
coherence
 MultBy (a,b) is parahalting
proofend;
cluster Divide (a,b) ->  parahalting ;
coherence
 Divide (a,b) is parahalting
proofend;
let f be FinSeq-Location ;
clusterb := (f,a) ->  parahalting ;
coherence
 b := (f,a) is parahalting
proofend;
cluster(f,a) := b ->  parahalting keeping_0 ;
coherence
 ( (f,a) := b is parahalting & (f,a) := b is keeping_0 )
proofend;
end;

registration
let a be Int-Location;
let f be FinSeq-Location ;
clustera :=len f ->  parahalting ;
coherence
 a :=len f is parahalting
proofend;
clusterf :=<0,...,0> a ->  parahalting keeping_0 ;
coherence
 ( f :=<0,...,0> a is parahalting &amp; f :=<0,...,0> a is keeping_0 )
proofend;
end;

registration
let a be read-write Int-Location;
let b be Int-Location;
clustera := b ->  keeping_0 ;
coherence
 a := b is keeping_0
proofend;
cluster AddTo (a,b) ->  keeping_0 ;
coherence
 AddTo (a,b) is keeping_0
proofend;
cluster SubFrom (a,b) ->  keeping_0 ;
coherence
 SubFrom (a,b) is keeping_0
proofend;
cluster MultBy (a,b) ->  keeping_0 ;
coherence
 MultBy (a,b) is keeping_0
proofend;
end;

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

registration
let a be Int-Location;
let f be FinSeq-Location ;
let b be read-write Int-Location;
clusterb := (f,a) ->  keeping_0 ;
coherence
 b := (f,a) is keeping_0
proofend;
end;

registration
let f be FinSeq-Location ;
let b be read-write Int-Location;
clusterb :=len f ->  keeping_0 ;
coherence
 b :=len f is keeping_0
proofend;
end;

registration
let i be parahalting Instruction of SCM+FSA;
let J be parahalting Program of SCM+FSA;
clusteri ";" 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;
clusterI ";" j ->  parahalting ;
coherence
 I ";" j is parahalting ;
end;

registration
let i, j be parahalting Instruction of SCM+FSA;
clusteri ";" 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;
clusteri ";" 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;
clusterI ";" j ->  keeping_0 ;
coherence
 I ";" j is keeping_0 ;
end;

registration
let i, j be keeping_0 Instruction of SCM+FSA;
clusteri ";" j ->  keeping_0 ;
coherence
 i ";" j is keeping_0 ;
end;

begin

theorem :: SCMFSA6C:3
canceled;

theorem Th4: :: SCMFSA6C:4
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))
proofend;

Lm3: now__::_thesis:_for_I_being_keeping_0_parahalting_Program_of_SCM+FSA
for_s_being_State_of_SCM+FSA
for_P_being_Instruction-Sequence_of_SCM+FSA_holds_DataPart_(Initialized_(IExec_(I,P,s)))_=_DataPart_(IExec_(I,P,s))
set IF = Data-Locations ;
let I be keeping_0 parahalting Program of SCM+FSA; ::_thesis: for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))
let s be State of SCM+FSA; ::_thesis: for P being Instruction-Sequence of SCM+FSA holds DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))
let P be Instruction-Sequence of SCM+FSA; ::_thesis: DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))
set IE = IExec (I,P,s);
now__::_thesis:_(_dom_(DataPart_(Initialized_(IExec_(I,P,s))))_=_(dom_(IExec_(I,P,s)))_/\_(Data-Locations_)_&amp;_(_for_x_being_set_st_x_in_dom_(DataPart_(Initialized_(IExec_(I,P,s))))_holds_
(DataPart_(Initialized_(IExec_(I,P,s))))_._x_=_(IExec_(I,P,s))_._x_)_)
A1: dom (Initialized (IExec (I,P,s))) = the carrier of SCM+FSA by PARTFUN1:def_2;
A2: the carrier of SCM+FSA = {(IC )} \/ (Data-Locations ) by STRUCT_0:4;
A3: dom (IExec (I,P,s)) = the carrier of SCM+FSA by PARTFUN1:def_2;
hence  dom (DataPart (Initialized (IExec (I,P,s)))) = (dom (IExec (I,P,s))) /\ (Data-Locations ) by A1, RELAT_1:61; ::_thesis: for x being set st x in dom (DataPart (Initialized (IExec (I,P,s)))) holds
(DataPart (Initialized (IExec (I,P,s)))) . b2 = (IExec (I,P,s)) . b2
then A4: dom (DataPart (Initialized (IExec (I,P,s)))) = Data-Locations by A3, A2, XBOOLE_1:21;
let x be set ; ::_thesis: ( x in dom (DataPart (Initialized (IExec (I,P,s)))) implies (DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1 )
assume A5: x in dom (DataPart (Initialized (IExec (I,P,s)))) ; ::_thesis: (DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
percases ( x in Int-Locations or x in FinSeq-Locations ) by A5, A4, SCMFSA_2:100, XBOOLE_0:def_3;
suppose x in Int-Locations ; ::_thesis: (DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
then reconsider x9 = x as Int-Location by AMI_2:def_16;
percases ( x9 is read-write or x9 is read-only ) ;
supposeA6: x9 is read-write ; ::_thesis: (DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
thus (DataPart (Initialized (IExec (I,P,s)))) . x = (Initialized (IExec (I,P,s))) . x by A5, A4, FUNCT_1:49
.= (IExec (I,P,s)) . x by A6, SCMFSA_M:37 ; ::_thesis: verum
end;
suppose x9 is read-only ; ::_thesis: (DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
then A7: x9 = intloc 0 by SCMFSA_M:def_2;
thus (DataPart (Initialized (IExec (I,P,s)))) . x = (Initialized (IExec (I,P,s))) . x9 by A5, A4, FUNCT_1:49
.= 1 by A7, SCMFSA_M:9
.= (IExec (I,P,s)) . x by A7, SCMFSA6B:11 ; ::_thesis: verum
end;
end;
end;
suppose x in FinSeq-Locations ; ::_thesis: (DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
then reconsider x9 = x as FinSeq-Location by SCMFSA_2:def_5;
thus (DataPart (Initialized (IExec (I,P,s)))) . x = (Initialized (IExec (I,P,s))) . x9 by A5, A4, FUNCT_1:49
.= (IExec (I,P,s)) . x by SCMFSA_M:37 ; ::_thesis: verum
end;
end;
end;
hence  DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s)) by FUNCT_1:46; ::_thesis: verum
end;

theorem Th5: :: SCMFSA6C:5
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for i being parahalting Instruction of SCM+FSA holds Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
proofend;

theorem Th6: :: SCMFSA6C:6
for a being Int-Location
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting 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
proofend;

theorem Th7: :: SCMFSA6C:7
for f being FinSeq-Location
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being keeping_0 parahalting 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
proofend;

theorem Th8: :: SCMFSA6C:8
for a being Int-Location
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
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
proofend;

theorem :: SCMFSA6C:9
for f being FinSeq-Location
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
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
proofend;

begin

definition
let a, b be Int-Location;
func swap (a,b) ->  Program of SCM+FSA equals :: SCMFSA6C:def 3
(((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  defines swap SCMFSA6C:def_3_:_
 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:10
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for a, b being read-write Int-Location holds
( (IExec ((swap (a,b)),P,s)) . a = s . b &amp; (IExec ((swap (a,b)),P,s)) . b = s . a )
proofend;

theorem :: SCMFSA6C:11
for a, b being Int-Location holds UsedInt*Loc (swap (a,b)) = {}
proofend;