[isabelle] Why is 'auto' slow here?



Hi,

I have the following and somehow 'auto' spends a lot of time and not doesn't terminate:

consts
f :: "real => real"
g :: "real => real"
S :: "real set"

types S = "real set"

axioms
a1: "EX Z < S. ALL x : Z. fx ~= g x"

lemma lem: "EX Z < S. EX x : Z. fx ~= g x"
using a1
apply auto

For some reason, auto doesn't terminate. Shouldn't the lemma be straightforward to prove given a1?

Thanks
John




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