# [isabelle] Proving lemmas containing a squareroot

Hi
I'm hoping some of you could help me with the following lemma:
consts
pl :: "real => real"
axioms
gt: "EX x y. pl x > pl y"
lemma rt4: "ALL a b. sqrt(4) / pl a > sqrt(4) / pl b"
using gt
sledgehammer;
It seems like a rather simple lemma but sledgehammer (E, SPASS, and
Vampire) can't seem to return the set of theorems for metis. Does
anyone know how to prove it?
Moreover, if I simplify the lemma by removing the sqrt to:
lemma rt4: "ALL a b. (4) / pl a > (4) / pl b"
using gt
sledgehammer;
Vampire gives me a minimal set of 14 theorems for metis:
apply (metis comm_monoid_add.mult_commute comp_arith(112)
divide_inverse eq_diff_eq' eq_number_of inverse_inverse_eq
linorder_neqE_ordered_idom monoid_add_class.add_0_right
mult.diff_right mult.zero_left real_less_def real_mult_right_cancel
rel_simps(38) rel_simps(46))
However, metis actually will not terminate. Assuming those 14 theorems
are the required theorems, why is having sqrt so difficult for
sledgehammer?
Thanks!
Michael

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*