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 ]} by Def11;
then A1: ( i = [1,0 ] or i = [0 ,0 ] ) by TARSKI:def 2;
assume InsCode i = 0 ; :: thesis: i is halting
then A2: i in {[0 ,0 ]} by A1, MCART_1:7, TARSKI:def 1;
let s be State of (STC N); :: according to AMI_1:def 8 :: thesis: Exec i,s = s
reconsider s = s as Element of product the Object-Kind of (STC N) by PBOOLE:155;
( 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 +* (NAT .--> (succ (s . NAT ))) ) & the Execution of (STC N) = ([1,0 ] .--> f) +* ([0 ,0 ] .--> (id (product the Object-Kind of (STC N)))) ) & dom ([0 ,0 ] .--> (id (product the Object-Kind of (STC N)))) = {[0 ,0 ]} ) by Def11, FUNCOP_1:19;
then the Execution of (STC N) . i = ({[0 ,0 ]} --> (id (product the Object-Kind of (STC N)))) . i by A2, FUNCT_4:14
.= id (product the Object-Kind of (STC N)) by A2, FUNCOP_1:13 ;
then (the Execution of (STC N) . i) . s = s by FUNCT_1:35;
hence Exec i,s = s ; :: thesis: verum