Re: [isabelle] Questions about arith

> ! (x::num) y z (f::num=>num).
> (x < y) & (f x < f y) & (!x::num. z <= x --> (f x = f z)) --> x < z

num = nat/int/real? In either case, this is beyond arith (and arith tries
Presburger) and not in any of the standard classes of decidable theories.
The f is indeed the problem. Clearly a more heuristic approach is needed here.


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