let I be Program of ; :: thesis: for s being State of
for k being Element of NAT st I is_halting_on s & k < LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (Computation (s +* (Initialized (stop I))),k) <> halt SCMPDS
let s be State of ; :: thesis: for k being Element of NAT st I is_halting_on s & k < LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (Computation (s +* (Initialized (stop I))),k) <> halt SCMPDS
let k be Element of NAT ; :: thesis: ( I is_halting_on s & k < LifeSpan (s +* (Initialized (stop I))) implies CurInstr (Computation (s +* (Initialized (stop I))),k) <> halt SCMPDS )
set ss = s +* (Initialized (stop I));
set m = LifeSpan (s +* (Initialized (stop I)));
assume that
A1: I is_halting_on s and
A2: k < LifeSpan (s +* (Initialized (stop I))) ; :: thesis: CurInstr (Computation (s +* (Initialized (stop I))),k) <> halt SCMPDS
assume A3: CurInstr (Computation (s +* (Initialized (stop I))),k) = halt SCMPDS ; :: thesis: contradiction
ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I)) by A1, SCMPDS_6:def 3;
hence contradiction by A2, A3, AMI_1:def 46; :: thesis: verum