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)
LE2 > [le2, true, false, int2, cons, nil]
s1 > [le2, true, false, int2, cons, nil]
0 > [le2, true, false, int2, cons, nil]
LE2: multiset
s1: [1]
le2: [1,2]
0: multiset
true: multiset
false: multiset
int2: [2,1]
cons: []
nil: multiset
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)