-- NEED1PROOF


Derivation of

r(f(x,y),z,0)

Narrowing the preceding formula leads to the formula

    r(0,z,0)
  & x = 0
  & y = 0
|   r(1,z,0)
  & Any x1:
    (x = suc(x1))
  & y = 0
|   r(2,z,0)
  & Any y1:
    (y = suc(y1))

Reducts have been simplified.

Narrowing the preceding formula leads to the formula

    z = 0
  & x = 0
  & y = 0
|   r(1,z,0)
  & Any x1:
    (x = suc(x1))
  & y = 0
|   r(2,z,0)
  & Any y1:
    (y = suc(y1))

Reducts have been simplified.

Narrowing the preceding formula leads to the formula

    z = 0
  & x = 0
  & y = 0
|   r(2,z,0)
  & Any y1:
    (y = suc(y1))

Reducts have been simplified.
Irreducible atoms have been removed.

Narrowing the preceding formula leads to the formula

  z = 0
& x = 0
& y = 0

Reducts have been simplified.
Irreducible atoms have been removed.

Number of proof steps: 4

Solutions:

  z = 0
& x = 0
& y = 0