val from_mech =
   (7 , --`((((x > 0) /\ (y > 0)) ==> ((x > 0) /\ ((y > 0) /\ (((((gcd) (x) )) (y) ) = ((((gcd) (x) )) (y) )))))
            /\
            ((MARKER ["EC"]
              (((((x > 0) /\ ((y > 0) /\ (((((gcd) (x) )) (y) ) = ((((gcd) (x__0) )) (y__0) )))) /\ (~((x notEqual y)))) ==> (x = ((((gcd) (x__0) )) (y__0) )))))
             /\
             ((MARKER ["TC2"]
               (((((x > 0) /\ ((y > 0) /\ (((((gcd) (x) )) (y) ) = ((((gcd) (x__0) )) (y__0) )))) /\ (x notEqual y)) ==> ((x > y) ==> (((x - y) + y) < (x + y))))))
              /\
              ((MARKER ["IC"]
                (((((x > 0) /\ ((y > 0) /\ (((((gcd) (x) )) (y) ) = ((((gcd) (x__0) )) (y__0) )))) /\ (x notEqual y)) ==> ((x > y) ==> (((x - y) > 0) /\ ((y > 0) /\ (((((gcd) ((x - y)) )) (y) ) = ((((gcd) (x__0) )) (y__0) ))))))))
               /\
               ((MARKER ["TC2"]
                 (((((x > 0) /\ ((y > 0) /\ (((((gcd) (x) )) (y) ) = ((((gcd) (x__0) )) (y__0) )))) /\ (x notEqual y)) ==> ((~((x > y))) ==> ((x + (y - x)) < (x + y))))))
                /\
                ((MARKER ["IC"]
                  (((((x > 0) /\ ((y > 0) /\ (((((gcd) (x) )) (y) ) = ((((gcd) (x__0) )) (y__0) )))) /\ (x notEqual y)) ==> ((~((x > y))) ==> ((x > 0) /\ (((y - x) > 0) /\ (((((gcd) (x) )) ((y - x)) ) = ((((gcd) (x__0) )) (y__0) ))))))))
                 /\
                 (MARKER ["TC1"]
                  (((((x > 0) /\ ((y > 0) /\ (((((gcd) (x) )) (y) ) = ((((gcd) (x__0) )) (y__0) )))) /\ (x notEqual y)) ==> ((x + y) > 0))))))))))`-- ) ;