begin
set SA0 = Start-At (0,SCM+FSA);
theorem
theorem
begin
:: 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
Lm2:
Macro (halt SCM+FSA) is keeping_0
registration
let a,
b be
Int-Location ;
cluster a := b -> parahalting ;
coherence
a := b is parahalting
cluster AddTo (
a,
b)
-> parahalting ;
coherence
AddTo (a,b) is parahalting
cluster SubFrom (
a,
b)
-> parahalting ;
coherence
SubFrom (a,b) is parahalting
cluster MultBy (
a,
b)
-> parahalting ;
coherence
MultBy (a,b) is parahalting
cluster Divide (
a,
b)
-> parahalting ;
coherence
Divide (a,b) is parahalting
let f be
FinSeq-Location ;
cluster b := (
f,
a)
-> parahalting ;
coherence
b := (f,a) is parahalting
cluster (
f,
a)
:= b -> parahalting keeping_0 ;
coherence
( (f,a) := b is parahalting & (f,a) := b is keeping_0 )
end;
begin
theorem Th3:
theorem Th5:
Lm3:
now
set IF =
Data-Locations ;
let I be
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))let s be
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 P be
Instruction-Sequence of
SCM+FSA;
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 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;
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)) . b2then A4:
dom (DataPart (Initialized (IExec (I,P,s)))) = Data-Locations
by A3, A2, XBOOLE_1:21;
let x be
set ;
( 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))))
;
(DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
per cases
( x in Int-Locations or x in FinSeq-Locations )
by A5, A4, SCMFSA_2:100, XBOOLE_0:def 3;
suppose
x in Int-Locations
;
(DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
then reconsider x9 =
x as
Int-Location by SCMFSA_2:4;
per cases
( not x9 is read-only or x9 is read-only )
;
suppose
x9 is
read-only
;
(DataPart (Initialized (IExec (I,P,s)))) . b1 = (IExec (I,P,s)) . b1
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:49
.=
1
by A7, SCMFSA6A:38
.=
(IExec (I,P,s)) . x
by A7, SCMFSA6B:11
;
verum
end;
end;
end;
end;
end;
hence
DataPart (Initialized (IExec (I,P,s))) = DataPart (IExec (I,P,s))
by FUNCT_1:46;
verum
end;
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem
begin
:: 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))));
theorem
theorem