0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 QDPOrderProof (⇔)
↳9 QDP
↳10 PisEmptyProof (⇔)
↳11 TRUE
↳12 QDP
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
int(x, y) → if(le(x, y), x, y)
if(true, x, y) → cons(x, int(s(x), y))
if(false, x, y) → nil
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
int(x, y) → if(le(x, y), x, y)
if(true, x, y) → cons(x, int(s(x), y))
if(false, x, y) → nil
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
int(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
LE(s(x), s(y)) → LE(x, y)
INT(x, y) → IF(le(x, y), x, y)
INT(x, y) → LE(x, y)
IF(true, x, y) → INT(s(x), y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
int(x, y) → if(le(x, y), x, y)
if(true, x, y) → cons(x, int(s(x), y))
if(false, x, y) → nil
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
int(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
LE(s(x), s(y)) → LE(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
int(x, y) → if(le(x, y), x, y)
if(true, x, y) → cons(x, int(s(x), y))
if(false, x, y) → nil
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
int(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LE(s(x), s(y)) → LE(x, y)
0 > true > s1 > false
0 > true > cons > false
int2 > le2 > true > s1 > false
int2 > le2 > true > cons > false
int2 > if3 > nil > false
int2: [1,2]
if3: [1,2,3]
cons: []
le2: [2,1]
true: []
false: []
s1: [1]
0: []
nil: []
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
int(x, y) → if(le(x, y), x, y)
if(true, x, y) → cons(x, int(s(x), y))
if(false, x, y) → nil
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
int(x, y) → if(le(x, y), x, y)
if(true, x, y) → cons(x, int(s(x), y))
if(false, x, y) → nil
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
int(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
INT(x, y) → IF(le(x, y), x, y)
IF(true, x, y) → INT(s(x), y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
int(x, y) → if(le(x, y), x, y)
if(true, x, y) → cons(x, int(s(x), y))
if(false, x, y) → nil
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
int(x0, x1)
if(true, x0, x1)
if(false, x0, x1)