R
↳Dependency Pair Analysis
F(cons(x, k), l) -> G(k, l, cons(x, k))
G(a, b, c) -> F(a, cons(b, c))
R
↳DPs
→DP Problem 1
↳Instantiation Transformation
G(a, b, c) -> F(a, cons(b, c))
F(cons(x, k), l) -> G(k, l, cons(x, k))
f(empty, l) -> l
f(cons(x, k), l) -> g(k, l, cons(x, k))
g(a, b, c) -> f(a, cons(b, c))
one new Dependency Pair is created:
F(cons(x, k), l) -> G(k, l, cons(x, k))
F(cons(x', k'), cons(b'', c'')) -> G(k', cons(b'', c''), cons(x', k'))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Instantiation Transformation
F(cons(x', k'), cons(b'', c'')) -> G(k', cons(b'', c''), cons(x', k'))
G(a, b, c) -> F(a, cons(b, c))
f(empty, l) -> l
f(cons(x, k), l) -> g(k, l, cons(x, k))
g(a, b, c) -> f(a, cons(b, c))
one new Dependency Pair is created:
G(a, b, c) -> F(a, cons(b, c))
G(a', cons(b'''', c''''), cons(x''', k'''')) -> F(a', cons(cons(b'''', c''''), cons(x''', k'''')))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 3
↳Instantiation Transformation
G(a', cons(b'''', c''''), cons(x''', k'''')) -> F(a', cons(cons(b'''', c''''), cons(x''', k'''')))
F(cons(x', k'), cons(b'', c'')) -> G(k', cons(b'', c''), cons(x', k'))
f(empty, l) -> l
f(cons(x, k), l) -> g(k, l, cons(x, k))
g(a, b, c) -> f(a, cons(b, c))
one new Dependency Pair is created:
F(cons(x', k'), cons(b'', c'')) -> G(k', cons(b'', c''), cons(x', k'))
F(cons(x'', k''), cons(cons(b'''''', c''''''), cons(x''''', k''''''))) -> G(k'', cons(cons(b'''''', c''''''), cons(x''''', k'''''')), cons(x'', k''))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 4
↳Instantiation Transformation
F(cons(x'', k''), cons(cons(b'''''', c''''''), cons(x''''', k''''''))) -> G(k'', cons(cons(b'''''', c''''''), cons(x''''', k'''''')), cons(x'', k''))
G(a', cons(b'''', c''''), cons(x''', k'''')) -> F(a', cons(cons(b'''', c''''), cons(x''', k'''')))
f(empty, l) -> l
f(cons(x, k), l) -> g(k, l, cons(x, k))
g(a, b, c) -> f(a, cons(b, c))
one new Dependency Pair is created:
G(a', cons(b'''', c''''), cons(x''', k'''')) -> F(a', cons(cons(b'''', c''''), cons(x''', k'''')))
G(a'', cons(cons(b'''''''', c''''''''), cons(x''''''', k'''''''')), cons(x''''', k''''')) -> F(a'', cons(cons(cons(b'''''''', c''''''''), cons(x''''''', k'''''''')), cons(x''''', k''''')))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 5
↳Instantiation Transformation
G(a'', cons(cons(b'''''''', c''''''''), cons(x''''''', k'''''''')), cons(x''''', k''''')) -> F(a'', cons(cons(cons(b'''''''', c''''''''), cons(x''''''', k'''''''')), cons(x''''', k''''')))
F(cons(x'', k''), cons(cons(b'''''', c''''''), cons(x''''', k''''''))) -> G(k'', cons(cons(b'''''', c''''''), cons(x''''', k'''''')), cons(x'', k''))
f(empty, l) -> l
f(cons(x, k), l) -> g(k, l, cons(x, k))
g(a, b, c) -> f(a, cons(b, c))
one new Dependency Pair is created:
F(cons(x'', k''), cons(cons(b'''''', c''''''), cons(x''''', k''''''))) -> G(k'', cons(cons(b'''''', c''''''), cons(x''''', k'''''')), cons(x'', k''))
F(cons(x''', k'''), cons(cons(cons(b'''''''''', c''''''''''), cons(x''''''''', k'''''''''')), cons(x''''''', k''''''''))) -> G(k''', cons(cons(cons(b'''''''''', c''''''''''), cons(x''''''''', k'''''''''')), cons(x''''''', k'''''''')), cons(x''', k'''))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 6
↳Instantiation Transformation
F(cons(x''', k'''), cons(cons(cons(b'''''''''', c''''''''''), cons(x''''''''', k'''''''''')), cons(x''''''', k''''''''))) -> G(k''', cons(cons(cons(b'''''''''', c''''''''''), cons(x''''''''', k'''''''''')), cons(x''''''', k'''''''')), cons(x''', k'''))
G(a'', cons(cons(b'''''''', c''''''''), cons(x''''''', k'''''''')), cons(x''''', k''''')) -> F(a'', cons(cons(cons(b'''''''', c''''''''), cons(x''''''', k'''''''')), cons(x''''', k''''')))
f(empty, l) -> l
f(cons(x, k), l) -> g(k, l, cons(x, k))
g(a, b, c) -> f(a, cons(b, c))
one new Dependency Pair is created:
G(a'', cons(cons(b'''''''', c''''''''), cons(x''''''', k'''''''')), cons(x''''', k''''')) -> F(a'', cons(cons(cons(b'''''''', c''''''''), cons(x''''''', k'''''''')), cons(x''''', k''''')))
G(a''', cons(cons(cons(b'''''''''''', c''''''''''''), cons(x''''''''''', k'''''''''''')), cons(x''''''''', k'''''''''')), cons(x'''''', k'''''')) -> F(a''', cons(cons(cons(cons(b'''''''''''', c''''''''''''), cons(x''''''''''', k'''''''''''')), cons(x''''''''', k'''''''''')), cons(x'''''', k'''''')))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 7
↳Instantiation Transformation
G(a''', cons(cons(cons(b'''''''''''', c''''''''''''), cons(x''''''''''', k'''''''''''')), cons(x''''''''', k'''''''''')), cons(x'''''', k'''''')) -> F(a''', cons(cons(cons(cons(b'''''''''''', c''''''''''''), cons(x''''''''''', k'''''''''''')), cons(x''''''''', k'''''''''')), cons(x'''''', k'''''')))
F(cons(x''', k'''), cons(cons(cons(b'''''''''', c''''''''''), cons(x''''''''', k'''''''''')), cons(x''''''', k''''''''))) -> G(k''', cons(cons(cons(b'''''''''', c''''''''''), cons(x''''''''', k'''''''''')), cons(x''''''', k'''''''')), cons(x''', k'''))
f(empty, l) -> l
f(cons(x, k), l) -> g(k, l, cons(x, k))
g(a, b, c) -> f(a, cons(b, c))
one new Dependency Pair is created:
F(cons(x''', k'''), cons(cons(cons(b'''''''''', c''''''''''), cons(x''''''''', k'''''''''')), cons(x''''''', k''''''''))) -> G(k''', cons(cons(cons(b'''''''''', c''''''''''), cons(x''''''''', k'''''''''')), cons(x''''''', k'''''''')), cons(x''', k'''))
F(cons(x'''', k''''), cons(cons(cons(cons(b'''''''''''''', c''''''''''''''), cons(x''''''''''''', k'''''''''''''')), cons(x''''''''''', k'''''''''''')), cons(x'''''''0, k'''''''''))) -> G(k'''', cons(cons(cons(cons(b'''''''''''''', c''''''''''''''), cons(x''''''''''''', k'''''''''''''')), cons(x''''''''''', k'''''''''''')), cons(x'''''''0, k''''''''')), cons(x'''', k''''))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 8
↳Instantiation Transformation
F(cons(x'''', k''''), cons(cons(cons(cons(b'''''''''''''', c''''''''''''''), cons(x''''''''''''', k'''''''''''''')), cons(x''''''''''', k'''''''''''')), cons(x'''''''0, k'''''''''))) -> G(k'''', cons(cons(cons(cons(b'''''''''''''', c''''''''''''''), cons(x''''''''''''', k'''''''''''''')), cons(x''''''''''', k'''''''''''')), cons(x'''''''0, k''''''''')), cons(x'''', k''''))
G(a''', cons(cons(cons(b'''''''''''', c''''''''''''), cons(x''''''''''', k'''''''''''')), cons(x''''''''', k'''''''''')), cons(x'''''', k'''''')) -> F(a''', cons(cons(cons(cons(b'''''''''''', c''''''''''''), cons(x''''''''''', k'''''''''''')), cons(x''''''''', k'''''''''')), cons(x'''''', k'''''')))
f(empty, l) -> l
f(cons(x, k), l) -> g(k, l, cons(x, k))
g(a, b, c) -> f(a, cons(b, c))
one new Dependency Pair is created:
G(a''', cons(cons(cons(b'''''''''''', c''''''''''''), cons(x''''''''''', k'''''''''''')), cons(x''''''''', k'''''''''')), cons(x'''''', k'''''')) -> F(a''', cons(cons(cons(cons(b'''''''''''', c''''''''''''), cons(x''''''''''', k'''''''''''')), cons(x''''''''', k'''''''''')), cons(x'''''', k'''''')))
G(a'''', cons(cons(cons(cons(b'''''''''''''''', c''''''''''''''''), cons(x''''''''''''''', k'''''''''''''''')), cons(x''''''''''''', k'''''''''''''')), cons(x'''''''''', k''''''''''0)), cons(x''''''', k''''''')) -> F(a'''', cons(cons(cons(cons(cons(b'''''''''''''''', c''''''''''''''''), cons(x''''''''''''''', k'''''''''''''''')), cons(x''''''''''''', k'''''''''''''')), cons(x'''''''''', k''''''''''0)), cons(x''''''', k''''''')))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 9
↳Instantiation Transformation
G(a'''', cons(cons(cons(cons(b'''''''''''''''', c''''''''''''''''), cons(x''''''''''''''', k'''''''''''''''')), cons(x''''''''''''', k'''''''''''''')), cons(x'''''''''', k''''''''''0)), cons(x''''''', k''''''')) -> F(a'''', cons(cons(cons(cons(cons(b'''''''''''''''', c''''''''''''''''), cons(x''''''''''''''', k'''''''''''''''')), cons(x''''''''''''', k'''''''''''''')), cons(x'''''''''', k''''''''''0)), cons(x''''''', k''''''')))
F(cons(x'''', k''''), cons(cons(cons(cons(b'''''''''''''', c''''''''''''''), cons(x''''''''''''', k'''''''''''''')), cons(x''''''''''', k'''''''''''')), cons(x'''''''0, k'''''''''))) -> G(k'''', cons(cons(cons(cons(b'''''''''''''', c''''''''''''''), cons(x''''''''''''', k'''''''''''''')), cons(x''''''''''', k'''''''''''')), cons(x'''''''0, k''''''''')), cons(x'''', k''''))
f(empty, l) -> l
f(cons(x, k), l) -> g(k, l, cons(x, k))
g(a, b, c) -> f(a, cons(b, c))
one new Dependency Pair is created:
F(cons(x'''', k''''), cons(cons(cons(cons(b'''''''''''''', c''''''''''''''), cons(x''''''''''''', k'''''''''''''')), cons(x''''''''''', k'''''''''''')), cons(x'''''''0, k'''''''''))) -> G(k'''', cons(cons(cons(cons(b'''''''''''''', c''''''''''''''), cons(x''''''''''''', k'''''''''''''')), cons(x''''''''''', k'''''''''''')), cons(x'''''''0, k''''''''')), cons(x'''', k''''))
F(cons(x''''', k'''''), cons(cons(cons(cons(cons(b'''''''''''''''''', c''''''''''''''''''), cons(x''''''''''''''''', k'''''''''''''''''')), cons(x''''''''''''''', k'''''''''''''''')), cons(x'''''''''''0, k''''''''''''')), cons(x'''''''0', k''''''''''))) -> G(k''''', cons(cons(cons(cons(cons(b'''''''''''''''''', c''''''''''''''''''), cons(x''''''''''''''''', k'''''''''''''''''')), cons(x''''''''''''''', k'''''''''''''''')), cons(x'''''''''''0, k''''''''''''')), cons(x'''''''0', k'''''''''')), cons(x''''', k'''''))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 10
↳Instantiation Transformation
F(cons(x''''', k'''''), cons(cons(cons(cons(cons(b'''''''''''''''''', c''''''''''''''''''), cons(x''''''''''''''''', k'''''''''''''''''')), cons(x''''''''''''''', k'''''''''''''''')), cons(x'''''''''''0, k''''''''''''')), cons(x'''''''0', k''''''''''))) -> G(k''''', cons(cons(cons(cons(cons(b'''''''''''''''''', c''''''''''''''''''), cons(x''''''''''''''''', k'''''''''''''''''')), cons(x''''''''''''''', k'''''''''''''''')), cons(x'''''''''''0, k''''''''''''')), cons(x'''''''0', k'''''''''')), cons(x''''', k'''''))
G(a'''', cons(cons(cons(cons(b'''''''''''''''', c''''''''''''''''), cons(x''''''''''''''', k'''''''''''''''')), cons(x''''''''''''', k'''''''''''''')), cons(x'''''''''', k''''''''''0)), cons(x''''''', k''''''')) -> F(a'''', cons(cons(cons(cons(cons(b'''''''''''''''', c''''''''''''''''), cons(x''''''''''''''', k'''''''''''''''')), cons(x''''''''''''', k'''''''''''''')), cons(x'''''''''', k''''''''''0)), cons(x''''''', k''''''')))
f(empty, l) -> l
f(cons(x, k), l) -> g(k, l, cons(x, k))
g(a, b, c) -> f(a, cons(b, c))
one new Dependency Pair is created:
G(a'''', cons(cons(cons(cons(b'''''''''''''''', c''''''''''''''''), cons(x''''''''''''''', k'''''''''''''''')), cons(x''''''''''''', k'''''''''''''')), cons(x'''''''''', k''''''''''0)), cons(x''''''', k''''''')) -> F(a'''', cons(cons(cons(cons(cons(b'''''''''''''''', c''''''''''''''''), cons(x''''''''''''''', k'''''''''''''''')), cons(x''''''''''''', k'''''''''''''')), cons(x'''''''''', k''''''''''0)), cons(x''''''', k''''''')))
G(a''''', cons(cons(cons(cons(cons(b'''''''''''''''''''', c''''''''''''''''''''), cons(x''''''''''''''''''', k'''''''''''''''''''')), cons(x''''''''''''''''', k'''''''''''''''''')), cons(x'''''''''''''', k''''''''''''''0)), cons(x''''''''''', k''''''''''0')), cons(x'''''''', k'''''''')) -> F(a''''', cons(cons(cons(cons(cons(cons(b'''''''''''''''''''', c''''''''''''''''''''), cons(x''''''''''''''''''', k'''''''''''''''''''')), cons(x''''''''''''''''', k'''''''''''''''''')), cons(x'''''''''''''', k''''''''''''''0)), cons(x''''''''''', k''''''''''0')), cons(x'''''''', k'''''''')))
R
↳DPs
→DP Problem 1
↳Inst
→DP Problem 2
↳Inst
...
→DP Problem 11
↳Remaining Obligation(s)
G(a''''', cons(cons(cons(cons(cons(b'''''''''''''''''''', c''''''''''''''''''''), cons(x''''''''''''''''''', k'''''''''''''''''''')), cons(x''''''''''''''''', k'''''''''''''''''')), cons(x'''''''''''''', k''''''''''''''0)), cons(x''''''''''', k''''''''''0')), cons(x'''''''', k'''''''')) -> F(a''''', cons(cons(cons(cons(cons(cons(b'''''''''''''''''''', c''''''''''''''''''''), cons(x''''''''''''''''''', k'''''''''''''''''''')), cons(x''''''''''''''''', k'''''''''''''''''')), cons(x'''''''''''''', k''''''''''''''0)), cons(x''''''''''', k''''''''''0')), cons(x'''''''', k'''''''')))
F(cons(x''''', k'''''), cons(cons(cons(cons(cons(b'''''''''''''''''', c''''''''''''''''''), cons(x''''''''''''''''', k'''''''''''''''''')), cons(x''''''''''''''', k'''''''''''''''')), cons(x'''''''''''0, k''''''''''''')), cons(x'''''''0', k''''''''''))) -> G(k''''', cons(cons(cons(cons(cons(b'''''''''''''''''', c''''''''''''''''''), cons(x''''''''''''''''', k'''''''''''''''''')), cons(x''''''''''''''', k'''''''''''''''')), cons(x'''''''''''0, k''''''''''''')), cons(x'''''''0', k'''''''''')), cons(x''''', k'''''))
f(empty, l) -> l
f(cons(x, k), l) -> g(k, l, cons(x, k))
g(a, b, c) -> f(a, cons(b, c))