0 QTRS
↳1 AAECC Innermost (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 QDP
↳22 UsableRulesProof (⇔)
↳23 QDP
↳24 QReductionProof (⇔)
↳25 QDP
↳26 Narrowing (⇔)
↳27 QDP
↳28 DependencyGraphProof (⇔)
↳29 QDP
↳30 Narrowing (⇔)
↳31 QDP
↳32 DependencyGraphProof (⇔)
↳33 QDP
↳34 UsableRulesProof (⇔)
↳35 QDP
↳36 QReductionProof (⇔)
↳37 QDP
↳38 Rewriting (⇔)
↳39 QDP
↳40 UsableRulesProof (⇔)
↳41 QDP
↳42 QReductionProof (⇔)
↳43 QDP
↳44 NonInfProof (⇔)
↳45 QDP
↳46 DependencyGraphProof (⇔)
↳47 TRUE
cond1(true, x, y) → cond2(gr(x, y), x, y)
cond2(true, x, y) → cond1(neq(x, 0), y, y)
cond2(false, x, y) → cond1(neq(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
p(0) → 0
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
p(0) → 0
p(s(x)) → x
cond1(true, x, y) → cond2(gr(x, y), x, y)
cond2(true, x, y) → cond1(neq(x, 0), y, y)
cond2(false, x, y) → cond1(neq(x, 0), p(x), y)
cond1(true, x, y) → cond2(gr(x, y), x, y)
cond2(true, x, y) → cond1(neq(x, 0), y, y)
cond2(false, x, y) → cond1(neq(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND1(true, x, y) → GR(x, y)
COND2(true, x, y) → COND1(neq(x, 0), y, y)
COND2(true, x, y) → NEQ(x, 0)
COND2(false, x, y) → COND1(neq(x, 0), p(x), y)
COND2(false, x, y) → NEQ(x, 0)
COND2(false, x, y) → P(x)
GR(s(x), s(y)) → GR(x, y)
NEQ(s(x), s(y)) → NEQ(x, y)
cond1(true, x, y) → cond2(gr(x, y), x, y)
cond2(true, x, y) → cond1(neq(x, 0), y, y)
cond2(false, x, y) → cond1(neq(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
NEQ(s(x), s(y)) → NEQ(x, y)
cond1(true, x, y) → cond2(gr(x, y), x, y)
cond2(true, x, y) → cond1(neq(x, 0), y, y)
cond2(false, x, y) → cond1(neq(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
NEQ(s(x), s(y)) → NEQ(x, y)
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
NEQ(s(x), s(y)) → NEQ(x, y)
From the DPs we obtained the following set of size-change graphs:
GR(s(x), s(y)) → GR(x, y)
cond1(true, x, y) → cond2(gr(x, y), x, y)
cond2(true, x, y) → cond1(neq(x, 0), y, y)
cond2(false, x, y) → cond1(neq(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
GR(s(x), s(y)) → GR(x, y)
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
GR(s(x), s(y)) → GR(x, y)
From the DPs we obtained the following set of size-change graphs:
COND2(true, x, y) → COND1(neq(x, 0), y, y)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, x, y) → COND1(neq(x, 0), p(x), y)
cond1(true, x, y) → cond2(gr(x, y), x, y)
cond2(true, x, y) → cond1(neq(x, 0), y, y)
cond2(false, x, y) → cond1(neq(x, 0), p(x), y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
neq(0, 0) → false
neq(0, s(x)) → true
neq(s(x), 0) → true
neq(s(x), s(y)) → neq(x, y)
p(0) → 0
p(s(x)) → x
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
COND2(true, x, y) → COND1(neq(x, 0), y, y)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, x, y) → COND1(neq(x, 0), p(x), y)
neq(0, 0) → false
neq(s(x), 0) → true
p(0) → 0
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
cond1(true, x0, x1)
cond2(true, x0, x1)
cond2(false, x0, x1)
COND2(true, x, y) → COND1(neq(x, 0), y, y)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, x, y) → COND1(neq(x, 0), p(x), y)
neq(0, 0) → false
neq(s(x), 0) → true
p(0) → 0
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
COND2(true, 0, y1) → COND1(false, y1, y1)
COND2(true, s(x0), y1) → COND1(true, y1, y1)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, x, y) → COND1(neq(x, 0), p(x), y)
COND2(true, 0, y1) → COND1(false, y1, y1)
COND2(true, s(x0), y1) → COND1(true, y1, y1)
neq(0, 0) → false
neq(s(x), 0) → true
p(0) → 0
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
COND2(false, x, y) → COND1(neq(x, 0), p(x), y)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(true, s(x0), y1) → COND1(true, y1, y1)
neq(0, 0) → false
neq(s(x), 0) → true
p(0) → 0
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
COND2(false, 0, y1) → COND1(false, p(0), y1)
COND2(false, s(x0), y1) → COND1(true, p(s(x0)), y1)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(true, s(x0), y1) → COND1(true, y1, y1)
COND2(false, 0, y1) → COND1(false, p(0), y1)
COND2(false, s(x0), y1) → COND1(true, p(s(x0)), y1)
neq(0, 0) → false
neq(s(x), 0) → true
p(0) → 0
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
COND2(true, s(x0), y1) → COND1(true, y1, y1)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, s(x0), y1) → COND1(true, p(s(x0)), y1)
neq(0, 0) → false
neq(s(x), 0) → true
p(0) → 0
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
COND2(true, s(x0), y1) → COND1(true, y1, y1)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, s(x0), y1) → COND1(true, p(s(x0)), y1)
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
p(0)
p(s(x0))
neq(0, 0)
neq(0, s(x0))
neq(s(x0), 0)
neq(s(x0), s(x1))
COND2(true, s(x0), y1) → COND1(true, y1, y1)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, s(x0), y1) → COND1(true, p(s(x0)), y1)
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
COND2(false, s(x0), y1) → COND1(true, x0, y1)
COND2(true, s(x0), y1) → COND1(true, y1, y1)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, s(x0), y1) → COND1(true, x0, y1)
p(s(x)) → x
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
COND2(true, s(x0), y1) → COND1(true, y1, y1)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, s(x0), y1) → COND1(true, x0, y1)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
p(0)
p(s(x0))
p(0)
p(s(x0))
COND2(true, s(x0), y1) → COND1(true, y1, y1)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, s(x0), y1) → COND1(true, x0, y1)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))
(1) (COND2(gr(x2, x3), x2, x3)=COND2(true, s(x4), x5) ⇒ COND2(true, s(x4), x5)≥COND1(true, x5, x5))
(2) (s(x4)=x26∧gr(x26, x3)=true ⇒ COND2(true, s(x4), x3)≥COND1(true, x3, x3))
(3) (true=true∧s(x4)=s(x28) ⇒ COND2(true, s(x4), 0)≥COND1(true, 0, 0))
(4) (gr(x30, x29)=true∧s(x4)=s(x30)∧(∀x31:gr(x30, x29)=true∧s(x31)=x30 ⇒ COND2(true, s(x31), x29)≥COND1(true, x29, x29)) ⇒ COND2(true, s(x4), s(x29))≥COND1(true, s(x29), s(x29)))
(5) (COND2(true, s(x4), 0)≥COND1(true, 0, 0))
(6) (gr(x30, x29)=true ⇒ COND2(true, s(x30), s(x29))≥COND1(true, s(x29), s(x29)))
(7) (true=true ⇒ COND2(true, s(s(x33)), s(0))≥COND1(true, s(0), s(0)))
(8) (gr(x35, x34)=true∧(gr(x35, x34)=true ⇒ COND2(true, s(x35), s(x34))≥COND1(true, s(x34), s(x34))) ⇒ COND2(true, s(s(x35)), s(s(x34)))≥COND1(true, s(s(x34)), s(s(x34))))
(9) (COND2(true, s(s(x33)), s(0))≥COND1(true, s(0), s(0)))
(10) (COND2(true, s(x35), s(x34))≥COND1(true, s(x34), s(x34)) ⇒ COND2(true, s(s(x35)), s(s(x34)))≥COND1(true, s(s(x34)), s(s(x34))))
(11) (COND1(true, x9, x9)=COND1(true, x10, x11) ⇒ COND1(true, x10, x11)≥COND2(gr(x10, x11), x10, x11))
(12) (COND1(true, x9, x9)≥COND2(gr(x9, x9), x9, x9))
(13) (COND1(true, x14, x15)=COND1(true, x16, x17) ⇒ COND1(true, x16, x17)≥COND2(gr(x16, x17), x16, x17))
(14) (COND1(true, x14, x15)≥COND2(gr(x14, x15), x14, x15))
(15) (COND2(gr(x20, x21), x20, x21)=COND2(false, s(x22), x23) ⇒ COND2(false, s(x22), x23)≥COND1(true, x22, x23))
(16) (s(x22)=x36∧gr(x36, x21)=false ⇒ COND2(false, s(x22), x21)≥COND1(true, x22, x21))
(17) (false=false∧s(x22)=0 ⇒ COND2(false, s(x22), x37)≥COND1(true, x22, x37))
(18) (gr(x40, x39)=false∧s(x22)=s(x40)∧(∀x41:gr(x40, x39)=false∧s(x41)=x40 ⇒ COND2(false, s(x41), x39)≥COND1(true, x41, x39)) ⇒ COND2(false, s(x22), s(x39))≥COND1(true, x22, s(x39)))
(19) (gr(x40, x39)=false ⇒ COND2(false, s(x40), s(x39))≥COND1(true, x40, s(x39)))
(20) (false=false ⇒ COND2(false, s(0), s(x42))≥COND1(true, 0, s(x42)))
(21) (gr(x45, x44)=false∧(gr(x45, x44)=false ⇒ COND2(false, s(x45), s(x44))≥COND1(true, x45, s(x44))) ⇒ COND2(false, s(s(x45)), s(s(x44)))≥COND1(true, s(x45), s(s(x44))))
(22) (COND2(false, s(0), s(x42))≥COND1(true, 0, s(x42)))
(23) (COND2(false, s(x45), s(x44))≥COND1(true, x45, s(x44)) ⇒ COND2(false, s(s(x45)), s(s(x44)))≥COND1(true, s(x45), s(s(x44))))
POL(0) = 0
POL(COND1(x1, x2, x3)) = -1 - x1 + x2 + x3
POL(COND2(x1, x2, x3)) = -1 - x1 + x2 + x3
POL(c) = -1
POL(false) = 0
POL(gr(x1, x2)) = 0
POL(s(x1)) = 1 + x1
POL(true) = 0
The following pairs are in Pbound:
COND2(true, s(x0), y1) → COND1(true, y1, y1)
COND2(false, s(x0), y1) → COND1(true, x0, y1)
The following rules are usable:
COND2(true, s(x0), y1) → COND1(true, y1, y1)
COND1(true, x, y) → COND2(gr(x, y), x, y)
COND2(false, s(x0), y1) → COND1(true, x0, y1)
false → gr(0, x)
true → gr(s(x), 0)
gr(x, y) → gr(s(x), s(y))
COND1(true, x, y) → COND2(gr(x, y), x, y)
gr(0, x) → false
gr(s(x), 0) → true
gr(s(x), s(y)) → gr(x, y)
gr(0, x0)
gr(s(x0), 0)
gr(s(x0), s(x1))