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 QDPSizeChangeProof (⇔)
↳27 TRUE
↳28 QDP
↳29 UsableRulesProof (⇔)
↳30 QDP
↳31 QReductionProof (⇔)
↳32 QDP
↳33 Instantiation (⇔)
↳34 QDP
↳35 NonInfProof (⇔)
↳36 QDP
↳37 Instantiation (⇔)
↳38 QDP
↳39 NonInfProof (⇔)
↳40 QDP
↳41 PisEmptyProof (⇔)
↳42 TRUE
le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)
double(0) → 0
double(s(x)) → s(s(double(x)))
le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)
le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)
LE(0, y, z) → GREATER(y, z)
LE(s(x), s(y), s(z)) → LE(x, y, z)
GREATER(s(x), s(y)) → GREATER(x, y)
DOUBLE(s(x)) → DOUBLE(x)
TRIPLE(x) → IF(le(x, x, double(x)), x, 0, 0)
TRIPLE(x) → LE(x, x, double(x))
TRIPLE(x) → DOUBLE(x)
IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))
IF(first, x, y, z) → LE(s(x), y, s(z))
IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
IF(second, x, y, z) → LE(s(x), s(y), z)
le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)
DOUBLE(s(x)) → DOUBLE(x)
le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)
DOUBLE(s(x)) → DOUBLE(x)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)
DOUBLE(s(x)) → DOUBLE(x)
From the DPs we obtained the following set of size-change graphs:
GREATER(s(x), s(y)) → GREATER(x, y)
le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)
GREATER(s(x), s(y)) → GREATER(x, y)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)
GREATER(s(x), s(y)) → GREATER(x, y)
From the DPs we obtained the following set of size-change graphs:
LE(s(x), s(y), s(z)) → LE(x, y, z)
le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)
LE(s(x), s(y), s(z)) → LE(x, y, z)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)
LE(s(x), s(y), s(z)) → LE(x, y, z)
From the DPs we obtained the following set of size-change graphs:
IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))
le(0, y, z) → greater(y, z)
le(s(x), 0, z) → false
le(s(x), s(y), 0) → false
le(s(x), s(y), s(z)) → le(x, y, z)
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
triple(x) → if(le(x, x, double(x)), x, 0, 0)
if(false, x, y, z) → true
if(first, x, y, z) → if(le(s(x), y, s(z)), s(x), y, s(z))
if(second, x, y, z) → if(le(s(x), s(y), z), s(x), s(y), z)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)
IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))
le(s(x), 0, z) → false
le(s(x), s(y), s(z)) → le(x, y, z)
le(0, y, z) → greater(y, z)
le(s(x), s(y), 0) → false
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)
double(0)
double(s(x0))
triple(x0)
if(false, x0, x1, x2)
if(first, x0, x1, x2)
if(second, x0, x1, x2)
IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))
le(s(x), 0, z) → false
le(s(x), s(y), s(z)) → le(x, y, z)
le(0, y, z) → greater(y, z)
le(s(x), s(y), 0) → false
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
IF(second, s(z0), s(z1), z2) → IF(le(s(s(z0)), s(s(z1)), z2), s(s(z0)), s(s(z1)), z2)
IF(second, s(z0), z1, s(z2)) → IF(le(s(s(z0)), s(z1), s(z2)), s(s(z0)), s(z1), s(z2))
IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))
IF(second, s(z0), s(z1), z2) → IF(le(s(s(z0)), s(s(z1)), z2), s(s(z0)), s(s(z1)), z2)
IF(second, s(z0), z1, s(z2)) → IF(le(s(s(z0)), s(z1), s(z2)), s(s(z0)), s(z1), s(z2))
le(s(x), 0, z) → false
le(s(x), s(y), s(z)) → le(x, y, z)
le(0, y, z) → greater(y, z)
le(s(x), s(y), 0) → false
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
(1) (IF(le(s(x0), s(x1), x2), s(x0), s(x1), x2)=IF(second, x3, x4, x5) ⇒ IF(second, x3, x4, x5)≥IF(le(s(x3), s(x4), x5), s(x3), s(x4), x5))
(2) (s(x0)=x24∧s(x1)=x25∧le(x24, x25, x2)=second ⇒ IF(second, s(x0), s(x1), x2)≥IF(le(s(s(x0)), s(s(x1)), x2), s(s(x0)), s(s(x1)), x2))
(3) (le(x30, x29, x28)=second∧s(x0)=s(x30)∧s(x1)=s(x29)∧(∀x31,x32:le(x30, x29, x28)=second∧s(x31)=x30∧s(x32)=x29 ⇒ IF(second, s(x31), s(x32), x28)≥IF(le(s(s(x31)), s(s(x32)), x28), s(s(x31)), s(s(x32)), x28)) ⇒ IF(second, s(x0), s(x1), s(x28))≥IF(le(s(s(x0)), s(s(x1)), s(x28)), s(s(x0)), s(s(x1)), s(x28)))
(4) (greater(x34, x33)=second∧s(x0)=0∧s(x1)=x34 ⇒ IF(second, s(x0), s(x1), x33)≥IF(le(s(s(x0)), s(s(x1)), x33), s(s(x0)), s(s(x1)), x33))
(5) (le(x30, x29, x28)=second ⇒ IF(second, s(x30), s(x29), s(x28))≥IF(le(s(s(x30)), s(s(x29)), s(x28)), s(s(x30)), s(s(x29)), s(x28)))
(6) (le(x41, x40, x39)=second∧(le(x41, x40, x39)=second ⇒ IF(second, s(x41), s(x40), s(x39))≥IF(le(s(s(x41)), s(s(x40)), s(x39)), s(s(x41)), s(s(x40)), s(x39))) ⇒ IF(second, s(s(x41)), s(s(x40)), s(s(x39)))≥IF(le(s(s(s(x41))), s(s(s(x40))), s(s(x39))), s(s(s(x41))), s(s(s(x40))), s(s(x39))))
(7) (greater(x43, x42)=second ⇒ IF(second, s(0), s(x43), s(x42))≥IF(le(s(s(0)), s(s(x43)), s(x42)), s(s(0)), s(s(x43)), s(x42)))
(8) (IF(second, s(x41), s(x40), s(x39))≥IF(le(s(s(x41)), s(s(x40)), s(x39)), s(s(x41)), s(s(x40)), s(x39)) ⇒ IF(second, s(s(x41)), s(s(x40)), s(s(x39)))≥IF(le(s(s(s(x41))), s(s(s(x40))), s(s(x39))), s(s(s(x41))), s(s(s(x40))), s(s(x39))))
(9) (IF(second, s(0), s(x43), s(x42))≥IF(le(s(s(0)), s(s(x43)), s(x42)), s(s(0)), s(s(x43)), s(x42)))
(10) (IF(le(s(x6), x7, s(x8)), s(x6), x7, s(x8))=IF(second, x9, x10, x11) ⇒ IF(second, x9, x10, x11)≥IF(le(s(x9), s(x10), x11), s(x9), s(x10), x11))
(11) (s(x6)=x46∧s(x8)=x47∧le(x46, x7, x47)=second ⇒ IF(second, s(x6), x7, s(x8))≥IF(le(s(s(x6)), s(x7), s(x8)), s(s(x6)), s(x7), s(x8)))
(12) (le(x52, x51, x50)=second∧s(x6)=s(x52)∧s(x8)=s(x50)∧(∀x53,x54:le(x52, x51, x50)=second∧s(x53)=x52∧s(x54)=x50 ⇒ IF(second, s(x53), x51, s(x54))≥IF(le(s(s(x53)), s(x51), s(x54)), s(s(x53)), s(x51), s(x54))) ⇒ IF(second, s(x6), s(x51), s(x8))≥IF(le(s(s(x6)), s(s(x51)), s(x8)), s(s(x6)), s(s(x51)), s(x8)))
(13) (greater(x56, x55)=second∧s(x6)=0∧s(x8)=x55 ⇒ IF(second, s(x6), x56, s(x8))≥IF(le(s(s(x6)), s(x56), s(x8)), s(s(x6)), s(x56), s(x8)))
(14) (le(x52, x51, x50)=second ⇒ IF(second, s(x52), s(x51), s(x50))≥IF(le(s(s(x52)), s(s(x51)), s(x50)), s(s(x52)), s(s(x51)), s(x50)))
(15) (le(x63, x62, x61)=second∧(le(x63, x62, x61)=second ⇒ IF(second, s(x63), s(x62), s(x61))≥IF(le(s(s(x63)), s(s(x62)), s(x61)), s(s(x63)), s(s(x62)), s(x61))) ⇒ IF(second, s(s(x63)), s(s(x62)), s(s(x61)))≥IF(le(s(s(s(x63))), s(s(s(x62))), s(s(x61))), s(s(s(x63))), s(s(s(x62))), s(s(x61))))
(16) (greater(x65, x64)=second ⇒ IF(second, s(0), s(x65), s(x64))≥IF(le(s(s(0)), s(s(x65)), s(x64)), s(s(0)), s(s(x65)), s(x64)))
(17) (IF(second, s(x63), s(x62), s(x61))≥IF(le(s(s(x63)), s(s(x62)), s(x61)), s(s(x63)), s(s(x62)), s(x61)) ⇒ IF(second, s(s(x63)), s(s(x62)), s(s(x61)))≥IF(le(s(s(s(x63))), s(s(s(x62))), s(s(x61))), s(s(s(x63))), s(s(s(x62))), s(s(x61))))
(18) (IF(second, s(0), s(x65), s(x64))≥IF(le(s(s(0)), s(s(x65)), s(x64)), s(s(0)), s(s(x65)), s(x64)))
(19) (IF(le(s(x12), s(x13), x14), s(x12), s(x13), x14)=IF(first, x15, x16, x17) ⇒ IF(first, x15, x16, x17)≥IF(le(s(x15), x16, s(x17)), s(x15), x16, s(x17)))
(20) (s(x12)=x68∧s(x13)=x69∧le(x68, x69, x14)=first ⇒ IF(first, s(x12), s(x13), x14)≥IF(le(s(s(x12)), s(x13), s(x14)), s(s(x12)), s(x13), s(x14)))
(21) (le(x74, x73, x72)=first∧s(x12)=s(x74)∧s(x13)=s(x73)∧(∀x75,x76:le(x74, x73, x72)=first∧s(x75)=x74∧s(x76)=x73 ⇒ IF(first, s(x75), s(x76), x72)≥IF(le(s(s(x75)), s(x76), s(x72)), s(s(x75)), s(x76), s(x72))) ⇒ IF(first, s(x12), s(x13), s(x72))≥IF(le(s(s(x12)), s(x13), s(s(x72))), s(s(x12)), s(x13), s(s(x72))))
(22) (greater(x78, x77)=first∧s(x12)=0∧s(x13)=x78 ⇒ IF(first, s(x12), s(x13), x77)≥IF(le(s(s(x12)), s(x13), s(x77)), s(s(x12)), s(x13), s(x77)))
(23) (le(x74, x73, x72)=first ⇒ IF(first, s(x74), s(x73), s(x72))≥IF(le(s(s(x74)), s(x73), s(s(x72))), s(s(x74)), s(x73), s(s(x72))))
(24) (le(x85, x84, x83)=first∧(le(x85, x84, x83)=first ⇒ IF(first, s(x85), s(x84), s(x83))≥IF(le(s(s(x85)), s(x84), s(s(x83))), s(s(x85)), s(x84), s(s(x83)))) ⇒ IF(first, s(s(x85)), s(s(x84)), s(s(x83)))≥IF(le(s(s(s(x85))), s(s(x84)), s(s(s(x83)))), s(s(s(x85))), s(s(x84)), s(s(s(x83)))))
(25) (greater(x87, x86)=first ⇒ IF(first, s(0), s(x87), s(x86))≥IF(le(s(s(0)), s(x87), s(s(x86))), s(s(0)), s(x87), s(s(x86))))
(26) (IF(first, s(x85), s(x84), s(x83))≥IF(le(s(s(x85)), s(x84), s(s(x83))), s(s(x85)), s(x84), s(s(x83))) ⇒ IF(first, s(s(x85)), s(s(x84)), s(s(x83)))≥IF(le(s(s(s(x85))), s(s(x84)), s(s(s(x83)))), s(s(s(x85))), s(s(x84)), s(s(s(x83)))))
(27) (IF(first, s(0), s(x87), s(x86))≥IF(le(s(s(0)), s(x87), s(s(x86))), s(s(0)), s(x87), s(s(x86))))
(28) (IF(le(s(x18), x19, s(x20)), s(x18), x19, s(x20))=IF(first, x21, x22, x23) ⇒ IF(first, x21, x22, x23)≥IF(le(s(x21), x22, s(x23)), s(x21), x22, s(x23)))
(29) (s(x18)=x90∧s(x20)=x91∧le(x90, x19, x91)=first ⇒ IF(first, s(x18), x19, s(x20))≥IF(le(s(s(x18)), x19, s(s(x20))), s(s(x18)), x19, s(s(x20))))
(30) (le(x96, x95, x94)=first∧s(x18)=s(x96)∧s(x20)=s(x94)∧(∀x97,x98:le(x96, x95, x94)=first∧s(x97)=x96∧s(x98)=x94 ⇒ IF(first, s(x97), x95, s(x98))≥IF(le(s(s(x97)), x95, s(s(x98))), s(s(x97)), x95, s(s(x98)))) ⇒ IF(first, s(x18), s(x95), s(x20))≥IF(le(s(s(x18)), s(x95), s(s(x20))), s(s(x18)), s(x95), s(s(x20))))
(31) (greater(x100, x99)=first∧s(x18)=0∧s(x20)=x99 ⇒ IF(first, s(x18), x100, s(x20))≥IF(le(s(s(x18)), x100, s(s(x20))), s(s(x18)), x100, s(s(x20))))
(32) (le(x96, x95, x94)=first ⇒ IF(first, s(x96), s(x95), s(x94))≥IF(le(s(s(x96)), s(x95), s(s(x94))), s(s(x96)), s(x95), s(s(x94))))
(33) (le(x107, x106, x105)=first∧(le(x107, x106, x105)=first ⇒ IF(first, s(x107), s(x106), s(x105))≥IF(le(s(s(x107)), s(x106), s(s(x105))), s(s(x107)), s(x106), s(s(x105)))) ⇒ IF(first, s(s(x107)), s(s(x106)), s(s(x105)))≥IF(le(s(s(s(x107))), s(s(x106)), s(s(s(x105)))), s(s(s(x107))), s(s(x106)), s(s(s(x105)))))
(34) (greater(x109, x108)=first ⇒ IF(first, s(0), s(x109), s(x108))≥IF(le(s(s(0)), s(x109), s(s(x108))), s(s(0)), s(x109), s(s(x108))))
(35) (IF(first, s(x107), s(x106), s(x105))≥IF(le(s(s(x107)), s(x106), s(s(x105))), s(s(x107)), s(x106), s(s(x105))) ⇒ IF(first, s(s(x107)), s(s(x106)), s(s(x105)))≥IF(le(s(s(s(x107))), s(s(x106)), s(s(s(x105)))), s(s(s(x107))), s(s(x106)), s(s(s(x105)))))
(36) (IF(first, s(0), s(x109), s(x108))≥IF(le(s(s(0)), s(x109), s(s(x108))), s(s(0)), s(x109), s(s(x108))))
POL(0) = 0
POL(IF(x1, x2, x3, x4)) = -1 - x1 - x2 + x4
POL(c) = -1
POL(false) = 0
POL(first) = 0
POL(greater(x1, x2)) = 0
POL(le(x1, x2, x3)) = 0
POL(s(x1)) = 1 + x1
POL(second) = 0
The following pairs are in Pbound:
IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
The following rules are usable:
IF(second, x, y, z) → IF(le(s(x), s(y), z), s(x), s(y), z)
IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))
first → greater(x, 0)
false → le(s(x), s(y), 0)
greater(x, y) → greater(s(x), s(y))
second → greater(0, s(y))
le(x, y, z) → le(s(x), s(y), s(z))
greater(y, z) → le(0, y, z)
false → le(s(x), 0, z)
IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))
le(s(x), 0, z) → false
le(s(x), s(y), s(z)) → le(x, y, z)
le(0, y, z) → greater(y, z)
le(s(x), s(y), 0) → false
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
IF(first, s(z0), z1, s(z2)) → IF(le(s(s(z0)), z1, s(s(z2))), s(s(z0)), z1, s(s(z2)))
IF(first, s(z0), z1, s(z2)) → IF(le(s(s(z0)), z1, s(s(z2))), s(s(z0)), z1, s(s(z2)))
le(s(x), 0, z) → false
le(s(x), s(y), s(z)) → le(x, y, z)
le(0, y, z) → greater(y, z)
le(s(x), s(y), 0) → false
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))
(1) (IF(le(s(x18), x19, s(x20)), s(x18), x19, s(x20))=IF(first, x21, x22, x23) ⇒ IF(first, x21, x22, x23)≥IF(le(s(x21), x22, s(x23)), s(x21), x22, s(x23)))
(2) (s(x18)=x90∧s(x20)=x91∧le(x90, x19, x91)=first ⇒ IF(first, s(x18), x19, s(x20))≥IF(le(s(s(x18)), x19, s(s(x20))), s(s(x18)), x19, s(s(x20))))
(3) (le(x96, x95, x94)=first∧s(x18)=s(x96)∧s(x20)=s(x94)∧(∀x97,x98:le(x96, x95, x94)=first∧s(x97)=x96∧s(x98)=x94 ⇒ IF(first, s(x97), x95, s(x98))≥IF(le(s(s(x97)), x95, s(s(x98))), s(s(x97)), x95, s(s(x98)))) ⇒ IF(first, s(x18), s(x95), s(x20))≥IF(le(s(s(x18)), s(x95), s(s(x20))), s(s(x18)), s(x95), s(s(x20))))
(4) (greater(x100, x99)=first∧s(x18)=0∧s(x20)=x99 ⇒ IF(first, s(x18), x100, s(x20))≥IF(le(s(s(x18)), x100, s(s(x20))), s(s(x18)), x100, s(s(x20))))
(5) (le(x96, x95, x94)=first ⇒ IF(first, s(x96), s(x95), s(x94))≥IF(le(s(s(x96)), s(x95), s(s(x94))), s(s(x96)), s(x95), s(s(x94))))
(6) (le(x107, x106, x105)=first∧(le(x107, x106, x105)=first ⇒ IF(first, s(x107), s(x106), s(x105))≥IF(le(s(s(x107)), s(x106), s(s(x105))), s(s(x107)), s(x106), s(s(x105)))) ⇒ IF(first, s(s(x107)), s(s(x106)), s(s(x105)))≥IF(le(s(s(s(x107))), s(s(x106)), s(s(s(x105)))), s(s(s(x107))), s(s(x106)), s(s(s(x105)))))
(7) (greater(x109, x108)=first ⇒ IF(first, s(0), s(x109), s(x108))≥IF(le(s(s(0)), s(x109), s(s(x108))), s(s(0)), s(x109), s(s(x108))))
(8) (IF(first, s(x107), s(x106), s(x105))≥IF(le(s(s(x107)), s(x106), s(s(x105))), s(s(x107)), s(x106), s(s(x105))) ⇒ IF(first, s(s(x107)), s(s(x106)), s(s(x105)))≥IF(le(s(s(s(x107))), s(s(x106)), s(s(s(x105)))), s(s(s(x107))), s(s(x106)), s(s(s(x105)))))
(9) (IF(first, s(0), s(x109), s(x108))≥IF(le(s(s(0)), s(x109), s(s(x108))), s(s(0)), s(x109), s(s(x108))))
POL(0) = 0
POL(IF(x1, x2, x3, x4)) = -1 - x1 - x2 + x3
POL(c) = -1
POL(false) = 0
POL(first) = 0
POL(greater(x1, x2)) = 0
POL(le(x1, x2, x3)) = 0
POL(s(x1)) = 1 + x1
POL(second) = 0
The following pairs are in Pbound:
IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))
The following rules are usable:
IF(first, x, y, z) → IF(le(s(x), y, s(z)), s(x), y, s(z))
first → greater(x, 0)
false → le(s(x), s(y), 0)
greater(x, y) → greater(s(x), s(y))
second → greater(0, s(y))
le(x, y, z) → le(s(x), s(y), s(z))
greater(y, z) → le(0, y, z)
false → le(s(x), 0, z)
le(s(x), 0, z) → false
le(s(x), s(y), s(z)) → le(x, y, z)
le(0, y, z) → greater(y, z)
le(s(x), s(y), 0) → false
greater(x, 0) → first
greater(0, s(y)) → second
greater(s(x), s(y)) → greater(x, y)
le(0, x0, x1)
le(s(x0), 0, x1)
le(s(x0), s(x1), 0)
le(s(x0), s(x1), s(x2))
greater(x0, 0)
greater(0, s(x0))
greater(s(x0), s(x1))