set I = [0,{},{}];
let W be Instruction of SCM; ( W is halting implies W = [0,{},{}] )
assume A1:
W is halting
; W = [0,{},{}]
assume A2:
[0,{},{}] <> W
; 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;
end;