set I = goto 0;
let W be Instruction of SCMPDS; :: thesis: ( W is halting implies W = goto 0 )
assume A1: W is halting ; :: thesis: W = goto 0
assume A2: goto 0 <> W ; :: thesis: contradiction
per cases ( ex k1 being Integer st W = goto k1 or ex a being Int_position st W = return a or ex a being Int_position ex k1 being Integer st W = saveIC (a,k1) or ex a being Int_position ex k1 being Integer st W = a := k1 or ex a being Int_position ex k1, k2 being Integer st W = (a,k1) := k2 or ex a being Int_position ex k1, k2 being Integer st W = (a,k1) <>0_goto k2 or ex a being Int_position ex k1, k2 being Integer st W = (a,k1) <=0_goto k2 or ex a being Int_position ex k1, k2 being Integer st W = (a,k1) >=0_goto k2 or ex a, b being Int_position ex k1, k2 being Integer st W = AddTo (a,k1,k2) or ex a, b being Int_position ex k1, k2 being Integer st W = AddTo (a,k1,b,k2) or ex a, b being Int_position ex k1, k2 being Integer st W = SubFrom (a,k1,b,k2) or ex a, b being Int_position ex k1, k2 being Integer st W = MultBy (a,k1,b,k2) or ex a, b being Int_position ex k1, k2 being Integer st W = Divide (a,k1,b,k2) or ex a, b being Int_position ex k1, k2 being Integer st W = (a,k1) := (b,k2) ) by Th91;
suppose ex k1 being Integer st W = goto k1 ; :: thesis: contradiction
hence contradiction by A1, A2, Th85; :: thesis: verum
end;
suppose ex a being Int_position st W = return a ; :: thesis: contradiction
hence contradiction by A1, Th89; :: thesis: verum
end;
suppose ex a being Int_position ex k1 being Integer st W = saveIC (a,k1) ; :: thesis: contradiction
hence contradiction by A1, Th90; :: thesis: verum
end;
suppose ex a being Int_position ex k1 being Integer st W = a := k1 ; :: thesis: contradiction
hence contradiction by A1, Th77; :: thesis: verum
end;
suppose ex a being Int_position ex k1, k2 being Integer st W = (a,k1) := k2 ; :: thesis: contradiction
hence contradiction by A1, Th78; :: thesis: verum
end;
suppose ex a being Int_position ex k1, k2 being Integer st W = (a,k1) <>0_goto k2 ; :: thesis: contradiction
hence contradiction by A1, Th86; :: thesis: verum
end;
suppose ex a being Int_position ex k1, k2 being Integer st W = (a,k1) <=0_goto k2 ; :: thesis: contradiction
hence contradiction by A1, Th87; :: thesis: verum
end;
suppose ex a being Int_position ex k1, k2 being Integer st W = (a,k1) >=0_goto k2 ; :: thesis: contradiction
hence contradiction by A1, Th88; :: thesis: verum
end;
suppose ex a, b being Int_position ex k1, k2 being Integer st W = AddTo (a,k1,k2) ; :: thesis: contradiction
hence contradiction by A1, Th80; :: thesis: verum
end;
suppose ex a, b being Int_position ex k1, k2 being Integer st W = AddTo (a,k1,b,k2) ; :: thesis: contradiction
hence contradiction by A1, Th81; :: thesis: verum
end;
suppose ex a, b being Int_position ex k1, k2 being Integer st W = SubFrom (a,k1,b,k2) ; :: thesis: contradiction
hence contradiction by A1, Th82; :: thesis: verum
end;
suppose ex a, b being Int_position ex k1, k2 being Integer st W = MultBy (a,k1,b,k2) ; :: thesis: contradiction
hence contradiction by A1, Th83; :: thesis: verum
end;
suppose ex a, b being Int_position ex k1, k2 being Integer st W = Divide (a,k1,b,k2) ; :: thesis: contradiction
hence contradiction by A1, Th84; :: thesis: verum
end;
suppose ex a, b being Int_position ex k1, k2 being Integer st W = (a,k1) := (b,k2) ; :: thesis: contradiction
hence contradiction by A1, Th79; :: thesis: verum
end;
end;