R
↳Dependency Pair Analysis
F(x, y, f(z, u, v)) -> F(f(x, y, z), u, f(x, y, v))
F(x, y, f(z, u, v)) -> F(x, y, z)
F(x, y, f(z, u, v)) -> F(x, y, v)
R
↳DPs
→DP Problem 1
↳Forward Instantiation Transformation
F(x, y, f(z, u, v)) -> F(x, y, z)
F(x, y, f(z, u, v)) -> F(f(x, y, z), u, f(x, y, v))
f(x, y, f(z, u, v)) -> f(f(x, y, z), u, f(x, y, v))
innermost
one new Dependency Pair is created:
F(x, y, f(z, u, v)) -> F(x, y, z)
F(x'', y'', f(f(z'', u'', v''), u, v)) -> F(x'', y'', f(z'', u'', v''))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Remaining Obligation(s)
F(x'', y'', f(f(z'', u'', v''), u, v)) -> F(x'', y'', f(z'', u'', v''))
F(x, y, f(z, u, v)) -> F(f(x, y, z), u, f(x, y, v))
f(x, y, f(z, u, v)) -> f(f(x, y, z), u, f(x, y, v))
innermost