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

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 really-closed parahalting Program of SCM+FSA
for J being really-closed 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 Instruction-Sequence of SCM+FSA
for I being keeping_0 really-closed parahalting Program of SCM+FSA
for J being really-closed parahalting Program of SCM+FSA holds (IExec ((I ";" J),P,s)) . f = (IExec (J,P,(IExec (I,P,s)))) . f
proof end;

canceled;

::$CD definition let i be Instruction of SCM+FSA; :: attr i is parahalting means :: :Def1: :: Macro i is parahalting; attr i is keeping_0 means :Def1: :: SCMFSA6C:def 1 Macro i is keeping_0 ; end; :: deftheorem Def1 defines keeping_0 SCMFSA6C:def 1 : for i being Instruction of SCM+FSA holds ( i is keeping_0 iff Macro i is keeping_0 ); Lm1: proof end; registration coherence by Lm1; end; registration let i be sequential Instruction of SCM+FSA; coherence proof end; end; registration let a, b be Int-Location; let f be FinSeq-Location ; cluster (f,a) := b -> keeping_0 ; coherence (f,a) := b is keeping_0 proof end; end; registration let a be Int-Location; let f be FinSeq-Location ; coherence 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 cluster sequential V155( Segm 3, SCM+FSA ) V157( Segm 3, SCM+FSA ) keeping_0 for M3( the InstructionsF of SCM+FSA); existence ex b1 being Instruction of SCM+FSA st ( b1 is keeping_0 & b1 is sequential ) proof end; end; registration let i be keeping_0 Instruction of SCM+FSA; coherence by Def1; 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; coherence b :=len f is keeping_0 proof end; end; registration let i be sequential Instruction of SCM+FSA; coherence proof end; end; :: registration :: let i be keeping_0 Instruction of SCM+FSA; :: cluster Macro i -> really-closed; :: coherence; :: end; registration let i be sequential Instruction of SCM+FSA; let J be really-closed parahalting Program of SCM+FSA; coherence ( i ";" J is parahalting & i ";" J is really-closed ) ; end; registration let I be really-closed parahalting Program of SCM+FSA; let j be sequential Instruction of SCM+FSA; coherence ( I ";" j is parahalting & I ";" j is really-closed ) ; end; registration let i, j be sequential Instruction of SCM+FSA; coherence ( i ";" j is parahalting & i ";" j is really-closed ) ; end; registration let i be sequential keeping_0 Instruction of SCM+FSA; let J be keeping_0 really-closed Program of SCM+FSA; cluster i ";" J -> keeping_0 ; coherence i ";" J is keeping_0 ; end; registration let I be keeping_0 really-closed Program of SCM+FSA; let j be sequential keeping_0 Instruction of SCM+FSA; cluster I ";" j -> keeping_0 ; coherence I ";" j is keeping_0 ; end; registration let i, j be sequential keeping_0 Instruction of SCM+FSA; cluster i ";" j -> keeping_0 ; coherence i ";" j is keeping_0 ; end; theorem :: SCMFSA6C:3 canceled; ::$CT
theorem Th3: :: 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))
proof end;

Lm2: 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))) /\ & ( for x being object 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 = {()} \/ 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))) /\ by ; :: thesis: for x being object 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 ;
let x be object ; :: 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
per cases by ;
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;
per cases ( x9 is read-write or x9 is read-only ) ;
suppose A6: 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
.= (IExec (I,P,s)) . x by ; :: 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 ;
thus (DataPart (Initialized (IExec (I,P,s)))) . x = (Initialized (IExec (I,P,s))) . x9 by
.= 1 by
.= (IExec (I,P,s)) . x by ; :: 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
.= (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 Th4: :: SCMFSA6C:5
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for i being sequential Instruction of SCM+FSA holds Exec (i,()) = IExec ((),P,s)
proof end;

theorem Th5: :: 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 really-closed parahalting Program of SCM+FSA
for j being sequential Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . a = (Exec (j,(IExec (I,P,s)))) . a
proof end;

theorem Th6: :: 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 really-closed parahalting Program of SCM+FSA
for j being sequential Instruction of SCM+FSA holds (IExec ((I ";" j),P,s)) . f = (Exec (j,(IExec (I,P,s)))) . f
proof end;

theorem Th7: :: 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 sequential keeping_0 Instruction of SCM+FSA
for j being sequential Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . a = (Exec (j,(Exec (i,())))) . a
proof end;

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 sequential keeping_0 Instruction of SCM+FSA
for j being sequential Instruction of SCM+FSA holds (IExec ((i ";" j),P,s)) . f = (Exec (j,(Exec (i,())))) . f
proof end;

definition
let a, b be Int-Location;
func swap (a,b) -> Program of SCM+FSA equals :: SCMFSA6C:def 2
(((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 2 :
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;
coherence
( swap (a,b) is parahalting & swap (a,b) is really-closed )
;
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 & (IExec ((swap (a,b)),P,s)) . b = s . a )
proof end;

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

registration
let i, j be sequential Instruction of SCM+FSA;
coherence
i ';' j is really-closed
;
end;

registration
let I be really-closed MacroInstruction of SCM+FSA ;
let j be sequential Instruction of SCM+FSA;
coherence
I ';' j is really-closed
;
end;

registration
let i be sequential Instruction of SCM+FSA;
let J be really-closed MacroInstruction of SCM+FSA ;
coherence
i ';' J is really-closed
;
end;