set I2 = (GBP := 0) ';' (SBP := 7);
set I3 = ((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC));
set I4 = (((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2);
set I5 = ((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS);
set I6 = (((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9);
set I7 = ((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3));
set I8 = (((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3));
set I9 = ((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3));
set I10 = (((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1));
set I11 = ((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' (AddTo (GBP,1,4));
set I12 = (((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' (saveIC (SBP,RetIC));
set I13 = ((((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' (saveIC (SBP,RetIC))) ';' (goto (- 7));
set I14 = (((((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' (saveIC (SBP,RetIC))) ';' (goto (- 7))) ';' ((SBP,2) := (SBP,6));
A1: card ((GBP := 0) ';' (SBP := 7)) = 2 by Th5;
then A2: card (((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) = 2 + 1 by Th4;
then A3: card ((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) = 3 + 1 by Th4;
then A4: card (((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) = 4 + 1 by Th4;
then A5: card ((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) = 5 + 1 by Th4;
then A6: card (((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) = 6 + 1 by Th4;
then A7: card ((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) = 7 + 1 by Th4;
then A8: card (((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) = 8 + 1 by Th4;
then A9: card ((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) = 9 + 1 by Th4;
then A10: card (((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' (AddTo (GBP,1,4))) = 10 + 1 by Th4;
then A11: card ((((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' (saveIC (SBP,RetIC))) = 11 + 1 by Th4;
then A12: card (((((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' (saveIC (SBP,RetIC))) ';' (goto (- 7))) = 12 + 1 by Th4;
then A13: card ((((((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' (saveIC (SBP,RetIC))) ';' (goto (- 7))) ';' ((SBP,2) := (SBP,6))) = 13 + 1 by Th4;
set J14 = ((SBP,2) := (SBP,6)) ';' (return SBP);
set J13 = (goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP));
set J12 = (saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP)));
set J11 = (AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP))));
set J10 = ((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP)))));
set J9 = ((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP))))));
set J8 = (Divide (SBP,2,SBP,3)) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP)))))));
set J7 = ((SBP,6) := (SBP,3)) ';' ((Divide (SBP,2,SBP,3)) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP))))))));
set J6 = ((SBP,3) <=0_goto 9) ';' (((SBP,6) := (SBP,3)) ';' ((Divide (SBP,2,SBP,3)) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP)))))))));
set J5 = (halt SCMPDS) ';' (((SBP,3) <=0_goto 9) ';' (((SBP,6) := (SBP,3)) ';' ((Divide (SBP,2,SBP,3)) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP))))))))));
set J4 = (goto 2) ';' ((halt SCMPDS) ';' (((SBP,3) <=0_goto 9) ';' (((SBP,6) := (SBP,3)) ';' ((Divide (SBP,2,SBP,3)) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP)))))))))));
set J3 = (saveIC (SBP,RetIC)) ';' ((goto 2) ';' ((halt SCMPDS) ';' (((SBP,3) <=0_goto 9) ';' (((SBP,6) := (SBP,3)) ';' ((Divide (SBP,2,SBP,3)) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP))))))))))));
set J2 = (SBP := 7) ';' ((saveIC (SBP,RetIC)) ';' ((goto 2) ';' ((halt SCMPDS) ';' (((SBP,3) <=0_goto 9) ';' (((SBP,6) := (SBP,3)) ';' ((Divide (SBP,2,SBP,3)) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP)))))))))))));
A14: GCD-Algorithm = (((((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' (saveIC (SBP,RetIC))) ';' (goto (- 7))) ';' (((SBP,2) := (SBP,6)) ';' (return SBP)) by SCMPDS_4:13;
then A15: GCD-Algorithm = ((((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' (saveIC (SBP,RetIC))) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP))) by SCMPDS_4:12;
then A16: GCD-Algorithm = (((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP)))) by SCMPDS_4:12;
then A17: GCD-Algorithm = ((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP))))) by SCMPDS_4:12;
then A18: GCD-Algorithm = (((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP)))))) by SCMPDS_4:12;
then A19: GCD-Algorithm = ((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP))))))) by SCMPDS_4:12;
then A20: GCD-Algorithm = (((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' ((Divide (SBP,2,SBP,3)) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP)))))))) by SCMPDS_4:12;
then A21: GCD-Algorithm = ((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' (((SBP,6) := (SBP,3)) ';' ((Divide (SBP,2,SBP,3)) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP))))))))) by SCMPDS_4:12;
then A22: GCD-Algorithm = (((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' (((SBP,3) <=0_goto 9) ';' (((SBP,6) := (SBP,3)) ';' ((Divide (SBP,2,SBP,3)) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP)))))))))) by SCMPDS_4:12;
then A23: GCD-Algorithm = ((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' ((halt SCMPDS) ';' (((SBP,3) <=0_goto 9) ';' (((SBP,6) := (SBP,3)) ';' ((Divide (SBP,2,SBP,3)) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP))))))))))) by SCMPDS_4:12;
then A24: GCD-Algorithm = (((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' ((goto 2) ';' ((halt SCMPDS) ';' (((SBP,3) <=0_goto 9) ';' (((SBP,6) := (SBP,3)) ';' ((Divide (SBP,2,SBP,3)) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP)))))))))))) by SCMPDS_4:12;
then A25: GCD-Algorithm = ((GBP := 0) ';' (SBP := 7)) ';' ((saveIC (SBP,RetIC)) ';' ((goto 2) ';' ((halt SCMPDS) ';' (((SBP,3) <=0_goto 9) ';' (((SBP,6) := (SBP,3)) ';' ((Divide (SBP,2,SBP,3)) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP))))))))))))) by SCMPDS_4:12;
then GCD-Algorithm = (GBP := 0) ';' ((SBP := 7) ';' ((saveIC (SBP,RetIC)) ';' ((goto 2) ';' ((halt SCMPDS) ';' (((SBP,3) <=0_goto 9) ';' (((SBP,6) := (SBP,3)) ';' ((Divide (SBP,2,SBP,3)) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP)))))))))))))) by SCMPDS_4:16;
hence GCD-Algorithm . 0 = GBP := 0 by SCMPDS_6:7; :: thesis: ( GCD-Algorithm . 1 = SBP := 7 & GCD-Algorithm . 2 = saveIC (SBP,RetIC) & GCD-Algorithm . 3 = goto 2 & GCD-Algorithm . 4 = halt SCMPDS & GCD-Algorithm . 5 = (SBP,3) <=0_goto 9 & GCD-Algorithm . 6 = (SBP,6) := (SBP,3) & GCD-Algorithm . 7 = Divide (SBP,2,SBP,3) & GCD-Algorithm . 8 = (SBP,7) := (SBP,3) & GCD-Algorithm . 9 = (SBP,(4 + RetSP)) := (GBP,1) & GCD-Algorithm . 10 = AddTo (GBP,1,4) & GCD-Algorithm . 11 = saveIC (SBP,RetIC) & GCD-Algorithm . 12 = goto (- 7) & GCD-Algorithm . 13 = (SBP,2) := (SBP,6) & GCD-Algorithm . 14 = return SBP )
A26: card (Load (GBP := 0)) = 1 by COMPOS_1:54;
GCD-Algorithm = ((Load (GBP := 0)) ';' (SBP := 7)) ';' ((saveIC (SBP,RetIC)) ';' ((goto 2) ';' ((halt SCMPDS) ';' (((SBP,3) <=0_goto 9) ';' (((SBP,6) := (SBP,3)) ';' ((Divide (SBP,2,SBP,3)) ';' (((SBP,7) := (SBP,3)) ';' (((SBP,(4 + RetSP)) := (GBP,1)) ';' ((AddTo (GBP,1,4)) ';' ((saveIC (SBP,RetIC)) ';' ((goto (- 7)) ';' (((SBP,2) := (SBP,6)) ';' (return SBP))))))))))))) by A25, SCMPDS_4:9;
hence GCD-Algorithm . 1 = SBP := 7 by A26, Th7; :: thesis: ( GCD-Algorithm . 2 = saveIC (SBP,RetIC) & GCD-Algorithm . 3 = goto 2 & GCD-Algorithm . 4 = halt SCMPDS & GCD-Algorithm . 5 = (SBP,3) <=0_goto 9 & GCD-Algorithm . 6 = (SBP,6) := (SBP,3) & GCD-Algorithm . 7 = Divide (SBP,2,SBP,3) & GCD-Algorithm . 8 = (SBP,7) := (SBP,3) & GCD-Algorithm . 9 = (SBP,(4 + RetSP)) := (GBP,1) & GCD-Algorithm . 10 = AddTo (GBP,1,4) & GCD-Algorithm . 11 = saveIC (SBP,RetIC) & GCD-Algorithm . 12 = goto (- 7) & GCD-Algorithm . 13 = (SBP,2) := (SBP,6) & GCD-Algorithm . 14 = return SBP )
thus GCD-Algorithm . 2 = saveIC (SBP,RetIC) by A1, A24, Th7; :: thesis: ( GCD-Algorithm . 3 = goto 2 & GCD-Algorithm . 4 = halt SCMPDS & GCD-Algorithm . 5 = (SBP,3) <=0_goto 9 & GCD-Algorithm . 6 = (SBP,6) := (SBP,3) & GCD-Algorithm . 7 = Divide (SBP,2,SBP,3) & GCD-Algorithm . 8 = (SBP,7) := (SBP,3) & GCD-Algorithm . 9 = (SBP,(4 + RetSP)) := (GBP,1) & GCD-Algorithm . 10 = AddTo (GBP,1,4) & GCD-Algorithm . 11 = saveIC (SBP,RetIC) & GCD-Algorithm . 12 = goto (- 7) & GCD-Algorithm . 13 = (SBP,2) := (SBP,6) & GCD-Algorithm . 14 = return SBP )
thus GCD-Algorithm . 3 = goto 2 by A2, A23, Th7; :: thesis: ( GCD-Algorithm . 4 = halt SCMPDS & GCD-Algorithm . 5 = (SBP,3) <=0_goto 9 & GCD-Algorithm . 6 = (SBP,6) := (SBP,3) & GCD-Algorithm . 7 = Divide (SBP,2,SBP,3) & GCD-Algorithm . 8 = (SBP,7) := (SBP,3) & GCD-Algorithm . 9 = (SBP,(4 + RetSP)) := (GBP,1) & GCD-Algorithm . 10 = AddTo (GBP,1,4) & GCD-Algorithm . 11 = saveIC (SBP,RetIC) & GCD-Algorithm . 12 = goto (- 7) & GCD-Algorithm . 13 = (SBP,2) := (SBP,6) & GCD-Algorithm . 14 = return SBP )
thus GCD-Algorithm . 4 = halt SCMPDS by A3, A22, Th7; :: thesis: ( GCD-Algorithm . 5 = (SBP,3) <=0_goto 9 & GCD-Algorithm . 6 = (SBP,6) := (SBP,3) & GCD-Algorithm . 7 = Divide (SBP,2,SBP,3) & GCD-Algorithm . 8 = (SBP,7) := (SBP,3) & GCD-Algorithm . 9 = (SBP,(4 + RetSP)) := (GBP,1) & GCD-Algorithm . 10 = AddTo (GBP,1,4) & GCD-Algorithm . 11 = saveIC (SBP,RetIC) & GCD-Algorithm . 12 = goto (- 7) & GCD-Algorithm . 13 = (SBP,2) := (SBP,6) & GCD-Algorithm . 14 = return SBP )
thus GCD-Algorithm . 5 = (SBP,3) <=0_goto 9 by A4, A21, Th7; :: thesis: ( GCD-Algorithm . 6 = (SBP,6) := (SBP,3) & GCD-Algorithm . 7 = Divide (SBP,2,SBP,3) & GCD-Algorithm . 8 = (SBP,7) := (SBP,3) & GCD-Algorithm . 9 = (SBP,(4 + RetSP)) := (GBP,1) & GCD-Algorithm . 10 = AddTo (GBP,1,4) & GCD-Algorithm . 11 = saveIC (SBP,RetIC) & GCD-Algorithm . 12 = goto (- 7) & GCD-Algorithm . 13 = (SBP,2) := (SBP,6) & GCD-Algorithm . 14 = return SBP )
thus GCD-Algorithm . 6 = (SBP,6) := (SBP,3) by A5, A20, Th7; :: thesis: ( GCD-Algorithm . 7 = Divide (SBP,2,SBP,3) & GCD-Algorithm . 8 = (SBP,7) := (SBP,3) & GCD-Algorithm . 9 = (SBP,(4 + RetSP)) := (GBP,1) & GCD-Algorithm . 10 = AddTo (GBP,1,4) & GCD-Algorithm . 11 = saveIC (SBP,RetIC) & GCD-Algorithm . 12 = goto (- 7) & GCD-Algorithm . 13 = (SBP,2) := (SBP,6) & GCD-Algorithm . 14 = return SBP )
thus GCD-Algorithm . 7 = Divide (SBP,2,SBP,3) by A6, A19, Th7; :: thesis: ( GCD-Algorithm . 8 = (SBP,7) := (SBP,3) & GCD-Algorithm . 9 = (SBP,(4 + RetSP)) := (GBP,1) & GCD-Algorithm . 10 = AddTo (GBP,1,4) & GCD-Algorithm . 11 = saveIC (SBP,RetIC) & GCD-Algorithm . 12 = goto (- 7) & GCD-Algorithm . 13 = (SBP,2) := (SBP,6) & GCD-Algorithm . 14 = return SBP )
thus GCD-Algorithm . 8 = (SBP,7) := (SBP,3) by A7, A18, Th7; :: thesis: ( GCD-Algorithm . 9 = (SBP,(4 + RetSP)) := (GBP,1) & GCD-Algorithm . 10 = AddTo (GBP,1,4) & GCD-Algorithm . 11 = saveIC (SBP,RetIC) & GCD-Algorithm . 12 = goto (- 7) & GCD-Algorithm . 13 = (SBP,2) := (SBP,6) & GCD-Algorithm . 14 = return SBP )
thus GCD-Algorithm . 9 = (SBP,(4 + RetSP)) := (GBP,1) by A8, A17, Th7; :: thesis: ( GCD-Algorithm . 10 = AddTo (GBP,1,4) & GCD-Algorithm . 11 = saveIC (SBP,RetIC) & GCD-Algorithm . 12 = goto (- 7) & GCD-Algorithm . 13 = (SBP,2) := (SBP,6) & GCD-Algorithm . 14 = return SBP )
thus GCD-Algorithm . 10 = AddTo (GBP,1,4) by A9, A16, Th7; :: thesis: ( GCD-Algorithm . 11 = saveIC (SBP,RetIC) & GCD-Algorithm . 12 = goto (- 7) & GCD-Algorithm . 13 = (SBP,2) := (SBP,6) & GCD-Algorithm . 14 = return SBP )
thus GCD-Algorithm . 11 = saveIC (SBP,RetIC) by A10, A15, Th7; :: thesis: ( GCD-Algorithm . 12 = goto (- 7) & GCD-Algorithm . 13 = (SBP,2) := (SBP,6) & GCD-Algorithm . 14 = return SBP )
thus GCD-Algorithm . 12 = goto (- 7) by A11, A14, Th7; :: thesis: ( GCD-Algorithm . 13 = (SBP,2) := (SBP,6) & GCD-Algorithm . 14 = return SBP )
GCD-Algorithm = ((((((((((((((GBP := 0) ';' (SBP := 7)) ';' (saveIC (SBP,RetIC))) ';' (goto 2)) ';' (halt SCMPDS)) ';' ((SBP,3) <=0_goto 9)) ';' ((SBP,6) := (SBP,3))) ';' (Divide (SBP,2,SBP,3))) ';' ((SBP,7) := (SBP,3))) ';' ((SBP,(4 + RetSP)) := (GBP,1))) ';' (AddTo (GBP,1,4))) ';' (saveIC (SBP,RetIC))) ';' (goto (- 7))) ';' ((SBP,2) := (SBP,6))) ';' (Load (return SBP)) by SCMPDS_4:def 3;
hence GCD-Algorithm . 13 = (SBP,2) := (SBP,6) by A12, Th7; :: thesis: GCD-Algorithm . 14 = return SBP
thus GCD-Algorithm . 14 = return SBP by A13, Th6; :: thesis: verum