begin
set SA0 = Start-At (0,SCM+FSA);
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
Lm1:
not IC in NAT
by COMPOS_1:3;
theorem
canceled;
theorem
canceled;
theorem Th8:
theorem Th9:
theorem Th10:
theorem
canceled;
theorem Th12:
theorem Th13:
begin
begin
:: deftheorem defines IExec SCMFSA6B:def 1 :
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 IExec (I,P,s) = (Result ((P +* I),(s +* (Initialized I)))) +* (s | NAT);
:: deftheorem Def2 defines paraclosed SCMFSA6B:def 2 :
for I being Program of SCM+FSA holds
( I is paraclosed 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 I c= s holds
IC (Comput (P,s,n)) in dom I );
:: deftheorem Def3 defines parahalting SCMFSA6B:def 3 :
for I being Program of SCM+FSA holds
( I is parahalting iff Initialize I is halting );
:: deftheorem Def4 defines keeping_0 SCMFSA6B:def 4 :
for I being Program of SCM+FSA holds
( I is keeping_0 iff for s being State of SCM+FSA st Initialize I 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) = s . (intloc 0) );
Lm2:
Macro (halt SCM+FSA) is parahalting
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th18:
theorem Th19:
theorem Th20:
theorem
canceled;
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem Th27:
for
s1,
s2 being
State of
SCM+FSA for
P,
Q being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
J being
parahalting Program of
SCM+FSA st
Initialize J c= s1 &
J c= P holds
for
n being
Element of
NAT st
Reloc (
J,
n)
c= Q &
IC s2 = n &
DataPart s1 = DataPart s2 holds
for
i being
Element of
NAT holds
(
(IC (Comput (P,s1,i))) + n = IC (Comput (Q,s2,i)) &
IncAddr (
(CurInstr (P,(Comput (P,s1,i)))),
n)
= CurInstr (
Q,
(Comput (Q,s2,i))) &
DataPart (Comput (P,s1,i)) = DataPart (Comput (Q,s2,i)) )
theorem Th28:
for
s1,
s2 being
State of
SCM+FSA for
P1,
P2 being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
I being
parahalting Program of
SCM+FSA st
I c= P1 &
I c= P2 &
Initialize I c= s1 &
Initialize I c= s2 &
s1,
s2 equal_outside NAT holds
for
k being
Element of
NAT holds
(
Comput (
P1,
s1,
k),
Comput (
P2,
s2,
k)
equal_outside NAT &
CurInstr (
P1,
(Comput (P1,s1,k)))
= CurInstr (
P2,
(Comput (P2,s2,k))) )
theorem Th29:
theorem Th30:
theorem
theorem
canceled;
theorem
theorem
Lm3:
Macro (halt SCM+FSA) is keeping_0
Lm4:
for I being Program of SCM+FSA holds Initialize I c= Initialized I
theorem
begin
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
Lm5:
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being parahalting keeping_0 Program of SCM+FSA
for J being parahalting Program of SCM+FSA
for s being State of SCM+FSA st I ';' J c= P & Initialized (I ';' J) c= s holds
( IC (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = card I & DataPart (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) = DataPart ((Comput ((P +* I),(s +* I),(LifeSpan ((P +* I),(s +* I))))) +* (Initialized J)) & Reloc (J,(card I)) c= P & (Comput (P,s,((LifeSpan ((P +* I),(s +* I))) + 1))) . (intloc 0) = 1 & P halts_on s & LifeSpan (P,s) = ((LifeSpan ((P +* I),(s +* I))) + 1) + (LifeSpan (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialized J)))) & ( J is keeping_0 implies (Result (P,s)) . (intloc 0) = 1 ) )
theorem Th41:
theorem Th42:
for
s being
State of
SCM+FSA for
P being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
I being
keeping_0 Program of
SCM+FSA st
P +* I halts_on s +* I holds
for
J being
paraclosed Program of
SCM+FSA st
I ';' J c= P &
Initialize (I ';' J) c= s holds
for
k being
Element of
NAT holds
(Comput (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialize J)),k)) +* (Start-At (((IC (Comput (((P +* I) +* J),((Result ((P +* I),(s +* I))) +* (Initialize J)),k))) + (card I)),SCM+FSA)),
Comput (
(P +* (I ';' J)),
(s +* (I ';' J)),
(((LifeSpan ((P +* I),(s +* I))) + 1) + k))
equal_outside NAT
theorem Th43:
theorem
for
s being
State of
SCM+FSA for
P being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
I being
parahalting keeping_0 Program of
SCM+FSA for
J being
parahalting Program of
SCM+FSA holds
IExec (
(I ';' J),
P,
s)
= (IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCM+FSA))
theorem