begin
set SA0 = Start-At 0 ,SCM+FSA ;
theorem
theorem
begin
:: deftheorem Def1 defines parahalting SCMFSA6C:def 1 :
:: deftheorem Def2 defines keeping_0 SCMFSA6C:def 2 :
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
:: deftheorem defines Initialize SCMFSA6C:def 3 :
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 (Initialize (IExec I,s)) = DataPart (IExec I,s)let s be
State of
SCM+FSA ;
DataPart (Initialize (IExec I,s)) = DataPart (IExec I,s)set IE =
IExec I,
s;
now
A1:
dom (Initialize (IExec I,s)) = the
carrier of
SCM+FSA
by PARTFUN1:def 4;
then A2:
dom (Initialize (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 (Initialize (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 (Initialize (IExec I,s))) holds
(DataPart (Initialize (IExec I,s))) . b2 = (IExec I,s) . b2then A4:
dom (DataPart (Initialize (IExec I,s))) = Int-Locations \/ FinSeq-Locations
by A1, A3, A2, XBOOLE_1:21;
let x be
set ;
( x in dom (DataPart (Initialize (IExec I,s))) implies (DataPart (Initialize (IExec I,s))) . b1 = (IExec I,s) . b1 )assume A5:
x in dom (DataPart (Initialize (IExec I,s)))
;
(DataPart (Initialize (IExec I,s))) . b1 = (IExec I,s) . b1
end;
hence
DataPart (Initialize (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 defines swap SCMFSA6C:def 4 :
theorem
theorem