let P be Instruction-Sequence of SCMPDS; for I being Program of
for s being State of SCMPDS
for k being Nat st I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS
let I be Program of ; for s being State of SCMPDS
for k being Nat st I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS
let s be State of SCMPDS; for k being Nat st I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) holds
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS
let k be Nat; ( I is_halting_on s,P & k < LifeSpan ((P +* (stop I)),(Initialize s)) implies CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS )
set ss = Initialize s;
set PP = P +* (stop I);
set m = LifeSpan ((P +* (stop I)),(Initialize s));
assume that
A1:
I is_halting_on s,P
and
A2:
k < LifeSpan ((P +* (stop I)),(Initialize s))
; CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) <> halt SCMPDS
assume A3:
CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),k))) = halt SCMPDS
; contradiction
P +* (stop I) halts_on Initialize s
by A1, SCMPDS_6:def 3;
hence
contradiction
by A2, A3, EXTPRO_1:def 15; verum