let R be Ring; :: thesis: for W being Instruction of (SCM R) st W is halting holds

W = [0,{},{}]

set I = [0,{},{}];

let W be Instruction of (SCM R); :: thesis: ( W is halting implies W = [0,{},{}] )

assume A1: W is halting ; :: thesis: W = [0,{},{}]

assume A2: [0,{},{}] <> W ; :: thesis: contradiction

W = [0,{},{}]

set I = [0,{},{}];

let W be Instruction of (SCM R); :: thesis: ( W is halting implies W = [0,{},{}] )

assume A1: W is halting ; :: thesis: W = [0,{},{}]

assume A2: [0,{},{}] <> W ; :: thesis: contradiction

per cases
( W = [0,{},{}] or ex a, b being Data-Location of R st W = a := b or ex a, b being Data-Location of R st W = AddTo (a,b) or ex a, b being Data-Location of R st W = SubFrom (a,b) or ex a, b being Data-Location of R st W = MultBy (a,b) or ex i1 being Nat st W = goto (i1,R) or ex a being Data-Location of R ex i1 being Nat st W = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st W = a := r )
by Th7;

end;

suppose
ex a being Data-Location of R ex i1 being Nat st W = a =0_goto i1
; :: thesis: contradiction

end;

end;

suppose
ex a being Data-Location of R ex r being Element of R st W = a := r
; :: thesis: contradiction

end;

end;