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 Induction-Processor (⇐)
↳34 AND
↳35 QDP
↳36 DependencyGraphProof (⇔)
↳37 TRUE
↳38 QTRS
↳39 QTRSRRRProof (⇔)
↳40 QTRS
↳41 RisEmptyProof (⇔)
↳42 TRUE
↳43 RisEmptyProof (⇔)
↳44 TRUE
↳45 RisEmptyProof (⇔)
↳46 TRUE
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
half(s(0)) → 0
half(s(s(x))) → s(half(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
half(0) → 0
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
f → g
f → h
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
half(0)
half(s(0))
half(s(s(x0)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
logarithm(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
f
HALF(s(s(x))) → HALF(x)
LE(s(x), s(y)) → LE(x, y)
INC(s(x)) → INC(x)
LOGARITHM(x) → LOGITER(x, 0)
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
LOGITER(x, y) → LE(s(0), x)
LOGITER(x, y) → LE(s(s(0)), x)
LOGITER(x, y) → HALF(x)
LOGITER(x, y) → INC(y)
IF(true, true, x, y) → LOGITER(x, y)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
half(0)
half(s(0))
half(s(s(x0)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
logarithm(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
f
INC(s(x)) → INC(x)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
half(0)
half(s(0))
half(s(s(x0)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
logarithm(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
f
INC(s(x)) → INC(x)
half(0)
half(s(0))
half(s(s(x0)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
logarithm(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
f
half(0)
half(s(0))
half(s(s(x0)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
logarithm(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
f
INC(s(x)) → INC(x)
From the DPs we obtained the following set of size-change graphs:
LE(s(x), s(y)) → LE(x, y)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
half(0)
half(s(0))
half(s(s(x0)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
logarithm(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
f
LE(s(x), s(y)) → LE(x, y)
half(0)
half(s(0))
half(s(s(x0)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
logarithm(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
f
half(0)
half(s(0))
half(s(s(x0)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
logarithm(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
f
LE(s(x), s(y)) → LE(x, y)
From the DPs we obtained the following set of size-change graphs:
HALF(s(s(x))) → HALF(x)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
half(0)
half(s(0))
half(s(s(x0)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
logarithm(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
f
HALF(s(s(x))) → HALF(x)
half(0)
half(s(0))
half(s(s(x0)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
logarithm(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
f
half(0)
half(s(0))
half(s(s(x0)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
logarithm(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
f
HALF(s(s(x))) → HALF(x)
From the DPs we obtained the following set of size-change graphs:
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
IF(true, true, x, y) → LOGITER(x, y)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
half(0)
half(s(0))
half(s(s(x0)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
logarithm(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
f
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
IF(true, true, x, y) → LOGITER(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
le(0, y) → true
half(0)
half(s(0))
half(s(s(x0)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
logarithm(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
f
logarithm(x0)
logIter(x0, x1)
if(false, x0, x1, x2)
if(true, false, x0, s(x1))
if(true, true, x0, x1)
f
LOGITER(x, y) → IF(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
IF(true, true, x, y) → LOGITER(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
le(0, y) → true
half(0)
half(s(0))
half(s(s(x0)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
POL(0) = 0
POL(IF(x1, x2, x3, x4)) = x1 + 2·x2
POL(LOGITER(x1, x2)) = 3
POL(false) = 0
POL(half(x1)) = 0
POL(inc(x1)) = 0
POL(le(x1, x2)) = 1
POL(s(x1)) = 0
POL(true) = 1
IF(true, true, x, y) → LOGITER(x, y)
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
inc(s(x)) → s(inc(x))
inc(0) → s(0)
le(0, y) → true
half(0)
half(s(0))
half(s(s(x0)))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
inc(s(x0))
inc(0)
le'(s(x), 0) → true
le'(s(x3), s(y'')) → le'(x3, y'')
le'(0, y13) → false
le(s(x), 0) → false
le(s(x3), s(y'')) → le(x3, y'')
half(0) → 0
half(s(0)) → 0
half(s(s(x16))) → s(half(x16))
inc(s(x21)) → s(inc(x21))
inc(0) → s(0)
le(0, y13) → true
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a23](witness_sort[a23], witness_sort[a23]) → true
le'2 > true
le'2 > false
le2 > true
le2 > false
half1 > s1
inc1 > s1
equalbool2 > true
not1 > true
not1 > false
isafalse1 > true
isafalse1 > false
equalsort[a0]2 > true
equalsort[a0]2 > false
equalsort[a23]2 > true
trivial
le'(s(x), 0) → true
le'(s(x3), s(y'')) → le'(x3, y'')
le'(0, y13) → false
le(s(x), 0) → false
le(s(x3), s(y'')) → le(x3, y'')
half(0) → 0
half(s(0)) → 0
half(s(s(x16))) → s(half(x16))
inc(s(x21)) → s(inc(x21))
inc(0) → s(0)
le(0, y13) → true
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a23](witness_sort[a23], witness_sort[a23]) → true