let N be with_zero set ; :: thesis: for i being Instruction of (STC N) st InsCode i = 0 holds
i is halting
let i be Instruction of (STC N); :: thesis: ( InsCode i = 0 implies i is halting )
set M = STC N;
the InstructionsF of (STC N) = {[1,{},{}],[0,{},{}]} by Def7;
then A1: ( i = [1,0,0] or i = [0,0,0] ) by TARSKI:def 2;
assume InsCode i = 0 ; :: thesis: i is halting
then A2: i in {[0,0,0]} by A1, TARSKI:def 1;
let s be State of (STC N); :: according to EXTPRO_1:def 3 :: thesis: Exec (i,s) = s
reconsider s = s as Element of product (the_Values_of (STC N)) by CARD_3:107;
( ex f being Function of (product (the_Values_of (STC N))),(product (the_Values_of (STC N))) st
( ( for s being Element of product (the_Values_of (STC N)) holds f . s = s +* (0 .--> ((In ((s . 0),NAT)) + 1)) ) & the Execution of (STC N) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product (the_Values_of (STC N))))) ) & dom ([0,0,0] .--> (id (product (the_Values_of (STC N))))) = {[0,0,0]} ) by Def7;
then the Execution of (STC N) . i = ([0,0,0] .--> (id (product (the_Values_of (STC N))))) . i by A2, FUNCT_4:13
.= id (product (the_Values_of (STC N))) by A2, FUNCOP_1:7 ;
then ( the Execution of (STC N) . i) . s = s ;
hence Exec (i,s) = s ; :: thesis: verum