R
↳Dependency Pair Analysis
F(a, f(f(a, x), a)) -> F(f(a, f(a, x)), a)
F(a, f(f(a, x), a)) -> F(a, f(a, x))
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
F(a, f(f(a, x), a)) -> F(a, f(a, x))
f(a, f(f(a, x), a)) -> f(f(a, f(a, x)), a)
one new Dependency Pair is created:
F(a, f(f(a, x), a)) -> F(a, f(a, x))
F(a, f(f(a, f(f(a, x''), a)), a)) -> F(a, f(f(a, f(a, x'')), a))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Narrowing Transformation
F(a, f(f(a, f(f(a, x''), a)), a)) -> F(a, f(f(a, f(a, x'')), a))
f(a, f(f(a, x), a)) -> f(f(a, f(a, x)), a)
one new Dependency Pair is created:
F(a, f(f(a, f(f(a, x''), a)), a)) -> F(a, f(f(a, f(a, x'')), a))
F(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)) -> F(a, f(f(a, f(f(a, f(a, x')), a)), a))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 3
↳Narrowing Transformation
F(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)) -> F(a, f(f(a, f(f(a, f(a, x')), a)), a))
f(a, f(f(a, x), a)) -> f(f(a, f(a, x)), a)
two new Dependency Pairs are created:
F(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)) -> F(a, f(f(a, f(f(a, f(a, x')), a)), a))
F(a, f(f(a, f(f(a, f(f(a, x''), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(a, x''))), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x''), a)), a)), a)), a)) -> F(a, f(f(a, f(f(a, f(f(a, f(a, x'')), a)), a)), a))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 4
↳Narrowing Transformation
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x''), a)), a)), a)), a)) -> F(a, f(f(a, f(f(a, f(f(a, f(a, x'')), a)), a)), a))
F(a, f(f(a, f(f(a, f(f(a, x''), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(a, x''))), a), a))
f(a, f(f(a, x), a)) -> f(f(a, f(a, x)), a)
one new Dependency Pair is created:
F(a, f(f(a, f(f(a, f(f(a, x''), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(a, x''))), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(f(a, f(a, x')), a))), a), a))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 5
↳Narrowing Transformation
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(f(a, f(a, x')), a))), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x''), a)), a)), a)), a)) -> F(a, f(f(a, f(f(a, f(f(a, f(a, x'')), a)), a)), a))
f(a, f(f(a, x), a)) -> f(f(a, f(a, x)), a)
three new Dependency Pairs are created:
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x''), a)), a)), a)), a)) -> F(a, f(f(a, f(f(a, f(f(a, f(a, x'')), a)), a)), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x'''), a)), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(f(a, f(a, x''')), a))), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x'''), a)), a)), a)), a)) -> F(a, f(f(a, f(f(f(a, f(a, f(a, x'''))), a), a)), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)), a)), a)) -> F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(a, x')), a)), a)), a)), a))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 6
↳Narrowing Transformation
F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)), a)), a)) -> F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(a, x')), a)), a)), a)), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x'''), a)), a)), a)), a)) -> F(a, f(f(a, f(f(f(a, f(a, f(a, x'''))), a), a)), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x'''), a)), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(f(a, f(a, x''')), a))), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(f(a, f(a, x')), a))), a), a))
f(a, f(f(a, x), a)) -> f(f(a, f(a, x)), a)
two new Dependency Pairs are created:
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(f(a, f(a, x')), a))), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x''), a)), a)), a)), a)) -> F(a, f(f(f(a, f(f(a, f(a, f(a, x''))), a)), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(f(a, x''), a)), a)), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(f(a, f(f(a, f(a, x'')), a)), a))), a), a))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 7
↳Narrowing Transformation
F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(f(a, x''), a)), a)), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(f(a, f(f(a, f(a, x'')), a)), a))), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x''), a)), a)), a)), a)) -> F(a, f(f(f(a, f(f(a, f(a, f(a, x''))), a)), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x'''), a)), a)), a)), a)) -> F(a, f(f(a, f(f(f(a, f(a, f(a, x'''))), a), a)), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x'''), a)), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(f(a, f(a, x''')), a))), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)), a)), a)) -> F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(a, x')), a)), a)), a)), a))
f(a, f(f(a, x), a)) -> f(f(a, f(a, x)), a)
two new Dependency Pairs are created:
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x'''), a)), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(f(a, f(a, x''')), a))), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x''''), a)), a)), a)), a)) -> F(a, f(f(f(a, f(f(a, f(a, f(a, x''''))), a)), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(f(a, f(f(a, f(a, x')), a)), a))), a), a))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 8
↳Narrowing Transformation
F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(f(a, f(f(a, f(a, x')), a)), a))), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x''''), a)), a)), a)), a)) -> F(a, f(f(f(a, f(f(a, f(a, f(a, x''''))), a)), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x''), a)), a)), a)), a)) -> F(a, f(f(f(a, f(f(a, f(a, f(a, x''))), a)), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)), a)), a)) -> F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(a, x')), a)), a)), a)), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x'''), a)), a)), a)), a)) -> F(a, f(f(a, f(f(f(a, f(a, f(a, x'''))), a), a)), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(f(a, x''), a)), a)), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(f(a, f(f(a, f(a, x'')), a)), a))), a), a))
f(a, f(f(a, x), a)) -> f(f(a, f(a, x)), a)
one new Dependency Pair is created:
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x'''), a)), a)), a)), a)) -> F(a, f(f(a, f(f(f(a, f(a, f(a, x'''))), a), a)), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)), a)), a)) -> F(a, f(f(a, f(f(f(a, f(a, f(f(a, f(a, x')), a))), a), a)), a))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 9
↳Remaining Obligation(s)
F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)), a)), a)) -> F(a, f(f(a, f(f(f(a, f(a, f(f(a, f(a, x')), a))), a), a)), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x''''), a)), a)), a)), a)) -> F(a, f(f(f(a, f(f(a, f(a, f(a, x''''))), a)), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(f(a, x''), a)), a)), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(f(a, f(f(a, f(a, x'')), a)), a))), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, x''), a)), a)), a)), a)) -> F(a, f(f(f(a, f(f(a, f(a, f(a, x''))), a)), a), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)), a)), a)) -> F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(a, x')), a)), a)), a)), a))
F(a, f(f(a, f(f(a, f(f(a, f(f(a, f(f(a, x'), a)), a)), a)), a)), a)) -> F(a, f(f(f(a, f(a, f(f(a, f(f(a, f(a, x')), a)), a))), a), a))
f(a, f(f(a, x), a)) -> f(f(a, f(a, x)), a)