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