+2(x, 0) -> x
+2(x, s1(y)) -> s1(+2(x, y))
*2(x, 0) -> 0
*2(x, s1(y)) -> +2(*2(x, y), x)
ge2(x, 0) -> true
ge2(0, s1(y)) -> false
ge2(s1(x), s1(y)) -> ge2(x, y)
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
fact1(x) -> iffact2(x, ge2(x, s1(s1(0))))
iffact2(x, true) -> *2(x, fact1(-2(x, s1(0))))
iffact2(x, false) -> s1(0)
↳ QTRS
↳ DependencyPairsProof
+2(x, 0) -> x
+2(x, s1(y)) -> s1(+2(x, y))
*2(x, 0) -> 0
*2(x, s1(y)) -> +2(*2(x, y), x)
ge2(x, 0) -> true
ge2(0, s1(y)) -> false
ge2(s1(x), s1(y)) -> ge2(x, y)
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
fact1(x) -> iffact2(x, ge2(x, s1(s1(0))))
iffact2(x, true) -> *2(x, fact1(-2(x, s1(0))))
iffact2(x, false) -> s1(0)
IFFACT2(x, true) -> *12(x, fact1(-2(x, s1(0))))
*12(x, s1(y)) -> +12(*2(x, y), x)
+12(x, s1(y)) -> +12(x, y)
*12(x, s1(y)) -> *12(x, y)
FACT1(x) -> IFFACT2(x, ge2(x, s1(s1(0))))
-12(s1(x), s1(y)) -> -12(x, y)
IFFACT2(x, true) -> FACT1(-2(x, s1(0)))
IFFACT2(x, true) -> -12(x, s1(0))
FACT1(x) -> GE2(x, s1(s1(0)))
GE2(s1(x), s1(y)) -> GE2(x, y)
+2(x, 0) -> x
+2(x, s1(y)) -> s1(+2(x, y))
*2(x, 0) -> 0
*2(x, s1(y)) -> +2(*2(x, y), x)
ge2(x, 0) -> true
ge2(0, s1(y)) -> false
ge2(s1(x), s1(y)) -> ge2(x, y)
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
fact1(x) -> iffact2(x, ge2(x, s1(s1(0))))
iffact2(x, true) -> *2(x, fact1(-2(x, s1(0))))
iffact2(x, false) -> s1(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
IFFACT2(x, true) -> *12(x, fact1(-2(x, s1(0))))
*12(x, s1(y)) -> +12(*2(x, y), x)
+12(x, s1(y)) -> +12(x, y)
*12(x, s1(y)) -> *12(x, y)
FACT1(x) -> IFFACT2(x, ge2(x, s1(s1(0))))
-12(s1(x), s1(y)) -> -12(x, y)
IFFACT2(x, true) -> FACT1(-2(x, s1(0)))
IFFACT2(x, true) -> -12(x, s1(0))
FACT1(x) -> GE2(x, s1(s1(0)))
GE2(s1(x), s1(y)) -> GE2(x, y)
+2(x, 0) -> x
+2(x, s1(y)) -> s1(+2(x, y))
*2(x, 0) -> 0
*2(x, s1(y)) -> +2(*2(x, y), x)
ge2(x, 0) -> true
ge2(0, s1(y)) -> false
ge2(s1(x), s1(y)) -> ge2(x, y)
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
fact1(x) -> iffact2(x, ge2(x, s1(s1(0))))
iffact2(x, true) -> *2(x, fact1(-2(x, s1(0))))
iffact2(x, false) -> s1(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
-12(s1(x), s1(y)) -> -12(x, y)
+2(x, 0) -> x
+2(x, s1(y)) -> s1(+2(x, y))
*2(x, 0) -> 0
*2(x, s1(y)) -> +2(*2(x, y), x)
ge2(x, 0) -> true
ge2(0, s1(y)) -> false
ge2(s1(x), s1(y)) -> ge2(x, y)
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
fact1(x) -> iffact2(x, ge2(x, s1(s1(0))))
iffact2(x, true) -> *2(x, fact1(-2(x, s1(0))))
iffact2(x, false) -> s1(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
-12(s1(x), s1(y)) -> -12(x, y)
POL(-12(x1, x2)) = x2
POL(s1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
+2(x, 0) -> x
+2(x, s1(y)) -> s1(+2(x, y))
*2(x, 0) -> 0
*2(x, s1(y)) -> +2(*2(x, y), x)
ge2(x, 0) -> true
ge2(0, s1(y)) -> false
ge2(s1(x), s1(y)) -> ge2(x, y)
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
fact1(x) -> iffact2(x, ge2(x, s1(s1(0))))
iffact2(x, true) -> *2(x, fact1(-2(x, s1(0))))
iffact2(x, false) -> s1(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
GE2(s1(x), s1(y)) -> GE2(x, y)
+2(x, 0) -> x
+2(x, s1(y)) -> s1(+2(x, y))
*2(x, 0) -> 0
*2(x, s1(y)) -> +2(*2(x, y), x)
ge2(x, 0) -> true
ge2(0, s1(y)) -> false
ge2(s1(x), s1(y)) -> ge2(x, y)
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
fact1(x) -> iffact2(x, ge2(x, s1(s1(0))))
iffact2(x, true) -> *2(x, fact1(-2(x, s1(0))))
iffact2(x, false) -> s1(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GE2(s1(x), s1(y)) -> GE2(x, y)
POL(GE2(x1, x2)) = x2
POL(s1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
+2(x, 0) -> x
+2(x, s1(y)) -> s1(+2(x, y))
*2(x, 0) -> 0
*2(x, s1(y)) -> +2(*2(x, y), x)
ge2(x, 0) -> true
ge2(0, s1(y)) -> false
ge2(s1(x), s1(y)) -> ge2(x, y)
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
fact1(x) -> iffact2(x, ge2(x, s1(s1(0))))
iffact2(x, true) -> *2(x, fact1(-2(x, s1(0))))
iffact2(x, false) -> s1(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
+12(x, s1(y)) -> +12(x, y)
+2(x, 0) -> x
+2(x, s1(y)) -> s1(+2(x, y))
*2(x, 0) -> 0
*2(x, s1(y)) -> +2(*2(x, y), x)
ge2(x, 0) -> true
ge2(0, s1(y)) -> false
ge2(s1(x), s1(y)) -> ge2(x, y)
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
fact1(x) -> iffact2(x, ge2(x, s1(s1(0))))
iffact2(x, true) -> *2(x, fact1(-2(x, s1(0))))
iffact2(x, false) -> s1(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
+12(x, s1(y)) -> +12(x, y)
POL(+12(x1, x2)) = x2
POL(s1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
+2(x, 0) -> x
+2(x, s1(y)) -> s1(+2(x, y))
*2(x, 0) -> 0
*2(x, s1(y)) -> +2(*2(x, y), x)
ge2(x, 0) -> true
ge2(0, s1(y)) -> false
ge2(s1(x), s1(y)) -> ge2(x, y)
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
fact1(x) -> iffact2(x, ge2(x, s1(s1(0))))
iffact2(x, true) -> *2(x, fact1(-2(x, s1(0))))
iffact2(x, false) -> s1(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
*12(x, s1(y)) -> *12(x, y)
+2(x, 0) -> x
+2(x, s1(y)) -> s1(+2(x, y))
*2(x, 0) -> 0
*2(x, s1(y)) -> +2(*2(x, y), x)
ge2(x, 0) -> true
ge2(0, s1(y)) -> false
ge2(s1(x), s1(y)) -> ge2(x, y)
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
fact1(x) -> iffact2(x, ge2(x, s1(s1(0))))
iffact2(x, true) -> *2(x, fact1(-2(x, s1(0))))
iffact2(x, false) -> s1(0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
*12(x, s1(y)) -> *12(x, y)
POL(*12(x1, x2)) = x2
POL(s1(x1)) = 1 + x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
+2(x, 0) -> x
+2(x, s1(y)) -> s1(+2(x, y))
*2(x, 0) -> 0
*2(x, s1(y)) -> +2(*2(x, y), x)
ge2(x, 0) -> true
ge2(0, s1(y)) -> false
ge2(s1(x), s1(y)) -> ge2(x, y)
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
fact1(x) -> iffact2(x, ge2(x, s1(s1(0))))
iffact2(x, true) -> *2(x, fact1(-2(x, s1(0))))
iffact2(x, false) -> s1(0)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
FACT1(x) -> IFFACT2(x, ge2(x, s1(s1(0))))
IFFACT2(x, true) -> FACT1(-2(x, s1(0)))
+2(x, 0) -> x
+2(x, s1(y)) -> s1(+2(x, y))
*2(x, 0) -> 0
*2(x, s1(y)) -> +2(*2(x, y), x)
ge2(x, 0) -> true
ge2(0, s1(y)) -> false
ge2(s1(x), s1(y)) -> ge2(x, y)
-2(x, 0) -> x
-2(s1(x), s1(y)) -> -2(x, y)
fact1(x) -> iffact2(x, ge2(x, s1(s1(0))))
iffact2(x, true) -> *2(x, fact1(-2(x, s1(0))))
iffact2(x, false) -> s1(0)