begin
:: deftheorem Def1 defines InitClosed SCM_HALT:def 1 :
:: deftheorem Def2 defines InitHalting SCM_HALT:def 2 :
:: deftheorem Def3 defines keepInt0_1 SCM_HALT:def 3 :
theorem Th1:
theorem Th2:
set iS = ((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ));
theorem
canceled;
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem
canceled;
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
:: deftheorem Def4 defines is_closed_onInit SCM_HALT:def 4 :
:: deftheorem Def5 defines is_halting_onInit SCM_HALT:def 5 :
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem
theorem Th40:
theorem Th41:
theorem
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
for
s being
State of
for
I,
J being
InitHalting Program of
for
a being
read-write Int-Location holds
(
if=0 a,
I,
J is
InitHalting & (
s . a = 0 implies
IExec (if=0 a,I,J),
s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) & (
s . a <> 0 implies
IExec (if=0 a,I,J),
s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) )
theorem
for
s being
State of
for
I,
J being
InitHalting Program of
for
a being
read-write Int-Location holds
(
IC (IExec (if=0 a,I,J),s) = insloc (((card I) + (card J)) + 3) & (
s . a = 0 implies ( ( for
d being
Int-Location holds
(IExec (if=0 a,I,J),s) . d = (IExec I,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if=0 a,I,J),s) . f = (IExec I,s) . f ) ) ) & (
s . a <> 0 implies ( ( for
d being
Int-Location holds
(IExec (if=0 a,I,J),s) . d = (IExec J,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if=0 a,I,J),s) . f = (IExec J,s) . f ) ) ) )
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
for
s being
State of
for
I,
J being
InitHalting Program of
for
a being
read-write Int-Location holds
(
if>0 a,
I,
J is
InitHalting & (
s . a > 0 implies
IExec (if>0 a,I,J),
s = (IExec I,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) & (
s . a <= 0 implies
IExec (if>0 a,I,J),
s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) )
theorem
for
s being
State of
for
I,
J being
InitHalting Program of
for
a being
read-write Int-Location holds
(
IC (IExec (if>0 a,I,J),s) = insloc (((card I) + (card J)) + 3) & (
s . a > 0 implies ( ( for
d being
Int-Location holds
(IExec (if>0 a,I,J),s) . d = (IExec I,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if>0 a,I,J),s) . f = (IExec I,s) . f ) ) ) & (
s . a <= 0 implies ( ( for
d being
Int-Location holds
(IExec (if>0 a,I,J),s) . d = (IExec J,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if>0 a,I,J),s) . f = (IExec J,s) . f ) ) ) )
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
for
s being
State of
for
I,
J being
InitHalting Program of
for
a being
read-write Int-Location holds
(
if<0 a,
I,
J is
InitHalting & (
s . a < 0 implies
IExec (if<0 a,I,J),
s = (IExec I,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7))) ) & (
s . a >= 0 implies
IExec (if<0 a,I,J),
s = (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7))) ) )
registration
let I,
J be
InitHalting Program of ;
let a be
read-write Int-Location ;
cluster if=0 a,
I,
J -> InitHalting ;
correctness
coherence
if=0 a,I,J is InitHalting ;
by Th47;
cluster if>0 a,
I,
J -> InitHalting ;
correctness
coherence
if>0 a,I,J is InitHalting ;
by Th53;
cluster if<0 a,
I,
J -> InitHalting ;
correctness
coherence
if<0 a,I,J is InitHalting ;
by Th58;
end;
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
theorem Th63:
theorem Th64:
theorem Th65:
theorem
theorem Th67:
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem
theorem Th73:
theorem
theorem
theorem
theorem Th77:
for
s being
State of
for
I being
good InitHalting Program of
for
a being
read-write Int-Location st
I does_not_destroy a &
s . a > 0 holds
ex
s2 being
State of ex
k being
Element of
NAT st
(
s2 = s +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) &
k = (LifeSpan (s +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 &
(Computation s2,k) . a = (s . a) - 1 &
(Computation s2,k) . (intloc 0 ) = 1 & ( for
b being
read-write Int-Location st
b <> a holds
(Computation s2,k) . b = (IExec I,s) . b ) & ( for
f being
FinSeq-Location holds
(Computation s2,k) . f = (IExec I,s) . f ) &
IC (Computation s2,k) = insloc 0 & ( for
n being
Element of
NAT st
n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
theorem Th78:
theorem Th79:
theorem
theorem
theorem
theorem
:: deftheorem Def6 defines good SCM_HALT:def 6 :