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 QTRSRRRProof (⇔)
↳42 QTRS
↳43 QTRSRRRProof (⇔)
↳44 QTRS
↳45 QTRSRRRProof (⇔)
↳46 QTRS
↳47 QTRSRRRProof (⇔)
↳48 QTRS
↳49 QTRSRRRProof (⇔)
↳50 QTRS
↳51 QTRSRRRProof (⇔)
↳52 QTRS
↳53 RisEmptyProof (⇔)
↳54 TRUE
↳55 RisEmptyProof (⇔)
↳56 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
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 1
POL(and(x1, x2)) = 1 + x1 + x2
POL(equal_bool(x1, x2)) = x1 + x2
POL(equal_sort[a0](x1, x2)) = x1 + x2
POL(equal_sort[a23](x1, x2)) = 1 + x1 + x2
POL(false) = 1
POL(half(x1)) = 1 + x1
POL(inc(x1)) = 1 + x1
POL(isa_false(x1)) = 2 + x1
POL(isa_true(x1)) = x1
POL(le(x1, x2)) = x1 + x2
POL(le'(x1, x2)) = 1 + x1 + x2
POL(not(x1)) = 2 + x1
POL(or(x1, x2)) = x1 + x2
POL(s(x1)) = x1
POL(true) = 0
POL(witness_sort[a23]) = 0
le'(s(x), 0) → true
le'(0, y13) → false
half(0) → 0
half(s(0)) → 0
inc(0) → s(0)
le(0, y13) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(false, x) → x
not(false) → true
not(true) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a23](witness_sort[a23], witness_sort[a23]) → true
le'(s(x3), s(y'')) → le'(x3, y'')
le(s(x), 0) → false
le(s(x3), s(y'')) → le(x3, y'')
half(s(s(x16))) → s(half(x16))
inc(s(x21)) → s(inc(x21))
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
or(true, x) → true
isa_true(true) → true
isa_true(false) → false
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)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(equal_bool(x1, x2)) = x1 + x2
POL(equal_sort[a0](x1, x2)) = x1 + x2
POL(false) = 0
POL(half(x1)) = x1
POL(inc(x1)) = x1
POL(isa_true(x1)) = x1
POL(le(x1, x2)) = 1 + x1 + x2
POL(le'(x1, x2)) = x1 + x2
POL(or(x1, x2)) = 1 + x1 + x2
POL(s(x1)) = x1
POL(true) = 0
le(s(x), 0) → false
or(true, x) → true
le'(s(x3), s(y'')) → le'(x3, y'')
le(s(x3), s(y'')) → le(x3, y'')
half(s(s(x16))) → s(half(x16))
inc(s(x21)) → s(inc(x21))
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
isa_true(true) → true
isa_true(false) → false
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)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(equal_bool(x1, x2)) = 1 + x1 + x2
POL(equal_sort[a0](x1, x2)) = x1 + x2
POL(false) = 0
POL(half(x1)) = x1
POL(inc(x1)) = x1
POL(isa_true(x1)) = x1
POL(le(x1, x2)) = x1 + x2
POL(le'(x1, x2)) = x1 + x2
POL(s(x1)) = x1
POL(true) = 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
le'(s(x3), s(y'')) → le'(x3, y'')
le(s(x3), s(y'')) → le(x3, y'')
half(s(s(x16))) → s(half(x16))
inc(s(x21)) → s(inc(x21))
isa_true(true) → true
isa_true(false) → false
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)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(equal_sort[a0](x1, x2)) = x1 + x2
POL(false) = 0
POL(half(x1)) = x1
POL(inc(x1)) = x1
POL(isa_true(x1)) = 1 + x1
POL(le(x1, x2)) = x1 + x2
POL(le'(x1, x2)) = x1 + x2
POL(s(x1)) = x1
POL(true) = 0
isa_true(true) → true
isa_true(false) → false
le'(s(x3), s(y'')) → le'(x3, y'')
le(s(x3), s(y'')) → le(x3, y'')
half(s(s(x16))) → s(half(x16))
inc(s(x21)) → s(inc(x21))
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)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(0) = 0
POL(equal_sort[a0](x1, x2)) = 1 + x1 + x2
POL(false) = 0
POL(half(x1)) = x1
POL(inc(x1)) = x1
POL(le(x1, x2)) = x1 + x2
POL(le'(x1, x2)) = x1 + x2
POL(s(x1)) = x1
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
le'(s(x3), s(y'')) → le'(x3, y'')
le(s(x3), s(y'')) → le(x3, y'')
half(s(s(x16))) → s(half(x16))
inc(s(x21)) → s(inc(x21))
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(equal_sort[a0](x1, x2)) = x1 + x2
POL(half(x1)) = x1
POL(inc(x1)) = x1
POL(le(x1, x2)) = x1 + x2
POL(le'(x1, x2)) = x1 + x2
POL(s(x1)) = 1 + x1
le'(s(x3), s(y'')) → le'(x3, y'')
le(s(x3), s(y'')) → le(x3, y'')
half(s(s(x16))) → s(half(x16))
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
inc(s(x21)) → s(inc(x21))
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
POL(inc(x1)) = 2 + 2·x1
POL(s(x1)) = 1 + x1
inc(s(x21)) → s(inc(x21))