rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev1(0, nil) → 0
rev1(s(x), nil) → s(x)
rev1(x, cons(y, l)) → rev1(y, l)
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
↳ QTRS
↳ DependencyPairsProof
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev1(0, nil) → 0
rev1(s(x), nil) → s(x)
rev1(x, cons(y, l)) → rev1(y, l)
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
REV1(x, cons(y, l)) → REV1(y, l)
REV(cons(x, l)) → REV2(x, l)
REV2(x, cons(y, l)) → REV2(y, l)
REV(cons(x, l)) → REV1(x, l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev1(0, nil) → 0
rev1(s(x), nil) → s(x)
rev1(x, cons(y, l)) → rev1(y, l)
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
REV1(x, cons(y, l)) → REV1(y, l)
REV(cons(x, l)) → REV2(x, l)
REV2(x, cons(y, l)) → REV2(y, l)
REV(cons(x, l)) → REV1(x, l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev1(0, nil) → 0
rev1(s(x), nil) → s(x)
rev1(x, cons(y, l)) → rev1(y, l)
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
REV1(x, cons(y, l)) → REV1(y, l)
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev1(0, nil) → 0
rev1(s(x), nil) → s(x)
rev1(x, cons(y, l)) → rev1(y, l)
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
REV1(x, cons(y, l)) → REV1(y, l)
The value of delta used in the strict ordering is 4.
POL(cons(x1, x2)) = 1 + (4)x_1 + (4)x_2
POL(REV1(x1, x2)) = (3)x_1 + (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev1(0, nil) → 0
rev1(s(x), nil) → s(x)
rev1(x, cons(y, l)) → rev1(y, l)
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
REV(cons(x, l)) → REV2(x, l)
REV2(x, cons(y, l)) → REV2(y, l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev1(0, nil) → 0
rev1(s(x), nil) → s(x)
rev1(x, cons(y, l)) → rev1(y, l)
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
REV(cons(x, l)) → REV2(x, l)
REV2(x, cons(y, l)) → REV2(y, l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
The value of delta used in the strict ordering is 1.
POL(REV2(x1, x2)) = 2 + (2)x_2
POL(cons(x1, x2)) = 1 + x_2
POL(rev2(x1, x2)) = x_2
POL(REV(x1)) = 1 + (2)x_1
POL(s(x1)) = 3 + (4)x_1
POL(0) = 2
POL(rev(x1)) = x_1
POL(rev1(x1, x2)) = (4)x_1 + x_2
POL(nil) = 3
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev1(0, nil) → 0
rev1(s(x), nil) → s(x)
rev1(x, cons(y, l)) → rev1(y, l)
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))