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

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