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

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