0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 QDPOrderProof (⇔)
↳4 QDP
↳5 PisEmptyProof (⇔)
↳6 TRUE
++(nil, y) → y
++(x, nil) → x
++(.(x, y), z) → .(x, ++(y, z))
++(++(x, y), z) → ++(x, ++(y, z))
++1(.(x, y), z) → ++1(y, z)
++1(++(x, y), z) → ++1(x, ++(y, z))
++1(++(x, y), z) → ++1(y, z)
++(nil, y) → y
++(x, nil) → x
++(.(x, y), z) → .(x, ++(y, z))
++(++(x, y), z) → ++(x, ++(y, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
++1(.(x, y), z) → ++1(y, z)
++1(++(x, y), z) → ++1(x, ++(y, z))
++1(++(x, y), z) → ++1(y, z)
[++^12, ++2] > .2
++^12: [1,2]
++2: [1,2]
.2: [2,1]
nil: multiset
++(nil, y) → y
++(x, nil) → x
++(.(x, y), z) → .(x, ++(y, z))
++(++(x, y), z) → ++(x, ++(y, z))
++(nil, y) → y
++(x, nil) → x
++(.(x, y), z) → .(x, ++(y, z))
++(++(x, y), z) → ++(x, ++(y, z))