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
↳13 QDPOrderProof (⇔)
↳14 QDP
↳15 PisEmptyProof (⇔)
↳16 TRUE
↳17 QDP
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), p(x), p(y))
cond2(false, x, y) → cond1(and(eq(x, y), gr(x, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
eq(0, 0) → true
eq(s(x), 0) → false
eq(0, s(x)) → false
eq(s(x), s(y)) → eq(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
eq(0, 0) → true
eq(s(x), 0) → false
eq(0, s(x)) → false
eq(s(x), s(y)) → eq(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), p(x), p(y))
cond2(false, x, y) → cond1(and(eq(x, y), gr(x, 0)), x, y)
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), p(x), p(y))
cond2(false, x, y) → cond1(and(eq(x, y), gr(x, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
eq(0, 0) → true
eq(s(x), 0) → false
eq(0, s(x)) → false
eq(s(x), s(y)) → eq(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
eq(0, 0)
eq(s(x0), 0)
eq(0, s(x0))
eq(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
COND1(true, x, y) → COND2(gr(y, 0), x, y)
COND1(true, x, y) → GR(y, 0)
COND2(true, x, y) → COND2(gr(y, 0), p(x), p(y))
COND2(true, x, y) → GR(y, 0)
COND2(true, x, y) → P(x)
COND2(true, x, y) → P(y)
COND2(false, x, y) → COND1(and(eq(x, y), gr(x, 0)), x, y)
COND2(false, x, y) → AND(eq(x, y), gr(x, 0))
COND2(false, x, y) → EQ(x, y)
COND2(false, x, y) → GR(x, 0)
GR(s(x), s(y)) → GR(x, y)
EQ(s(x), s(y)) → EQ(x, y)
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), p(x), p(y))
cond2(false, x, y) → cond1(and(eq(x, y), gr(x, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
eq(0, 0) → true
eq(s(x), 0) → false
eq(0, s(x)) → false
eq(s(x), s(y)) → eq(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
eq(0, 0)
eq(s(x0), 0)
eq(0, s(x0))
eq(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
EQ(s(x), s(y)) → EQ(x, y)
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), p(x), p(y))
cond2(false, x, y) → cond1(and(eq(x, y), gr(x, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
eq(0, 0) → true
eq(s(x), 0) → false
eq(0, s(x)) → false
eq(s(x), s(y)) → eq(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
eq(0, 0)
eq(s(x0), 0)
eq(0, s(x0))
eq(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
EQ(s(x), s(y)) → EQ(x, y)
gr > [s1, false]
gr > true
0 > [s1, false]
0 > true
and2 > [s1, false]
and2 > true
s1: multiset
true: multiset
gr: []
0: multiset
false: multiset
and2: multiset
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), p(x), p(y))
cond2(false, x, y) → cond1(and(eq(x, y), gr(x, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
eq(0, 0) → true
eq(s(x), 0) → false
eq(0, s(x)) → false
eq(s(x), s(y)) → eq(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), p(x), p(y))
cond2(false, x, y) → cond1(and(eq(x, y), gr(x, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
eq(0, 0) → true
eq(s(x), 0) → false
eq(0, s(x)) → false
eq(s(x), s(y)) → eq(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
eq(0, 0)
eq(s(x0), 0)
eq(0, s(x0))
eq(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
GR(s(x), s(y)) → GR(x, y)
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), p(x), p(y))
cond2(false, x, y) → cond1(and(eq(x, y), gr(x, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
eq(0, 0) → true
eq(s(x), 0) → false
eq(0, s(x)) → false
eq(s(x), s(y)) → eq(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
eq(0, 0)
eq(s(x0), 0)
eq(0, s(x0))
eq(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GR(s(x), s(y)) → GR(x, y)
0 > [s1, gr, false] > true
and2 > [s1, gr, false] > true
s1: multiset
true: multiset
gr: multiset
0: multiset
false: multiset
and2: multiset
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), p(x), p(y))
cond2(false, x, y) → cond1(and(eq(x, y), gr(x, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
eq(0, 0) → true
eq(s(x), 0) → false
eq(0, s(x)) → false
eq(s(x), s(y)) → eq(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), p(x), p(y))
cond2(false, x, y) → cond1(and(eq(x, y), gr(x, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
eq(0, 0) → true
eq(s(x), 0) → false
eq(0, s(x)) → false
eq(s(x), s(y)) → eq(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
eq(0, 0)
eq(s(x0), 0)
eq(0, s(x0))
eq(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)
COND2(true, x, y) → COND2(gr(y, 0), p(x), p(y))
COND2(false, x, y) → COND1(and(eq(x, y), gr(x, 0)), x, y)
COND1(true, x, y) → COND2(gr(y, 0), x, y)
cond1(true, x, y) → cond2(gr(y, 0), x, y)
cond2(true, x, y) → cond2(gr(y, 0), p(x), p(y))
cond2(false, x, y) → cond1(and(eq(x, y), gr(x, 0)), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
p(0) → 0
p(s(x)) → x
eq(0, 0) → true
eq(s(x), 0) → false
eq(0, s(x)) → false
eq(s(x), s(y)) → eq(x, y)
and(true, true) → true
and(false, x) → false
and(x, false) → false
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
eq(0, 0)
eq(s(x0), 0)
eq(0, s(x0))
eq(s(x0), s(x1))
and(true, true)
and(false, x0)
and(x0, false)