begin
set SA0 = Start-At (0,SCM+FSA);
set iS = Initialize ((intloc 0) .--> 1);
reconsider EP = {} as PartState of SCM+FSA by FUNCT_1:174, RELAT_1:206;
IC in dom (Start-At (0,SCM+FSA))
by COMPOS_1:52;
then ICiS: IC (Initialize ((intloc 0) .--> 1)) =
IC (Start-At (0,SCM+FSA))
by FUNCT_4:14
.=
0
by COMPOS_1:64
;
zSA0:
Start-At (0,SCM+FSA) c= Initialize ((intloc 0) .--> 1)
by FUNCT_4:26;
diS: dom (Initialize ((intloc 0) .--> 1)) =
(dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA)))
by FUNCT_4:def 1
.=
{(intloc 0)} \/ (dom (Start-At (0,SCM+FSA)))
by FUNCOP_1:19
.=
{(intloc 0)} \/ {(IC )}
by FUNCOP_1:19
;
then ddiS:
dom (Initialize ((intloc 0) .--> 1)) = {(intloc 0),(IC )}
by ENUMSET1:41;
intloc 0 in {(intloc 0)}
by TARSKI:def 1;
then iniS:
intloc 0 in dom (Initialize ((intloc 0) .--> 1))
by diS, XBOOLE_0:def 3;
AA:
intloc 0 <> IC
by SCMFSA_2:81;
dom (Start-At (0,SCM+FSA)) = {(IC )}
by FUNCOP_1:19;
then
not intloc 0 in dom (Start-At (0,SCM+FSA))
by AA, TARSKI:def 1;
then iSint: (Initialize ((intloc 0) .--> 1)) . (intloc 0) =
((intloc 0) .--> 1) . (intloc 0)
by FUNCT_4:12
.=
1
by FUNCOP_1:87
;
:: deftheorem Def1 defines InitClosed SCM_HALT:def 1 :
for I being Program of SCM+FSA holds
( I is InitClosed iff for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
for n being Element of NAT st Initialize ((intloc 0) .--> 1) c= s holds
IC (Comput (P,s,n)) in dom I );
:: deftheorem Def2 defines InitHalting SCM_HALT:def 2 :
for I being Program of SCM+FSA holds
( I is InitHalting iff for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= P holds
P halts_on s );
:: deftheorem Def3 defines keepInt0_1 SCM_HALT:def 3 :
for I being Program of SCM+FSA holds
( I is keepInt0_1 iff for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT st I c= p holds
for k being Element of NAT holds (Comput (p,s,k)) . (intloc 0) = 1 );
theorem Th1:
theorem Th2:
theorem
canceled;
theorem Th4:
theorem Th5:
theorem
canceled;
theorem Th7:
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem Th12:
for
s1,
s2 being
State of
SCM+FSA for
p1,
p2 being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
J being
InitHalting Program of
SCM+FSA st
Initialize ((intloc 0) .--> 1) c= s1 &
J c= p1 holds
for
n being
Element of
NAT st
Reloc (
J,
n)
c= p2 &
IC s2 = n &
DataPart s1 = DataPart s2 holds
for
i being
Element of
NAT holds
(
(IC (Comput (p1,s1,i))) + n = IC (Comput (p2,s2,i)) &
IncAddr (
(CurInstr (p1,(Comput (p1,s1,i)))),
n)
= CurInstr (
p2,
(Comput (p2,s2,i))) &
DataPart (Comput (p1,s1,i)) = DataPart (Comput (p2,s2,i)) )
theorem
theorem Th14:
for
s1,
s2 being
State of
SCM+FSA for
p1,
p2 being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
I being
InitHalting Program of
SCM+FSA st
Initialize ((intloc 0) .--> 1) c= s1 &
Initialize ((intloc 0) .--> 1) c= s2 &
I c= p1 &
I c= p2 &
NPP s1 = NPP s2 holds
for
k being
Element of
NAT holds
(
NPP (Comput (p1,s1,k)) = NPP (Comput (p2,s2,k)) &
CurInstr (
p1,
(Comput (p1,s1,k)))
= CurInstr (
p2,
(Comput (p2,s2,k))) )
theorem Th15:
theorem
canceled;
theorem Th17:
theorem Th18:
theorem
theorem
canceled;
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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
Initialize ((intloc 0) .--> 1) c= s &
I ';' J c= p holds
(
IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I &
DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = DataPart ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) &
Reloc (
J,
(card I))
c= p &
(Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) . (intloc 0) = 1 &
p halts_on s &
LifeSpan (
p,
s)
= ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & (
J is
keeping_0 implies
(Result (p,s)) . (intloc 0) = 1 ) )
theorem Th26:
for
s being
State of
SCM+FSA for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
I being
keepInt0_1 Program of
SCM+FSA st
p +* I halts_on s holds
for
J being
InitClosed Program of
SCM+FSA st
Initialize ((intloc 0) .--> 1) c= s &
I ';' J c= p holds
for
k being
Element of
NAT holds
NPP ((Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)),SCM+FSA))) = NPP (Comput ((p +* (I ';' J)),s,(((LifeSpan ((p +* I),s)) + 1) + k)))
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 :
for I being Program of SCM+FSA
for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds
( I is_closed_onInit s,p iff for k being Element of NAT holds IC (Comput ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) in dom I );
:: deftheorem Def5 defines is_halting_onInit SCM_HALT:def 5 :
for I being Program of SCM+FSA
for s being State of SCM+FSA
for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds
( I is_halting_onInit s,p iff p +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) );
theorem Th35:
theorem Th36:
theorem Th37:
LmX:
for s1, s2 being State of SCM+FSA
for J being InitHalting Program of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st NPP s1 = NPP s2 holds
NPP (IExec (J,P,s1)) = NPP (IExec (J,P,s2))
theorem
theorem
theorem Th40:
theorem Th41:
theorem
theorem Th43:
theorem Th44:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a = 0 &
I is_closed_onInit s,
p &
I is_halting_onInit s,
p holds
IExec (
(if=0 (a,I,J)),
p,
s)
= (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
theorem Th45:
theorem Th46:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA st
s . a <> 0 &
J is_closed_onInit s,
p &
J is_halting_onInit s,
p holds
IExec (
(if=0 (a,I,J)),
p,
s)
= (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
theorem Th47:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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)),
p,
s)
= (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & (
s . a <> 0 implies
IExec (
(if=0 (a,I,J)),
p,
s)
= (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
theorem
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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)),p,s)) = ((card I) + (card J)) + 3 & (
s . a = 0 implies ( ( for
d being
Int-Location holds
(IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f ) ) ) & (
s . a <> 0 implies ( ( for
d being
Int-Location holds
(IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f ) ) ) )
theorem Th49:
theorem Th50:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a > 0 &
I is_closed_onInit s,
p &
I is_halting_onInit s,
p holds
IExec (
(if>0 (a,I,J)),
p,
s)
= (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
theorem Th51:
theorem Th52:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA st
s . a <= 0 &
J is_closed_onInit s,
p &
J is_halting_onInit s,
p holds
IExec (
(if>0 (a,I,J)),
p,
s)
= (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
theorem Th53:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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)),
p,
s)
= (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & (
s . a <= 0 implies
IExec (
(if>0 (a,I,J)),
p,
s)
= (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )
theorem
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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)),p,s)) = ((card I) + (card J)) + 3 & (
s . a > 0 implies ( ( for
d being
Int-Location holds
(IExec ((if>0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if>0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f ) ) ) & (
s . a <= 0 implies ( ( for
d being
Int-Location holds
(IExec ((if>0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if>0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f ) ) ) )
theorem Th55:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a < 0 &
I is_closed_onInit s,
p &
I is_halting_onInit s,
p holds
IExec (
(if<0 (a,I,J)),
p,
s)
= (IExec (I,p,s)) +* (Start-At (((((card I) + (card J)) + (card J)) + 7),SCM+FSA))
theorem Th56:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a = 0 &
J is_closed_onInit s,
p &
J is_halting_onInit s,
p holds
IExec (
(if<0 (a,I,J)),
p,
s)
= (IExec (J,p,s)) +* (Start-At (((((card I) + (card J)) + (card J)) + 7),SCM+FSA))
theorem Th57:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a > 0 &
J is_closed_onInit s,
p &
J is_halting_onInit s,
p holds
IExec (
(if<0 (a,I,J)),
p,
s)
= (IExec (J,p,s)) +* (Start-At (((((card I) + (card J)) + (card J)) + 7),SCM+FSA))
theorem Th58:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT 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)),
p,
s)
= (IExec (I,p,s)) +* (Start-At (((((card I) + (card J)) + (card J)) + 7),SCM+FSA)) ) & (
s . a >= 0 implies
IExec (
(if<0 (a,I,J)),
p,
s)
= (IExec (J,p,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 = Data-Locations SCM+FSA;
theorem Th63:
theorem Th64:
theorem Th65:
theorem
theorem
canceled;
theorem Th68:
theorem Th69:
theorem
theorem Th71:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_onInit s,
p &
I is_halting_onInit s,
p holds
(
CurInstr (
(p +* (loop I)),
(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((p +* I),(s +* (Initialize ((intloc 0) .--> 1))))))))
= goto 0 & ( for
m being
Element of
NAT st
m <= LifeSpan (
(p +* I),
(s +* (Initialize ((intloc 0) .--> 1)))) holds
CurInstr (
(p +* (loop I)),
(Comput ((p +* (loop I)),(s +* (Initialize ((intloc 0) .--> 1))),m)))
<> halt SCM+FSA ) )
theorem
canceled;
theorem Th73:
theorem
theorem
theorem
theorem Th77:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s being
State of
SCM+FSA for
I being
good InitHalting Program of
SCM+FSA for
a being
read-write Int-Location st not
I destroys a &
s . a > 0 holds
ex
s2 being
State of
SCM+FSA ex
p2 being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT ex
k being
Element of
NAT st
(
s2 = s +* (Initialize ((intloc 0) .--> 1)) &
p2 = p +* (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) &
k = (LifeSpan ((p +* (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 &
(Comput (p2,s2,k)) . a = (s . a) - 1 &
(Comput (p2,s2,k)) . (intloc 0) = 1 & ( for
b being
read-write Int-Location st
b <> a holds
(Comput (p2,s2,k)) . b = (IExec (I,p,s)) . b ) & ( for
f being
FinSeq-Location holds
(Comput (p2,s2,k)) . f = (IExec (I,p,s)) . f ) &
IC (Comput (p2,s2,k)) = 0 & ( for
n being
Element of
NAT st
n <= k holds
IC (Comput (p2,s2,n)) in dom (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))) ) )
theorem Th78:
theorem Th79:
for
p being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s being
State of
SCM+FSA for
I being
good InitHalting Program of
SCM+FSA for
a being
read-write Int-Location st not
I destroys a &
s . a > 0 holds
(
(IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 &
DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ';' (SubFrom (a,(intloc 0)))),p,s)))) )
theorem
theorem
theorem
theorem
:: deftheorem Def6 defines good SCM_HALT:def 6 :
for i being Instruction of SCM+FSA holds
( i is good iff not i destroys intloc 0 );