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
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;
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 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 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;