[isabelle] Why is 'auto' slow here?
I have the following and somehow 'auto' spends a lot of time and not
f :: "real => real"
g :: "real => real"
S :: "real set"
types S = "real set"
a1: "EX Z < S. ALL x : Z. fx ~= g x"
lemma lem: "EX Z < S. EX x : Z. fx ~= g x"
For some reason, auto doesn't terminate. Shouldn't the lemma be
straightforward to prove given a1?
This archive was generated by a fusion of
Pipermail (Mailman edition) and