let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for I being Program of
for i being Nat st stop I c= P & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan (P,s) holds
IC (Comput (P,s,i)) in dom I
let s be 0 -started State of SCMPDS; for I being Program of
for i being Nat st stop I c= P & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan (P,s) holds
IC (Comput (P,s,i)) in dom I
let I be Program of ; for i being Nat st stop I c= P & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan (P,s) holds
IC (Comput (P,s,i)) in dom I
let i be Nat; ( stop I c= P & I is_closed_on s,P & I is_halting_on s,P & i < LifeSpan (P,s) implies IC (Comput (P,s,i)) in dom I )
set sI = stop I;
set Ci = Comput (P,s,i);
set Lc = IC (Comput (P,s,i));
assume that
A1:
stop I c= P
and
A2:
I is_closed_on s,P
and
A3:
I is_halting_on s,P
and
A4:
i < LifeSpan (P,s)
; IC (Comput (P,s,i)) in dom I
A5:
Start-At (0,SCMPDS) c= s
by MEMSTR_0:29;
A6:
P +* (stop I) = P
by A1, FUNCT_4:98;
A7:
s = Initialize s
by A5, FUNCT_4:98;
then A8:
IC (Comput (P,s,i)) in dom (stop I)
by A2, A6, SCMPDS_6:def 2;
A9:
P halts_on s
by A3, A7, A6, SCMPDS_6:def 3;
now not (stop I) . (IC (Comput (P,s,i))) = halt SCMPDSassume A10:
(stop I) . (IC (Comput (P,s,i))) = halt SCMPDS
;
contradiction CurInstr (
P,
(Comput (P,s,i))) =
P . (IC (Comput (P,s,i)))
by PBOOLE:143
.=
halt SCMPDS
by A8, A1, A10, GRFUNC_1:2
;
hence
contradiction
by A4, A9, EXTPRO_1:def 15;
verum end;
hence
IC (Comput (P,s,i)) in dom I
by A8, COMPOS_1:51; verum