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

P +* (stop I) halts_on Initialize s by A1, SCMPDS_6:def 3;

hence contradiction by A2, A3, EXTPRO_1:def 15; :: thesis: verum

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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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)) ; :: thesis: 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 ; :: thesis: contradiction

P +* (stop I) halts_on Initialize s by A1, SCMPDS_6:def 3;

hence contradiction by A2, A3, EXTPRO_1:def 15; :: thesis: verum