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

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, Lm3; :: thesis: verum

end;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

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

hence contradiction by A1, Lm8; :: 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, 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;

end;