(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
:(:(:(:(C, x), y), z), u) → :(:(x, z), :(:(:(x, y), z), u))
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:
:1(:(:(:(C, x), y), z), u) → :1(:(x, z), :(:(:(x, y), z), u))
:1(:(:(:(C, x), y), z), u) → :1(x, z)
:1(:(:(:(C, x), y), z), u) → :1(:(:(x, y), z), u)
:1(:(:(:(C, x), y), z), u) → :1(:(x, y), z)
:1(:(:(:(C, x), y), z), u) → :1(x, y)
The TRS R consists of the following rules:
:(:(:(:(C, x), y), z), u) → :(:(x, z), :(:(:(x, y), z), u))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(3) QDPSizeChangeProof (EQUIVALENT transformation)
We used the following order and afs together with the size-change analysis [AAECC05] to show that there are no infinite chains for this DP problem.
Order:Recursive path order with status [RPO].
Quasi-Precedence:
C > :2
Status:
:2: [1,2]
C: multiset
AFS:
:(x1, x2) = :(x1, x2)
C = C
From the DPs we obtained the following set of size-change graphs:
- :1(:(:(:(C, x), y), z), u) → :1(:(x, z), :(:(:(x, y), z), u)) (allowed arguments on rhs = {1})
The graph contains the following edges 1 > 1
- :1(:(:(:(C, x), y), z), u) → :1(x, z) (allowed arguments on rhs = {1, 2})
The graph contains the following edges 1 > 1, 1 > 2
- :1(:(:(:(C, x), y), z), u) → :1(:(:(x, y), z), u) (allowed arguments on rhs = {1, 2})
The graph contains the following edges 1 > 1, 2 >= 2
- :1(:(:(:(C, x), y), z), u) → :1(:(x, y), z) (allowed arguments on rhs = {1, 2})
The graph contains the following edges 1 > 1, 1 > 2
- :1(:(:(:(C, x), y), z), u) → :1(x, y) (allowed arguments on rhs = {1, 2})
The graph contains the following edges 1 > 1, 1 > 2
We oriented the following set of usable rules [AAECC05,FROCOS05].
:(:(:(:(C, x), y), z), u) → :(:(x, z), :(:(:(x, y), z), u))
(4) TRUE