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.

Tobias

munddr at googlemail.com wrote:
> 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.