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; ( 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; ( 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; ( 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; ( 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; ( 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; ( 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; ( 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; ( 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; ( 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; ( 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; ( 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; ( 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; ( 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; GCD-Algorithm . 14 = return SBP
thus
GCD-Algorithm . 14 = return SBP
by A13, Th6; verum