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;