-- FRUIT4PROOF



Derivation of

All b c:
(    (b,c) = (pfirsich,dose)
 ==>     p8(b,c)
       & p8(x,y)
     |   p9(b,c)
       & p9(x,y))

Simplifying (5 steps) the preceding tree leads to the summand

  p8(pfirsich,dose)
& p8(x,y)

Narrowing (4 steps) at position [] of the preceding summand leads to the summand

  True
& p8(x0,y0)

Simplifying the preceding summand leads to the summand

p8(x0,y0)

Narrowing at position [] of the summand

  p9(pfirsich,dose)
& p9(x,y)

leads to the summand

  p9(pfirsich,dose)
& p9(x,y)

Simplifying the preceding summand leads to a new formula. The current formula is given by

p8(x0,y0)