let I be Instruction of SCM ; :: thesis: ( I = [0 ,{} ] implies I is halting )
assume A1: I = [0 ,{} ] ; :: thesis: I is halting
let s be State of SCM ; :: according to AMI_1:def 8 :: thesis: Exec I,s = s
reconsider L = I as Element of SCM-Instr ;
A2: I `2 = {} by A1, MCART_1:7;
A3: for i being Element of NAT
for mk, ml being Element of SCM-Data-Loc holds not I = [i,<*mk,ml*>] by A2, FINSEQ_3:38, MCART_1:7;
A4: for i, mk being Element of NAT holds not I = [i,<*mk*>] by A2, MCART_1:7, TREES_1:4;
for i, mk being Element of NAT
for ml being Element of SCM-Data-Loc holds not I = [i,<*mk,ml*>] by A2, FINSEQ_3:38, MCART_1:7;
then A5: ( ( for mk, ml being Element of SCM-Data-Loc holds not I = [1,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not I = [2,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not I = [3,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not I = [4,<*mk,ml*>] ) & ( for mk, ml being Element of SCM-Data-Loc holds not I = [5,<*mk,ml*>] ) & ( for mk being Element of NAT holds not I = [6,<*mk*>] ) & ( for mk being Element of NAT
for ml being Element of SCM-Data-Loc holds not I = [7,<*mk,ml*>] ) & ( for mk being Element of NAT
for ml being Element of SCM-Data-Loc holds not I = [8,<*mk,ml*>] ) ) by A3, A4;
reconsider t = s as SCM-State ;
thus Exec I,s = SCM-Exec-Res L,t by AMI_2:def 17
.= s by A5, AMI_2:def 16 ; :: thesis: verum