[isabelle] Questions about arith
Should I expect the following to be solved by arith? Or presburger? Or
some other procedure? Or does the presence of the "f" go beyond what
these procedures can handle? Is there an extension to presburger that
can handle problems of this form?
! (x::num) y z (f::num=>num).
(x < y) & (f x < f y) & (!x::num. z <= x --> (f x = f z)) --> x < z
apply(intro allI impI, elim conjE)
apply(frule_tac x=x in spec)
apply(drule_tac x=y in spec)
This archive was generated by a fusion of
Pipermail (Mailman edition) and