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 Th9;
then A2: card (((GBP := 0 ) ';' (SBP := 7)) ';' (saveIC SBP ,RetIC )) = 2 + 1 by Th8;
then A3: card ((((GBP := 0 ) ';' (SBP := 7)) ';' (saveIC SBP ,RetIC )) ';' (goto 2)) = 3 + 1 by Th8;
then A4: card (((((GBP := 0 ) ';' (SBP := 7)) ';' (saveIC SBP ,RetIC )) ';' (goto 2)) ';' (halt SCMPDS )) = 4 + 1 by Th8;
then A5: card ((((((GBP := 0 ) ';' (SBP := 7)) ';' (saveIC SBP ,RetIC )) ';' (goto 2)) ';' (halt SCMPDS )) ';' (SBP ,3 <=0_goto 9)) = 5 + 1 by Th8;
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 Th8;
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 Th8;
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 Th8;
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 Th8;
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 Th8;
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 Th8;
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 Th8;
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 Th8;
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:49;
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:48;
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:48;
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:48;
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:48;
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:48;
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:48;
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:48;
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:48;
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:48;
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:48;
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:48;
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:52;
hence GCD-Algorithm . 0 = GBP := 0 by SCMPDS_6:16; :: 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 SCMPDS_5:6;
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:43;
hence GCD-Algorithm . 1 = SBP := 7 by A26, Th11; :: 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, Th11; :: 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, Th11; :: 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, Th11; :: 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, Th11; :: 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, Th11; :: 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, Th11; :: 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, Th11; :: 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, Th11; :: 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, Th11; :: 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, Th11; :: 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, Th11; :: 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 5;
hence GCD-Algorithm . 13 = SBP ,2 := SBP ,6 by A12, Th11; :: thesis: GCD-Algorithm . 14 = return SBP
thus GCD-Algorithm . 14 = return SBP by A13, Th10; :: thesis: verum