Re: [isabelle] Why is 'auto' slow here?
I'm afraid your formulae are not well-formed. Never mind the "fx", but
"EX Z < S. ALL x : Z" doesnt make sense. Pls send an actual theory that
Isabelle is prepared to accept.
munddr at googlemail.com wrote:
> I have the following and somehow 'auto' spends a lot of time and not
> doesn't terminate:
> 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"
> using a1
> apply auto
> 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