Termination w.r.t. Q of the given QTRS could not be shown:

0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
  ↳5 QDP
  ↳6 QDP

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(x, f(s(s(y)), f(z, w))) → f(s(x), f(y, f(s(z), w)))
L(f(s(s(y)), f(z, w))) → L(f(s(0), f(y, f(s(z), w))))
f(x, f(s(s(y)), nil)) → f(s(x), f(y, f(s(0), nil)))

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(x, f(s(s(y)), f(z, w))) → F(s(x), f(y, f(s(z), w)))
F(x, f(s(s(y)), f(z, w))) → F(y, f(s(z), w))
F(x, f(s(s(y)), f(z, w))) → F(s(z), w)
L1(f(s(s(y)), f(z, w))) → L1(f(s(0), f(y, f(s(z), w))))
L1(f(s(s(y)), f(z, w))) → F(s(0), f(y, f(s(z), w)))
L1(f(s(s(y)), f(z, w))) → F(y, f(s(z), w))
L1(f(s(s(y)), f(z, w))) → F(s(z), w)
F(x, f(s(s(y)), nil)) → F(s(x), f(y, f(s(0), nil)))
F(x, f(s(s(y)), nil)) → F(y, f(s(0), nil))
F(x, f(s(s(y)), nil)) → F(s(0), nil)

The TRS R consists of the following rules:

f(x, f(s(s(y)), f(z, w))) → f(s(x), f(y, f(s(z), w)))
L(f(s(s(y)), f(z, w))) → L(f(s(0), f(y, f(s(z), w))))
f(x, f(s(s(y)), nil)) → f(s(x), f(y, f(s(0), nil)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 5 less nodes.

(4) Complex Obligation (AND)

(5) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F(x, f(s(s(y)), f(z, w))) → F(y, f(s(z), w))
F(x, f(s(s(y)), f(z, w))) → F(s(x), f(y, f(s(z), w)))
F(x, f(s(s(y)), f(z, w))) → F(s(z), w)
F(x, f(s(s(y)), nil)) → F(s(x), f(y, f(s(0), nil)))

The TRS R consists of the following rules:

f(x, f(s(s(y)), f(z, w))) → f(s(x), f(y, f(s(z), w)))
L(f(s(s(y)), f(z, w))) → L(f(s(0), f(y, f(s(z), w))))
f(x, f(s(s(y)), nil)) → f(s(x), f(y, f(s(0), nil)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(6) Obligation:

Q DP problem:
The TRS P consists of the following rules:

L1(f(s(s(y)), f(z, w))) → L1(f(s(0), f(y, f(s(z), w))))

The TRS R consists of the following rules:

f(x, f(s(s(y)), f(z, w))) → f(s(x), f(y, f(s(z), w)))
L(f(s(s(y)), f(z, w))) → L(f(s(0), f(y, f(s(z), w))))
f(x, f(s(s(y)), nil)) → f(s(x), f(y, f(s(0), nil)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.