0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 AND
↳5 QDP
↳6 UsableRulesProof (⇔)
↳7 QDP
↳8 MRRProof (⇔)
↳9 QDP
↳10 DependencyGraphProof (⇔)
↳11 QDP
↳12 MRRProof (⇔)
↳13 QDP
↳14 PisEmptyProof (⇔)
↳15 TRUE
↳16 QDP
↳17 UsableRulesProof (⇔)
↳18 QDP
↳19 Narrowing (⇔)
↳20 QDP
↳21 DependencyGraphProof (⇔)
↳22 QDP
↳23 QDPOrderProof (⇔)
↳24 QDP
↳25 UsableRulesProof (⇔)
↳26 QDP
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)))
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)
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)))
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)))
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)))
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)))
f(x, f(s(s(y)), nil)) → f(s(x), f(y, f(s(0), nil)))
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)
POL(0) = 0
POL(F(x1, x2)) = x1 + x2
POL(f(x1, x2)) = x1 + x2
POL(nil) = 0
POL(s(x1)) = 1 + x1
F(x, f(s(s(y)), f(z, w))) → F(s(x), f(y, 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(s(x), f(y, f(s(0), nil)))
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(x), f(y, 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)), f(z, w))) → f(s(x), f(y, f(s(z), w)))
F(x, f(s(s(y)), f(z, w))) → F(s(x), f(y, f(s(z), w)))
POL(0) = 0
POL(F(x1, x2)) = 2·x1 + 2·x2
POL(f(x1, x2)) = 2·x1 + x2
POL(nil) = 0
POL(s(x1)) = 2 + x1
f(x, f(s(s(y)), nil)) → f(s(x), f(y, f(s(0), nil)))
f(x, f(s(s(y)), f(z, w))) → f(s(x), f(y, f(s(z), w)))
L1(f(s(s(y)), f(z, w))) → L1(f(s(0), f(y, f(s(z), w))))
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)))
L1(f(s(s(y)), f(z, w))) → L1(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)))
f(x, f(s(s(y)), f(z, w))) → f(s(x), f(y, f(s(z), w)))
L1(f(s(s(s(s(x1)))), f(y1, x3))) → L1(f(s(s(0)), f(x1, f(s(s(y1)), x3))))
L1(f(s(s(x0)), f(s(x1), nil))) → L1(f(s(0), f(s(x0), f(x1, f(s(0), nil)))))
L1(f(s(s(x0)), f(s(x1), f(x2, x3)))) → L1(f(s(0), f(s(x0), f(x1, f(s(x2), x3)))))
L1(f(s(s(y0)), f(y1, f(s(s(x1)), nil)))) → L1(f(s(0), f(y0, f(s(s(y1)), f(x1, f(s(0), nil))))))
L1(f(s(s(y0)), f(y1, f(s(s(x1)), f(x2, x3))))) → L1(f(s(0), f(y0, f(s(s(y1)), f(x1, f(s(x2), x3))))))
L1(f(s(s(s(s(x1)))), f(y1, x3))) → L1(f(s(s(0)), f(x1, f(s(s(y1)), x3))))
L1(f(s(s(x0)), f(s(x1), nil))) → L1(f(s(0), f(s(x0), f(x1, f(s(0), nil)))))
L1(f(s(s(x0)), f(s(x1), f(x2, x3)))) → L1(f(s(0), f(s(x0), f(x1, f(s(x2), x3)))))
L1(f(s(s(y0)), f(y1, f(s(s(x1)), nil)))) → L1(f(s(0), f(y0, f(s(s(y1)), f(x1, f(s(0), nil))))))
L1(f(s(s(y0)), f(y1, f(s(s(x1)), f(x2, x3))))) → L1(f(s(0), f(y0, f(s(s(y1)), f(x1, f(s(x2), x3))))))
f(x, f(s(s(y)), nil)) → f(s(x), f(y, f(s(0), nil)))
f(x, f(s(s(y)), f(z, w))) → f(s(x), f(y, f(s(z), w)))
L1(f(s(s(s(s(x1)))), f(y1, x3))) → L1(f(s(s(0)), f(x1, f(s(s(y1)), x3))))
L1(f(s(s(x0)), f(s(x1), f(x2, x3)))) → L1(f(s(0), f(s(x0), f(x1, f(s(x2), x3)))))
L1(f(s(s(y0)), f(y1, f(s(s(x1)), nil)))) → L1(f(s(0), f(y0, f(s(s(y1)), f(x1, f(s(0), nil))))))
L1(f(s(s(y0)), f(y1, f(s(s(x1)), f(x2, x3))))) → L1(f(s(0), f(y0, f(s(s(y1)), f(x1, f(s(x2), x3))))))
f(x, f(s(s(y)), nil)) → f(s(x), f(y, f(s(0), nil)))
f(x, f(s(s(y)), f(z, w))) → f(s(x), f(y, f(s(z), w)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
L1(f(s(s(y0)), f(y1, f(s(s(x1)), nil)))) → L1(f(s(0), f(y0, f(s(s(y1)), f(x1, f(s(0), nil))))))
The value of delta used in the strict ordering is 3/4.
POL(L1(x1)) = (2)x1
POL(f(x1, x2)) = (1/2)x2
POL(s(x1)) = (1/4)x1
POL(0) = 0
POL(nil) = 4
f(x, f(s(s(y)), f(z, w))) → f(s(x), f(y, f(s(z), w)))
f(x, f(s(s(y)), nil)) → f(s(x), f(y, f(s(0), nil)))
L1(f(s(s(s(s(x1)))), f(y1, x3))) → L1(f(s(s(0)), f(x1, f(s(s(y1)), x3))))
L1(f(s(s(x0)), f(s(x1), f(x2, x3)))) → L1(f(s(0), f(s(x0), f(x1, f(s(x2), x3)))))
L1(f(s(s(y0)), f(y1, f(s(s(x1)), f(x2, x3))))) → L1(f(s(0), f(y0, f(s(s(y1)), f(x1, f(s(x2), x3))))))
f(x, f(s(s(y)), nil)) → f(s(x), f(y, f(s(0), nil)))
f(x, f(s(s(y)), f(z, w))) → f(s(x), f(y, f(s(z), w)))
L1(f(s(s(y)), f(z, w))) → L1(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)))
f(x, f(s(s(y)), f(z, w))) → f(s(x), f(y, f(s(z), w)))