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 0 ,SCM+FSA );
theorem
canceled;
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem Th12:
for
s1,
s2 being
State of
SCM+FSA for
J being
InitHalting Program of
SCM+FSA st
Initialized J c= s1 holds
for
n being
Element of
NAT st
ProgramPart (Relocated J,n) c= s2 &
IC s2 = n &
DataPart s1 = DataPart s2 holds
for
i being
Element of
NAT holds
(
(IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) &
IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),
n = CurInstr (ProgramPart s2),
(Comput (ProgramPart s2),s2,i) &
DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) )
theorem Th13:
theorem Th14:
for
s1,
s2 being
State of
SCM+FSA for
I being
InitHalting Program of
SCM+FSA st
Initialized I c= s1 &
Initialized I c= s2 &
s1,
s2 equal_outside NAT holds
for
k being
Element of
NAT holds
(
Comput (ProgramPart s1),
s1,
k,
Comput (ProgramPart s2),
s2,
k equal_outside NAT &
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,k)),
(Comput (ProgramPart s1),s1,k) = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,k)),
(Comput (ProgramPart s2),s2,k) )
theorem Th15:
theorem
canceled;
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
for
I being
InitHalting keepInt0_1 Program of
SCM+FSA for
J being
InitHalting Program of
SCM+FSA for
s being
State of
SCM+FSA st
Initialized (I ';' J) c= s holds
(
IC (Comput (ProgramPart s),s,((LifeSpan (ProgramPart (s +* I)),(s +* I)) + 1)) = card I &
DataPart (Comput (ProgramPart s),s,((LifeSpan (ProgramPart (s +* I)),(s +* I)) + 1)) = DataPart ((Comput (ProgramPart (s +* I)),(s +* I),(LifeSpan (ProgramPart (s +* I)),(s +* I))) +* (Initialized J)) &
ProgramPart (Relocated J,(card I)) c= Comput (ProgramPart s),
s,
((LifeSpan (ProgramPart (s +* I)),(s +* I)) + 1) &
(Comput (ProgramPart s),s,((LifeSpan (ProgramPart (s +* I)),(s +* I)) + 1)) . (intloc 0 ) = 1 &
ProgramPart s halts_on s &
LifeSpan (ProgramPart s),
s = ((LifeSpan (ProgramPart (s +* I)),(s +* I)) + 1) + (LifeSpan (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))) & (
J is
keeping_0 implies
(Result (ProgramPart s),s) . (intloc 0 ) = 1 ) )
theorem Th26:
for
s being
State of
SCM+FSA for
I being
keepInt0_1 Program of
SCM+FSA st
ProgramPart (s +* I) halts_on s +* I holds
for
J being
InitClosed Program of
SCM+FSA st
Initialized (I ';' J) c= s holds
for
k being
Element of
NAT holds
(Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J)),k) +* (Start-At ((IC (Comput (ProgramPart ((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J))),((Result (ProgramPart (s +* I)),(s +* I)) +* (Initialized J)),k)) + (card I)),SCM+FSA ),
Comput (ProgramPart (s +* (I ';' J))),
(s +* (I ';' J)),
(((LifeSpan (ProgramPart (s +* I)),(s +* I)) + 1) + k) equal_outside NAT
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
SCM+FSA for
I,
J being
InitHalting Program of
SCM+FSA 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 (((card I) + (card J)) + 3),SCM+FSA ) ) & (
s . a <> 0 implies
IExec (if=0 a,I,J),
s = (IExec J,s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA ) ) )
theorem
for
s being
State of
SCM+FSA for
I,
J being
InitHalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
IC (IExec (if=0 a,I,J),s) = ((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
SCM+FSA for
I,
J being
InitHalting Program of
SCM+FSA 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 (((card I) + (card J)) + 3),SCM+FSA ) ) & (
s . a <= 0 implies
IExec (if>0 a,I,J),
s = (IExec J,s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA ) ) )
theorem
for
s being
State of
SCM+FSA for
I,
J being
InitHalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
IC (IExec (if>0 a,I,J),s) = ((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
SCM+FSA for
I,
J being
InitHalting Program of
SCM+FSA 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 ((((card I) + (card J)) + (card J)) + 7),SCM+FSA ) ) & (
s . a >= 0 implies
IExec (if<0 a,I,J),
s = (IExec J,s) +* (Start-At ((((card I) + (card J)) + (card J)) + 7),SCM+FSA ) ) )
registration
let I,
J be
InitHalting Program of
SCM+FSA ;
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:
for
s being
State of
SCM+FSA for
I being
InitHalting keepInt0_1 Program of
SCM+FSA for
a being
read-write Int-Location st
I does_not_destroy a holds
(Comput (ProgramPart ((Initialize s) +* ((I ';' (SubFrom a,(intloc 0 ))) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* ((I ';' (SubFrom a,(intloc 0 ))) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialize s) +* ((I ';' (SubFrom a,(intloc 0 ))) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* ((I ';' (SubFrom a,(intloc 0 ))) +* (Start-At 0 ,SCM+FSA ))))) . a = (s . a) - 1
theorem Th65:
theorem
theorem Th67:
theorem Th68:
theorem Th69:
for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_onInit s &
I is_halting_onInit s holds
for
m being
Element of
NAT st
m < LifeSpan (ProgramPart (s +* (Initialized I))),
(s +* (Initialized I)) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m)),
(Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m) = CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m)),
(Comput (ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m)
theorem Th70:
theorem Th71:
for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_onInit s &
I is_halting_onInit s holds
(
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))))),
(Comput (ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) = goto 0 & ( for
m being
Element of
NAT st
m <= LifeSpan (ProgramPart (s +* (Initialized I))),
(s +* (Initialized I)) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m)),
(Comput (ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m) <> halt SCM+FSA ) )
theorem
canceled;
theorem Th73:
theorem
theorem
theorem
theorem Th77:
for
s being
State of
SCM+FSA for
I being
good InitHalting Program of
SCM+FSA for
a being
read-write Int-Location st
I does_not_destroy a &
s . a > 0 holds
ex
s2 being
State of
SCM+FSA ex
k being
Element of
NAT st
(
s2 = s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) &
k = (LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 &
(Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 &
(Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for
b being
read-write Int-Location st
b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for
f being
FinSeq-Location holds
(Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) &
IC (Comput (ProgramPart s2),s2,k) = 0 & ( for
n being
Element of
NAT st
n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
theorem Th78:
theorem Th79:
theorem
theorem
theorem
theorem
:: deftheorem Def6 defines good SCM_HALT:def 6 :