begin
set SA0 = Start-At (0,SCM+FSA);
set Q = (intloc 0) .--> 1;
theorem
canceled;
theorem Th2:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem
theorem Th24:
theorem
canceled;
theorem
theorem Th27:
theorem Th28:
theorem
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem
canceled;
theorem
canceled;
theorem Th36:
theorem
canceled;
theorem Th38:
theorem Th39:
theorem
canceled;
theorem
canceled;
theorem Th42:
for
P1,
P2 being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s1,
P1 &
Initialize I c= s1 &
I c= P1 holds
for
n being
Element of
NAT st
Reloc (
I,
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 Th43:
for
P1,
P2 being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s1,
P1 &
Initialize I c= s1 &
Initialize I c= s2 &
I c= P1 &
I c= P2 &
DataPart s1 = DataPart s2 holds
for
i being
Element of
NAT holds
(
IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) &
CurInstr (
P1,
(Comput (P1,s1,i)))
= CurInstr (
P2,
(Comput (P2,s2,i))) &
DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) )
theorem Th44:
theorem Th45:
theorem Th46:
Lm1:
now
let P be the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT ;
for s being State of SCM+FSA
for I being Program of SCM+FSA holds
( ( Initialized I is_pseudo-closed_on s,P implies ( I is_pseudo-closed_on Initialized s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) ) ) & ( I is_pseudo-closed_on Initialized s,P implies ( Initialized I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) ) ) )let s be
State of
SCM+FSA;
for I being Program of SCM+FSA holds
( ( Initialized I is_pseudo-closed_on s,P implies ( I is_pseudo-closed_on Initialized s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) ) ) & ( I is_pseudo-closed_on Initialized s,P implies ( Initialized I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) ) ) )let I be
Program of
SCM+FSA;
( ( Initialized I is_pseudo-closed_on s,P implies ( I is_pseudo-closed_on Initialized s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) ) ) & ( I is_pseudo-closed_on Initialized s,P implies ( Initialized I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) ) ) )set k =
pseudo-LifeSpan (
(Initialized s),
P,
I);
A1:
ProgramPart (Initialized I) = I
by SCMFSA6A:33;
A2:
ProgramPart I = I
by RELAT_1:209;
hereby ( I is_pseudo-closed_on Initialized s,P implies ( Initialized I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) ) )
set k =
pseudo-LifeSpan (
s,
P,
(Initialized I));
A3:
s +* (Initialize (Initialized I)) = (Initialized s) +* (Initialize I)
by Th16;
assume A4:
Initialized I is_pseudo-closed_on s,
P
;
( I is_pseudo-closed_on Initialized s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) )then
IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),(pseudo-LifeSpan (s,P,(Initialized I))))) = card I
by SCMFSA8A:def 5, A1;
then
IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),(pseudo-LifeSpan (s,P,(Initialized I))))) = card I
by A3;
then A5:
IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),(pseudo-LifeSpan (s,P,(Initialized I))))) = card (ProgramPart I)
by RELAT_1:209;
A6:
now
let n be
Element of
NAT ;
( n < pseudo-LifeSpan (s,P,(Initialized I)) implies IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),n)) in dom I )A7:
s +* (Initialize (Initialized I)) = (Initialized s) +* (Initialize I)
by Th16;
assume
n < pseudo-LifeSpan (
s,
P,
(Initialized I))
;
IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),n)) in dom Ithen
IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),n)) in dom (Initialized I)
by A4, SCMFSA8A:def 5, A1;
then
IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),n)) in dom (Initialized I)
by A7;
hence
IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),n)) in dom I
by Th20;
verum
end;
hence A8:
I is_pseudo-closed_on Initialized s,
P
by A5, SCMFSA8A:def 3, A2;
pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I)
for
n being
Element of
NAT st not
IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),n)) in dom I holds
pseudo-LifeSpan (
s,
P,
(Initialized I))
<= n
by A6;
hence
pseudo-LifeSpan (
s,
P,
(Initialized I))
= pseudo-LifeSpan (
(Initialized s),
P,
I)
by A5, A8, SCMFSA8A:def 5, A2;
verum
end;
A9:
s +* (Initialize (Initialized I)) = (Initialized s) +* (Initialize I)
by Th16;
assume A10:
I is_pseudo-closed_on Initialized s,
P
;
( Initialized I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I) )then
IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),(pseudo-LifeSpan ((Initialized s),P,I)))) = card (ProgramPart I)
by SCMFSA8A:def 5, A2;
then
IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),(pseudo-LifeSpan ((Initialized s),P,I)))) = card (ProgramPart I)
by A9;
then A11:
IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),(pseudo-LifeSpan ((Initialized s),P,I)))) = card I
by RELAT_1:209;
A12:
now
let n be
Element of
NAT ;
( n < pseudo-LifeSpan ((Initialized s),P,I) implies IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),n)) in dom (Initialized I) )A13:
s +* (Initialize (Initialized I)) = (Initialized s) +* (Initialize I)
by Th16;
assume
n < pseudo-LifeSpan (
(Initialized s),
P,
I)
;
IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),n)) in dom (Initialized I)then
IC (Comput ((P +* I),((Initialized s) +* (Initialize I)),n)) in dom I
by A10, SCMFSA8A:def 5, A2;
then
IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),n)) in dom I
by A13;
hence
IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),n)) in dom (Initialized I)
by Th20;
verum
end;
hence A14:
Initialized I is_pseudo-closed_on s,
P
by A11, SCMFSA8A:def 3, A1;
pseudo-LifeSpan (s,P,(Initialized I)) = pseudo-LifeSpan ((Initialized s),P,I)
for
n being
Element of
NAT st not
IC (Comput ((P +* I),(s +* (Initialize (Initialized I))),n)) in dom (Initialized I) holds
pseudo-LifeSpan (
(Initialized s),
P,
I)
<= n
by A12;
hence
pseudo-LifeSpan (
s,
P,
(Initialized I))
= pseudo-LifeSpan (
(Initialized s),
P,
I)
by A11, A14, SCMFSA8A:def 5, A1;
verum
end;
theorem
theorem
theorem
theorem Th50:
theorem Th51:
for
P1,
P2 being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
Initialize I c= s1 &
I c= P1 &
I is_pseudo-closed_on s1,
P1 holds
for
n being
Element of
NAT st
Reloc (
I,
n)
c= s2 &
Reloc (
I,
n)
c= P2 &
IC s2 = n &
DataPart s1 = DataPart s2 holds
( ( for
i being
Element of
NAT st
i < pseudo-LifeSpan (
s1,
P1,
I) holds
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
n)
= CurInstr (
P2,
(Comput (P2,s2,i))) ) & ( for
i being
Element of
NAT st
i <= pseudo-LifeSpan (
s1,
P1,
I) holds
(
(IC (Comput (P1,s1,i))) + n = IC (Comput (P2,s2,i)) &
DataPart (Comput (P1,s1,i)) = DataPart (Comput (P2,s2,i)) ) ) )
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
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
Directed I is_pseudo-closed_on s,
P holds
(
I ';' (Stop SCM+FSA) is_closed_on s,
P &
I ';' (Stop SCM+FSA) is_halting_on s,
P &
LifeSpan (
(P +* (I ';' (Stop SCM+FSA))),
(s +* (Initialize (I ';' (Stop SCM+FSA)))))
= pseudo-LifeSpan (
s,
P,
(Directed I)) & ( for
n being
Element of
NAT st
n < pseudo-LifeSpan (
s,
P,
(Directed I)) holds
IC (Comput ((P +* I),(s +* (Initialize I)),n)) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) & ( for
n being
Element of
NAT st
n <= pseudo-LifeSpan (
s,
P,
(Directed I)) holds
DataPart (Comput ((P +* I),(s +* (Initialize I)),n)) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),n)) ) )
theorem Th59:
theorem
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
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 &
Directed I is_pseudo-closed_on s,
P holds
(
if=0 (
a,
I,
J)
is_halting_on s,
P &
if=0 (
a,
I,
J)
is_closed_on s,
P &
LifeSpan (
(P +* (if=0 (a,I,J))),
(s +* (Initialize (if=0 (a,I,J)))))
= (LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))) + 1 )
theorem
theorem Th68:
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 &
Directed I is_pseudo-closed_on s,
P holds
(
if>0 (
a,
I,
J)
is_halting_on s,
P &
if>0 (
a,
I,
J)
is_closed_on s,
P &
LifeSpan (
(P +* (if>0 (a,I,J))),
(s +* (Initialize (if>0 (a,I,J)))))
= (LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))) + 1 )
theorem Th69:
theorem Th70:
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 &
Directed J is_pseudo-closed_on s,
P holds
(
if=0 (
a,
I,
J)
is_halting_on s,
P &
if=0 (
a,
I,
J)
is_closed_on s,
P &
LifeSpan (
(P +* (if=0 (a,I,J))),
(s +* (Initialize (if=0 (a,I,J)))))
= (LifeSpan ((P +* (J ';' (Stop SCM+FSA))),(s +* (Initialize (J ';' (Stop SCM+FSA)))))) + 3 )
theorem
theorem Th72:
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 &
Directed J is_pseudo-closed_on s,
P holds
(
if>0 (
a,
I,
J)
is_halting_on s,
P &
if>0 (
a,
I,
J)
is_closed_on s,
P &
LifeSpan (
(P +* (if>0 (a,I,J))),
(s +* (Initialize (if>0 (a,I,J)))))
= (LifeSpan ((P +* (J ';' (Stop SCM+FSA))),(s +* (Initialize (J ';' (Stop SCM+FSA)))))) + 3 )
theorem Th73:
theorem
theorem
theorem
theorem Th77:
theorem Th78:
theorem
theorem
theorem Th81:
theorem Th82:
theorem
theorem
theorem Th85:
theorem Th86:
theorem Th87:
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_halting_on Initialized s,
P holds
( ( for
a being
read-write Int-Location holds
(IExec (I,P,s)) . a = (Comput ((P +* I),((Initialized s) +* (Initialize I)),(LifeSpan ((P +* I),((Initialized s) +* (Initialize I)))))) . a ) & ( for
f being
FinSeq-Location holds
(IExec (I,P,s)) . f = (Comput ((P +* I),((Initialized s) +* (Initialize I)),(LifeSpan ((P +* I),((Initialized s) +* (Initialize I)))))) . f ) )
theorem Th88:
theorem Th89:
theorem Th90:
theorem Th91:
theorem Th92:
theorem Th93:
theorem Th94:
theorem Th95:
theorem Th96:
theorem
theorem Th98:
theorem Th99:
theorem Th100:
for
P1,
P2 being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s1,
P1 &
I is_halting_on s1,
P1 &
DataPart s1 = DataPart s2 holds
for
k being
Element of
NAT holds
(
Comput (
(P1 +* I),
(s1 +* (Initialize I)),
k),
Comput (
(P2 +* I),
(s2 +* (Initialize I)),
k)
equal_outside NAT &
CurInstr (
(P1 +* I),
(Comput ((P1 +* I),(s1 +* (Initialize I)),k)))
= CurInstr (
(P2 +* I),
(Comput ((P2 +* I),(s2 +* (Initialize I)),k))) )
theorem Th101:
theorem
canceled;
theorem Th103:
for
P1,
P2 being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s1,
P1 &
I is_halting_on s1,
P1 &
Initialize I c= s1 &
Initialize I c= s2 &
I c= P1 &
I c= P2 & ex
k being
Element of
NAT st
Comput (
P1,
s1,
k),
s2 equal_outside NAT holds
Result (
P1,
s1),
Result (
P2,
s2)
equal_outside NAT
begin
:: deftheorem SCMFSA8C:def 1 :
canceled;
:: deftheorem SCMFSA8C:def 2 :
canceled;
:: deftheorem SCMFSA8C:def 3 :
canceled;
:: deftheorem defines loop SCMFSA8C:def 4 :
for I being Program of SCM+FSA holds loop I = Directed (I,0);
theorem
canceled;
theorem
theorem
canceled;
theorem Th107:
theorem
canceled;
theorem Th109:
theorem Th110:
Lm2:
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_on s,P & I is_halting_on s,P holds
( CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),(LifeSpan ((P +* I),(s +* (Initialize I))))))) = goto 0 & ( for m being Element of NAT st m <= LifeSpan ((P +* I),(s +* (Initialize I))) holds
CurInstr ((P +* (loop I)),(Comput ((P +* (loop I)),(s +* (Initialize (loop I))),m))) <> halt SCM+FSA ) )
theorem
theorem
theorem Th113:
theorem
begin
definition
let a be
Int-Location ;
let I be
Program of
SCM+FSA;
func Times (
a,
I)
-> Program of
SCM+FSA equals
if>0 (
a,
(loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),
(Stop SCM+FSA));
correctness
coherence
if>0 (a,(loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Stop SCM+FSA)) is Program of SCM+FSA;
;
end;
:: deftheorem defines Times SCMFSA8C:def 5 :
for a being Int-Location
for I being Program of SCM+FSA holds Times (a,I) = if>0 (a,(loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))))),(Stop SCM+FSA));
theorem Th115:
theorem Th116:
theorem Th117:
theorem
theorem
theorem
theorem
theorem Th122:
for
P being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s being
State of
SCM+FSA for
I being
parahalting good Program of
SCM+FSA for
a being
read-write Int-Location st not
I destroys a &
s . (intloc 0) = 1 &
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 (loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))) &
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 (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))))))) + 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 Th123:
theorem Th124:
for
P being the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT for
s being
State of
SCM+FSA for
I being
parahalting good 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)))) )
begin
theorem