0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 QDP
↳5 QDPOrderProof (⇔)
↳6 QDP
↳7 QDPOrderProof (⇔)
↳8 QDP
↳9 PisEmptyProof (⇔)
↳10 TRUE
del(.(x, .(y, z))) → f(=(x, y), x, y, z)
f(true, x, y, z) → del(.(y, z))
f(false, x, y, z) → .(x, del(.(y, z)))
=(nil, nil) → true
=(.(x, y), nil) → false
=(nil, .(y, z)) → false
=(.(x, y), .(u, v)) → and(=(x, u), =(y, v))
DEL(.(x, .(y, z))) → F(=(x, y), x, y, z)
DEL(.(x, .(y, z))) → =1(x, y)
F(true, x, y, z) → DEL(.(y, z))
F(false, x, y, z) → DEL(.(y, z))
=1(.(x, y), .(u, v)) → =1(x, u)
=1(.(x, y), .(u, v)) → =1(y, v)
del(.(x, .(y, z))) → f(=(x, y), x, y, z)
f(true, x, y, z) → del(.(y, z))
f(false, x, y, z) → .(x, del(.(y, z)))
=(nil, nil) → true
=(.(x, y), nil) → false
=(nil, .(y, z)) → false
=(.(x, y), .(u, v)) → and(=(x, u), =(y, v))
F(true, x, y, z) → DEL(.(y, z))
DEL(.(x, .(y, z))) → F(=(x, y), x, y, z)
F(false, x, y, z) → DEL(.(y, z))
del(.(x, .(y, z))) → f(=(x, y), x, y, z)
f(true, x, y, z) → del(.(y, z))
f(false, x, y, z) → .(x, del(.(y, z)))
=(nil, nil) → true
=(.(x, y), nil) → false
=(nil, .(y, z)) → false
=(.(x, y), .(u, v)) → and(=(x, u), =(y, v))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(true, x, y, z) → DEL(.(y, z))
POL(.(x1, x2)) = x1 + x2
POL(=(x1, x2)) = x1
POL(DEL(x1)) = x1
POL(F(x1, x2, x3, x4)) = x1 + x3 + x4
POL(and(x1, x2)) = 0
POL(false) = 0
POL(nil) = 1
POL(true) = 1
POL(u) = 0
POL(v) = 0
=(nil, nil) → true
=(.(x, y), nil) → false
=(nil, .(y, z)) → false
=(.(x, y), .(u, v)) → and(=(x, u), =(y, v))
DEL(.(x, .(y, z))) → F(=(x, y), x, y, z)
F(false, x, y, z) → DEL(.(y, z))
del(.(x, .(y, z))) → f(=(x, y), x, y, z)
f(true, x, y, z) → del(.(y, z))
f(false, x, y, z) → .(x, del(.(y, z)))
=(nil, nil) → true
=(.(x, y), nil) → false
=(nil, .(y, z)) → false
=(.(x, y), .(u, v)) → and(=(x, u), =(y, v))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DEL(.(x, .(y, z))) → F(=(x, y), x, y, z)
F(false, x, y, z) → DEL(.(y, z))
POL(.(x1, x2)) = 1 + x2
POL(=(x1, x2)) = 0
POL(DEL(x1)) = 1 + x1
POL(F(x1, x2, x3, x4)) = 1 + x4
POL(and(x1, x2)) = 1
POL(false) = 1
POL(nil) = 0
POL(true) = 1
POL(u) = 0
POL(v) = 0
del(.(x, .(y, z))) → f(=(x, y), x, y, z)
f(true, x, y, z) → del(.(y, z))
f(false, x, y, z) → .(x, del(.(y, z)))
=(nil, nil) → true
=(.(x, y), nil) → false
=(nil, .(y, z)) → false
=(.(x, y), .(u, v)) → and(=(x, u), =(y, v))