let R be good Ring; :: thesis: for I being Instruction of (SCM R) st I = [0 ,{} ,{} ] holds
I is halting
let I be Instruction of (SCM R); :: thesis: ( I = [0 ,{} ,{} ] implies I is halting )
assume A1: I = [0 ,{} ,{} ] ; :: thesis: I is halting
A2: I `3_3 = {} by A1, RECDEF_2:def 3;
then A3: ( ( 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;
A4: for mk being Element of SCM-Data-Loc
for r being Element of R holds not I = [5,{} ,<*mk,r*>] by A2, RECDEF_2:def 3;
I `2_3 = {} by A1, RECDEF_2:def 2;
then A5: ( ( 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*>] ) ) by RECDEF_2:def 2;
reconsider L = I as Element of SCM-Instr R by A1, SCMRING1:22;
let s be State of (SCM R); :: according to AMI_1:def 8 :: thesis: Exec I,s = s
Y: the Object-Kind of (SCM R) = SCM-OK R by Def1;
reconsider t = s as SCM-State of R by Y, PBOOLE:155;
A6: ( ( 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 A2, RECDEF_2:def 3;
thus Exec I,s = SCM-Exec-Res L,t by Th12
.= s by A3, A6, A5, A4, SCMRING1:def 14 ; :: thesis: verum