[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

higher order sub-term rewriting



We have got a problem to apply a higher order rewrite on a subterm:

{-1}    (FORALL (P: pred[below(N)]):
         (FORALL (x: below(N)): P(x)) = 
         (FORALL (x: below(N)): P(p!1(x))))
  |-------
[1]    EXISTS (x1: below(N)):
        FORALL (x2: below(N)):
          EXISTS (x3: below(N)): 
             P!1((x1 = x2), (x1 = x3), (f!1(x2) = f!1(x3)))


Is it possible to rewrite the goal using the hypothesis. Note that
such a rewrite is possible within the HOL system, thanks to higher
order rewriting.

Thanks for any help.