0 QTRS
↳1 AAECC Innermost (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 QDPOrderProof (⇔)
↳9 QDP
↳10 PisEmptyProof (⇔)
↳11 TRUE
↳12 QDP
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
f(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)
F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z)
F(true, x, y, z) → AND(gt(x, y), gt(x, z))
F(true, x, y, z) → GT(x, y)
F(true, x, y, z) → GT(x, z)
F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, y, s(z))
GT(s(u), s(v)) → GT(u, v)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
f(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)
GT(s(u), s(v)) → GT(u, v)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
f(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GT(s(u), s(v)) → GT(u, v)
s1 > true
f > true
and1 > false > true
gt > false > true
0 > true
s1: multiset
f: multiset
true: multiset
and1: multiset
gt: []
0: multiset
false: multiset
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
f(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)
F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, y, s(z))
F(true, x, y, z) → F(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, s(y), z)
f(true, x, y, z) → f(and(gt(x, y), gt(x, z)), x, y, s(z))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
f(true, x0, x1, x2)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
and(x0, true)
and(x0, false)