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 & Macro (halt SCM+FSA) is parahalting )
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 Th4:
theorem Th5:
Lm3:
now
set IF =
Int-Locations \/ FinSeq-Locations;
let I be
parahalting keeping_0 Program of
SCM+FSA;
for s being State of SCM+FSA holds DataPart (Initialized (IExec (I,s))) = DataPart (IExec (I,s))let s be
State of
SCM+FSA;
DataPart (Initialized (IExec (I,s))) = DataPart (IExec (I,s))set IE =
IExec (
I,
s);
now
A1:
dom (Initialized (IExec (I,s))) = the
carrier of
SCM+FSA
by PARTFUN1:def 4;
then A2:
dom (Initialized (IExec (I,s))) = (Int-Locations \/ FinSeq-Locations) \/ ({(IC SCM+FSA)} \/ NAT)
by SCMFSA_2:8, XBOOLE_1:4;
A3:
dom (IExec (I,s)) = the
carrier of
SCM+FSA
by PARTFUN1:def 4;
hence
dom (DataPart (Initialized (IExec (I,s)))) = (dom (IExec (I,s))) /\ (Int-Locations \/ FinSeq-Locations)
by A1, RELAT_1:90, SCMFSA_2:127;
for x being set st x in dom (DataPart (Initialized (IExec (I,s)))) holds
(DataPart (Initialized (IExec (I,s)))) . b2 = (IExec (I,s)) . b2then A4:
dom (DataPart (Initialized (IExec (I,s)))) = Int-Locations \/ FinSeq-Locations
by A1, A3, A2, XBOOLE_1:21;
let x be
set ;
( x in dom (DataPart (Initialized (IExec (I,s)))) implies (DataPart (Initialized (IExec (I,s)))) . b1 = (IExec (I,s)) . b1 )assume A5:
x in dom (DataPart (Initialized (IExec (I,s))))
;
(DataPart (Initialized (IExec (I,s)))) . b1 = (IExec (I,s)) . b1
end;
hence
DataPart (Initialized (IExec (I,s))) = DataPart (IExec (I,s))
by FUNCT_1:68, SCMFSA_2:127;
verum
end;
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem
begin
:: 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))));
theorem
theorem