0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 QDPOrderProof (⇔)
↳9 QDP
↳10 PisEmptyProof (⇔)
↳11 TRUE
↳12 QDP
↳13 QDPOrderProof (⇔)
↳14 QDP
↳15 DependencyGraphProof (⇔)
↳16 TRUE
rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
rev(nil)
rev(++(x0, x1))
rev1(x0, nil)
rev1(x0, ++(x1, x2))
rev2(x0, nil)
rev2(x0, ++(x1, x2))
REV(++(x, y)) → REV1(x, y)
REV(++(x, y)) → REV2(x, y)
REV1(x, ++(y, z)) → REV1(y, z)
REV2(x, ++(y, z)) → REV(++(x, rev(rev2(y, z))))
REV2(x, ++(y, z)) → REV(rev2(y, z))
REV2(x, ++(y, z)) → REV2(y, z)
rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
rev(nil)
rev(++(x0, x1))
rev1(x0, nil)
rev1(x0, ++(x1, x2))
rev2(x0, nil)
rev2(x0, ++(x1, x2))
REV1(x, ++(y, z)) → REV1(y, z)
rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
rev(nil)
rev(++(x0, x1))
rev1(x0, nil)
rev1(x0, ++(x1, x2))
rev2(x0, nil)
rev2(x0, ++(x1, x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
REV1(x, ++(y, z)) → REV1(y, z)
trivial
rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
rev(nil)
rev(++(x0, x1))
rev1(x0, nil)
rev1(x0, ++(x1, x2))
rev2(x0, nil)
rev2(x0, ++(x1, x2))
REV(++(x, y)) → REV2(x, y)
REV2(x, ++(y, z)) → REV(++(x, rev(rev2(y, z))))
REV2(x, ++(y, z)) → REV(rev2(y, z))
REV2(x, ++(y, z)) → REV2(y, z)
rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
rev(nil)
rev(++(x0, x1))
rev1(x0, nil)
rev1(x0, ++(x1, x2))
rev2(x0, nil)
rev2(x0, ++(x1, x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
REV(++(x, y)) → REV2(x, y)
REV2(x, ++(y, z)) → REV(rev2(y, z))
REV2(x, ++(y, z)) → REV2(y, z)
trivial
rev2(x, nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
rev(nil) → nil
REV2(x, ++(y, z)) → REV(++(x, rev(rev2(y, z))))
rev(nil) → nil
rev(++(x, y)) → ++(rev1(x, y), rev2(x, y))
rev1(x, nil) → x
rev1(x, ++(y, z)) → rev1(y, z)
rev2(x, nil) → nil
rev2(x, ++(y, z)) → rev(++(x, rev(rev2(y, z))))
rev(nil)
rev(++(x0, x1))
rev1(x0, nil)
rev1(x0, ++(x1, x2))
rev2(x0, nil)
rev2(x0, ++(x1, x2))