let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for I being parahalting Program of
for J being Program of st stop I c= P holds
for m being Nat st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (I ';' J)),s,m)
let s be 0 -started State of SCMPDS; for I being parahalting Program of
for J being Program of st stop I c= P holds
for m being Nat st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (I ';' J)),s,m)
let I be parahalting Program of ; for J being Program of st stop I c= P holds
for m being Nat st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (I ';' J)),s,m)
let J be Program of ; ( stop I c= P implies for m being Nat st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (I ';' J)),s,m) )
set SI = stop I;
defpred S1[ Nat] means ( $1 <= LifeSpan (P,s) implies Comput (P,s,$1) = Comput ((P +* (I ';' J)),s,$1) );
assume A1:
stop I c= P
; for m being Nat st m <= LifeSpan (P,s) holds
Comput (P,s,m) = Comput ((P +* (I ';' J)),s,m)
then A2:
P halts_on s
by SCMPDS_4:def 7;
A3:
for m being Nat st S1[m] holds
S1[m + 1]
proof
dom (I ';' J) = (dom I) \/ (dom (Shift (J,(card I))))
by FUNCT_4:def 1;
then A4:
dom I c= dom (I ';' J)
by XBOOLE_1:7;
let m be
Nat;
( S1[m] implies S1[m + 1] )
assume A5:
(
m <= LifeSpan (
P,
s) implies
Comput (
P,
s,
m)
= Comput (
(P +* (I ';' J)),
s,
m) )
;
S1[m + 1]
assume A6:
m + 1
<= LifeSpan (
P,
s)
;
Comput (P,s,(m + 1)) = Comput ((P +* (I ';' J)),s,(m + 1))
A7:
Comput (
(P +* (I ';' J)),
s,
(m + 1))
= Following (
(P +* (I ';' J)),
(Comput ((P +* (I ';' J)),s,m)))
by EXTPRO_1:3;
A8:
Comput (
P,
s,
(m + 1))
= Following (
P,
(Comput (P,s,m)))
by EXTPRO_1:3;
A9:
I ';' J c= P +* (I ';' J)
by FUNCT_4:25;
A10:
IC (Comput (P,s,m)) in dom (stop I)
by A1, SCMPDS_4:def 6;
A11:
P /. (IC (Comput (P,s,m))) = P . (IC (Comput (P,s,m)))
by PBOOLE:143;
A12:
CurInstr (
P,
(Comput (P,s,m)))
= (stop I) . (IC (Comput (P,s,m)))
by A10, A11, A1, GRFUNC_1:2;
A13:
(P +* (I ';' J)) /. (IC (Comput ((P +* (I ';' J)),s,m))) = (P +* (I ';' J)) . (IC (Comput ((P +* (I ';' J)),s,m)))
by PBOOLE:143;
m < LifeSpan (
P,
s)
by A6, NAT_1:13;
then
(stop I) . (IC (Comput (P,s,m))) <> halt SCMPDS
by A2, A12, EXTPRO_1:def 15;
then A14:
IC (Comput (P,s,m)) in dom I
by A10, COMPOS_1:51;
CurInstr (
P,
(Comput (P,s,m))) =
I . (IC (Comput (P,s,m)))
by A12, A14, AFINSQ_1:def 3
.=
(I ';' J) . (IC (Comput (P,s,m)))
by A14, AFINSQ_1:def 3
.=
CurInstr (
(P +* (I ';' J)),
(Comput ((P +* (I ';' J)),s,m)))
by A6, A9, A14, A4, A13, A5, GRFUNC_1:2, NAT_1:13
;
hence
Comput (
P,
s,
(m + 1))
= Comput (
(P +* (I ';' J)),
s,
(m + 1))
by A5, A6, A8, A7, NAT_1:13;
verum
end;
A15:
S1[ 0 ]
;
thus
for m being Nat holds S1[m]
from NAT_1:sch 2(A15, A3); verum