let N be with_zero set ; :: thesis: for i being Instruction of (STC N) st InsCode i = 1 holds
not i is halting
let i be Instruction of (STC N); :: thesis: ( InsCode i = 1 implies not i is halting )
set M = STC N;
set s = the State of (STC N);
assume InsCode i = 1 ; :: thesis: not i is halting
then A1: (Exec (i, the State of (STC N))) . (IC ) = (IC the State of (STC N)) + 1 by Lm3;
assume for s being State of (STC N) holds Exec (i,s) = s ; :: according to EXTPRO_1:def 3 :: thesis: contradiction
then (Exec (i, the State of (STC N))) . (IC ) = IC the State of (STC N) ;
hence contradiction by A1; :: thesis: verum