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

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 Element of NAT st W = goto i1,R or ex a being Data-Location of R ex i1 being Element of 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 Th8;

suppose W = [0 ,{} ,{} ] ; :: thesis: contradiction

hence contradiction by A2; :: thesis: verum

end;

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

hence contradiction by A1; :: thesis: verum

end;

suppose ex a, b being Data-Location of R st W = AddTo a,b ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

suppose ex a, b being Data-Location of R st W = SubFrom a,b ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

suppose ex a, b being Data-Location of R st W = MultBy a,b ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

suppose ex i1 being Element of NAT st W = goto i1,R ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

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

hence contradiction by A1; :: thesis: verum

end;

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

hence contradiction by A1; :: thesis: verum

end;

end;