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