let P be Instruction-Sequence of SCMPDS; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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;

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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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 :: thesis: not (stop I) . (IC (Comput (P,s,i))) = halt SCMPDS

hence
IC (Comput (P,s,i)) in dom I
by A8, COMPOS_1:51; :: thesis: verumassume A10:
(stop I) . (IC (Comput (P,s,i))) = halt SCMPDS
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum