let R be 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;

then A3: ( ( for mk, ml being Element of Data-Locations holds not I = [1,{},<*mk,ml*>] ) & ( for mk, ml being Element of Data-Locations holds not I = [2,{},<*mk,ml*>] ) ) ;

A4: for mk being Element of Data-Locations

for r being Element of R holds not I = [5,{},<*mk,r*>] by A2;

I `2_3 = {} by A1;

then A5: ( ( for mk being Element of NAT holds not I = [6,<*mk*>,{}] ) & ( for mk being Element of NAT

for ml being Element of Data-Locations holds not I = [7,<*mk*>,<*ml*>] ) ) ;

reconsider L = I as Element of SCM-Instr R by A1, SCMRINGI:6;

let s be State of (SCM R); :: according to EXTPRO_1:def 3 :: thesis: Exec (I,s) = s

A6: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1;

reconsider t = s as SCM-State of R by A6, CARD_3:107;

A7: ( ( for mk, ml being Element of Data-Locations holds not I = [3,{},<*mk,ml*>] ) & ( for mk, ml being Element of Data-Locations holds not I = [4,{},<*mk,ml*>] ) ) by A2;

thus Exec (I,s) = SCM-Exec-Res (L,t) by Th10

.= s by A3, A7, A5, A4, AMI_3:27, SCMRING1:def 14 ; :: thesis: verum

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;

then A3: ( ( for mk, ml being Element of Data-Locations holds not I = [1,{},<*mk,ml*>] ) & ( for mk, ml being Element of Data-Locations holds not I = [2,{},<*mk,ml*>] ) ) ;

A4: for mk being Element of Data-Locations

for r being Element of R holds not I = [5,{},<*mk,r*>] by A2;

I `2_3 = {} by A1;

then A5: ( ( for mk being Element of NAT holds not I = [6,<*mk*>,{}] ) & ( for mk being Element of NAT

for ml being Element of Data-Locations holds not I = [7,<*mk*>,<*ml*>] ) ) ;

reconsider L = I as Element of SCM-Instr R by A1, SCMRINGI:6;

let s be State of (SCM R); :: according to EXTPRO_1:def 3 :: thesis: Exec (I,s) = s

A6: the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1;

reconsider t = s as SCM-State of R by A6, CARD_3:107;

A7: ( ( for mk, ml being Element of Data-Locations holds not I = [3,{},<*mk,ml*>] ) & ( for mk, ml being Element of Data-Locations holds not I = [4,{},<*mk,ml*>] ) ) by A2;

thus Exec (I,s) = SCM-Exec-Res (L,t) by Th10

.= s by A3, A7, A5, A4, AMI_3:27, SCMRING1:def 14 ; :: thesis: verum