set I = [0,{},{}];
let W be Instruction of SCM; :: 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 st W = a := b or ex a, b being Data-Location st W = AddTo (a,b) or ex a, b being Data-Location st W = SubFrom (a,b) or ex a, b being Data-Location st W = MultBy (a,b) or ex a, b being Data-Location st W = Divide (a,b) or ex loc being Nat st W = SCM-goto loc or ex a being Data-Location ex loc being Nat st W = a =0_goto loc or ex a being Data-Location ex loc being Nat st W = a >0_goto loc ) by Lm12;

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

hence contradiction by A2; :: thesis: verum

end;

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

hence contradiction by A1, Lm4; :: thesis: verum

end;

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

hence contradiction by A1, Lm5; :: thesis: verum

end;

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

hence contradiction by A1, Lm6; :: thesis: verum

end;

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

hence contradiction by A1, Lm7; :: thesis: verum

end;

suppose ex a, b being Data-Location st W = Divide (a,b) ; :: thesis: contradiction

hence contradiction by A1, Lm8; :: thesis: verum

end;

suppose ex loc being Nat st W = SCM-goto loc ; :: thesis: contradiction

hence contradiction by A1, Lm9; :: thesis: verum

end;

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

hence contradiction by A1, Lm10; :: thesis: verum

end;

suppose ex a being Data-Location ex loc being Nat st W = a >0_goto loc ; :: thesis: contradiction

hence contradiction by A1, Lm11; :: thesis: verum

end;

end;