Re: [isabelle] Unifiction question

To do that, you need to show somehow that "a" equals one of the arguments of ?V_ff32. You say its arguments include "a Un a", but I see "a Un aa". If indeed a = nV_f2 - aa then "a" and "aa" are disjoint, so "a Un aa" can't equal "a".

Larry Paulson

On 10 Nov 2005, at 21:09, shimonyb at wrote:

My question: Is it possible to unify the premisis and the subgoal, possibly
using the additional assumption i have: 'a = nV_f2 - aa' ?

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