let N be non empty with_non-empty_elements 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 Instructions of (STC N) = {[1,0,0],[0,0,0]} by Def11;
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, RECDEF_2:def 1, 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 Object-Kind of (STC N) by CARD_3:107;
( ex f being Function of (product the Object-Kind of (STC N)),(product the Object-Kind of (STC N)) st
( ( for s being Element of product the Object-Kind of (STC N) holds f . s = s +* (0 .--> (succ (s . 0))) ) & the Execution of (STC N) = ([1,0,0] .--> f) +* ([0,0,0] .--> (id (product the Object-Kind of (STC N)))) ) & dom ([0,0,0] .--> (id (product the Object-Kind of (STC N)))) = {[0,0,0]} ) by Def11, FUNCOP_1:13;
then the Execution of (STC N) . i = ({[0,0,0]} --> (id (product the Object-Kind of (STC N)))) . i by A2, FUNCT_4:13
.= id (product the Object-Kind of (STC N)) by A2, FUNCOP_1:7 ;
then ( the Execution of (STC N) . i) . s = s by FUNCT_1:18;
hence Exec (i,s) = s ; :: thesis: verum