let N be non empty with_non-empty_elements 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;
consider s being State of (STC N);
assume InsCode i = 1 ; :: thesis: not i is halting
then A1: (Exec i,s) . (IC (STC N)) = succ (IC s) by Lm4;
assume for s being State of (STC N) holds Exec i,s = s ; :: according to AMI_1:def 8 :: thesis: contradiction
then (Exec i,s) . (IC (STC N)) = IC s ;
hence contradiction by A1; :: thesis: verum