let I be Instruction of SCM; :: thesis: ( I = [0,{},{}] implies I is halting )
assume Z: I = [0,{},{}] ; :: thesis: I is halting
then A1: I `3_3 = {} by RECDEF_2:def 3;
then A2: ( ( 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*>] ) ) by RECDEF_2:def 3;
A3: ( ( 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 A1, RECDEF_2:def 3;
I `2_3 = {} by Z, RECDEF_2:def 2;
then A4: ( ( 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*>,{}] ) ) by A1, RECDEF_2:def 2, RECDEF_2:def 3;
reconsider L = I as Element of SCM-Instr ;
let s be State of SCM; :: according to EXTPRO_1:def 3 :: thesis: Exec (I,s) = s
reconsider t = s as SCM-State by PBOOLE:155;
A5: ( ( 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*>] ) ) by A1, RECDEF_2:def 3;
thus Exec (I,s) = SCM-Exec-Res (L,t) by AMI_2:def 17
.= s by A2, A5, A4, A3, AMI_2:def 16 ; :: thesis: verum