Re: [isabelle] Stuck with existential quantifier
the nth function on lists (xs ! n) is undefined when n is outside the
bounds of xs. That means that we do not know anything about the result.
Since we do not know anything, we do in particular not know whether the
result is 0 or not. Thus your statement is not provable.
I hope this helps.
On 07/25/2011 10:17 PM, Christian Kühnel wrote:
Dear isabelle users,
I'm trying to prove this obvious lemma:
"~ (EX t. [1::nat,1,1] ! t = 0 )"
I've been trying for a while but could not figure it out. Can you please
give me a hint, how I can prove this?
Is there more documatation on prooving terms with existential and universal
quantifiers? The isabelle tutorial did not help me there.
This archive was generated by a fusion of
Pipermail (Mailman edition) and