(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
active(minus(0, Y)) → mark(0)
active(minus(s(X), s(Y))) → mark(minus(X, Y))
active(geq(X, 0)) → mark(true)
active(geq(0, s(Y))) → mark(false)
active(geq(s(X), s(Y))) → mark(geq(X, Y))
active(div(0, s(Y))) → mark(0)
active(div(s(X), s(Y))) → mark(if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(minus(X1, X2)) → active(minus(X1, X2))
mark(0) → active(0)
mark(s(X)) → active(s(mark(X)))
mark(geq(X1, X2)) → active(geq(X1, X2))
mark(true) → active(true)
mark(false) → active(false)
mark(div(X1, X2)) → active(div(mark(X1), X2))
mark(if(X1, X2, X3)) → active(if(mark(X1), X2, X3))
minus(mark(X1), X2) → minus(X1, X2)
minus(X1, mark(X2)) → minus(X1, X2)
minus(active(X1), X2) → minus(X1, X2)
minus(X1, active(X2)) → minus(X1, X2)
s(mark(X)) → s(X)
s(active(X)) → s(X)
geq(mark(X1), X2) → geq(X1, X2)
geq(X1, mark(X2)) → geq(X1, X2)
geq(active(X1), X2) → geq(X1, X2)
geq(X1, active(X2)) → geq(X1, X2)
div(mark(X1), X2) → div(X1, X2)
div(X1, mark(X2)) → div(X1, X2)
div(active(X1), X2) → div(X1, X2)
div(X1, active(X2)) → div(X1, X2)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(minus(0, z0)) → mark(0)
active(minus(s(z0), s(z1))) → mark(minus(z0, z1))
active(geq(z0, 0)) → mark(true)
active(geq(0, s(z0))) → mark(false)
active(geq(s(z0), s(z1))) → mark(geq(z0, z1))
active(div(0, s(z0))) → mark(0)
active(div(s(z0), s(z1))) → mark(if(geq(z0, z1), s(div(minus(z0, z1), s(z1))), 0))
active(if(true, z0, z1)) → mark(z0)
active(if(false, z0, z1)) → mark(z1)
mark(minus(z0, z1)) → active(minus(z0, z1))
mark(0) → active(0)
mark(s(z0)) → active(s(mark(z0)))
mark(geq(z0, z1)) → active(geq(z0, z1))
mark(true) → active(true)
mark(false) → active(false)
mark(div(z0, z1)) → active(div(mark(z0), z1))
mark(if(z0, z1, z2)) → active(if(mark(z0), z1, z2))
minus(mark(z0), z1) → minus(z0, z1)
minus(z0, mark(z1)) → minus(z0, z1)
minus(active(z0), z1) → minus(z0, z1)
minus(z0, active(z1)) → minus(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
geq(mark(z0), z1) → geq(z0, z1)
geq(z0, mark(z1)) → geq(z0, z1)
geq(active(z0), z1) → geq(z0, z1)
geq(z0, active(z1)) → geq(z0, z1)
div(mark(z0), z1) → div(z0, z1)
div(z0, mark(z1)) → div(z0, z1)
div(active(z0), z1) → div(z0, z1)
div(z0, active(z1)) → div(z0, z1)
if(mark(z0), z1, z2) → if(z0, z1, z2)
if(z0, mark(z1), z2) → if(z0, z1, z2)
if(z0, z1, mark(z2)) → if(z0, z1, z2)
if(active(z0), z1, z2) → if(z0, z1, z2)
if(z0, active(z1), z2) → if(z0, z1, z2)
if(z0, z1, active(z2)) → if(z0, z1, z2)
Tuples:
ACTIVE(minus(0, z0)) → c(MARK(0))
ACTIVE(minus(s(z0), s(z1))) → c1(MARK(minus(z0, z1)), MINUS(z0, z1))
ACTIVE(geq(z0, 0)) → c2(MARK(true))
ACTIVE(geq(0, s(z0))) → c3(MARK(false))
ACTIVE(geq(s(z0), s(z1))) → c4(MARK(geq(z0, z1)), GEQ(z0, z1))
ACTIVE(div(0, s(z0))) → c5(MARK(0))
ACTIVE(div(s(z0), s(z1))) → c6(MARK(if(geq(z0, z1), s(div(minus(z0, z1), s(z1))), 0)), IF(geq(z0, z1), s(div(minus(z0, z1), s(z1))), 0), GEQ(z0, z1), S(div(minus(z0, z1), s(z1))), DIV(minus(z0, z1), s(z1)), MINUS(z0, z1), S(z1))
ACTIVE(if(true, z0, z1)) → c7(MARK(z0))
ACTIVE(if(false, z0, z1)) → c8(MARK(z1))
MARK(minus(z0, z1)) → c9(ACTIVE(minus(z0, z1)), MINUS(z0, z1))
MARK(0) → c10(ACTIVE(0))
MARK(s(z0)) → c11(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(geq(z0, z1)) → c12(ACTIVE(geq(z0, z1)), GEQ(z0, z1))
MARK(true) → c13(ACTIVE(true))
MARK(false) → c14(ACTIVE(false))
MARK(div(z0, z1)) → c15(ACTIVE(div(mark(z0), z1)), DIV(mark(z0), z1), MARK(z0))
MARK(if(z0, z1, z2)) → c16(ACTIVE(if(mark(z0), z1, z2)), IF(mark(z0), z1, z2), MARK(z0))
MINUS(mark(z0), z1) → c17(MINUS(z0, z1))
MINUS(z0, mark(z1)) → c18(MINUS(z0, z1))
MINUS(active(z0), z1) → c19(MINUS(z0, z1))
MINUS(z0, active(z1)) → c20(MINUS(z0, z1))
S(mark(z0)) → c21(S(z0))
S(active(z0)) → c22(S(z0))
GEQ(mark(z0), z1) → c23(GEQ(z0, z1))
GEQ(z0, mark(z1)) → c24(GEQ(z0, z1))
GEQ(active(z0), z1) → c25(GEQ(z0, z1))
GEQ(z0, active(z1)) → c26(GEQ(z0, z1))
DIV(mark(z0), z1) → c27(DIV(z0, z1))
DIV(z0, mark(z1)) → c28(DIV(z0, z1))
DIV(active(z0), z1) → c29(DIV(z0, z1))
DIV(z0, active(z1)) → c30(DIV(z0, z1))
IF(mark(z0), z1, z2) → c31(IF(z0, z1, z2))
IF(z0, mark(z1), z2) → c32(IF(z0, z1, z2))
IF(z0, z1, mark(z2)) → c33(IF(z0, z1, z2))
IF(active(z0), z1, z2) → c34(IF(z0, z1, z2))
IF(z0, active(z1), z2) → c35(IF(z0, z1, z2))
IF(z0, z1, active(z2)) → c36(IF(z0, z1, z2))
S tuples:
ACTIVE(minus(0, z0)) → c(MARK(0))
ACTIVE(minus(s(z0), s(z1))) → c1(MARK(minus(z0, z1)), MINUS(z0, z1))
ACTIVE(geq(z0, 0)) → c2(MARK(true))
ACTIVE(geq(0, s(z0))) → c3(MARK(false))
ACTIVE(geq(s(z0), s(z1))) → c4(MARK(geq(z0, z1)), GEQ(z0, z1))
ACTIVE(div(0, s(z0))) → c5(MARK(0))
ACTIVE(div(s(z0), s(z1))) → c6(MARK(if(geq(z0, z1), s(div(minus(z0, z1), s(z1))), 0)), IF(geq(z0, z1), s(div(minus(z0, z1), s(z1))), 0), GEQ(z0, z1), S(div(minus(z0, z1), s(z1))), DIV(minus(z0, z1), s(z1)), MINUS(z0, z1), S(z1))
ACTIVE(if(true, z0, z1)) → c7(MARK(z0))
ACTIVE(if(false, z0, z1)) → c8(MARK(z1))
MARK(minus(z0, z1)) → c9(ACTIVE(minus(z0, z1)), MINUS(z0, z1))
MARK(0) → c10(ACTIVE(0))
MARK(s(z0)) → c11(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(geq(z0, z1)) → c12(ACTIVE(geq(z0, z1)), GEQ(z0, z1))
MARK(true) → c13(ACTIVE(true))
MARK(false) → c14(ACTIVE(false))
MARK(div(z0, z1)) → c15(ACTIVE(div(mark(z0), z1)), DIV(mark(z0), z1), MARK(z0))
MARK(if(z0, z1, z2)) → c16(ACTIVE(if(mark(z0), z1, z2)), IF(mark(z0), z1, z2), MARK(z0))
MINUS(mark(z0), z1) → c17(MINUS(z0, z1))
MINUS(z0, mark(z1)) → c18(MINUS(z0, z1))
MINUS(active(z0), z1) → c19(MINUS(z0, z1))
MINUS(z0, active(z1)) → c20(MINUS(z0, z1))
S(mark(z0)) → c21(S(z0))
S(active(z0)) → c22(S(z0))
GEQ(mark(z0), z1) → c23(GEQ(z0, z1))
GEQ(z0, mark(z1)) → c24(GEQ(z0, z1))
GEQ(active(z0), z1) → c25(GEQ(z0, z1))
GEQ(z0, active(z1)) → c26(GEQ(z0, z1))
DIV(mark(z0), z1) → c27(DIV(z0, z1))
DIV(z0, mark(z1)) → c28(DIV(z0, z1))
DIV(active(z0), z1) → c29(DIV(z0, z1))
DIV(z0, active(z1)) → c30(DIV(z0, z1))
IF(mark(z0), z1, z2) → c31(IF(z0, z1, z2))
IF(z0, mark(z1), z2) → c32(IF(z0, z1, z2))
IF(z0, z1, mark(z2)) → c33(IF(z0, z1, z2))
IF(active(z0), z1, z2) → c34(IF(z0, z1, z2))
IF(z0, active(z1), z2) → c35(IF(z0, z1, z2))
IF(z0, z1, active(z2)) → c36(IF(z0, z1, z2))
K tuples:none
Defined Rule Symbols:
active, mark, minus, s, geq, div, if
Defined Pair Symbols:
ACTIVE, MARK, MINUS, S, GEQ, DIV, IF
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
ACTIVE(minus(0, z0)) → c(MARK(0))
ACTIVE(minus(s(z0), s(z1))) → c1(MARK(minus(z0, z1)), MINUS(z0, z1))
ACTIVE(geq(z0, 0)) → c2(MARK(true))
ACTIVE(geq(0, s(z0))) → c3(MARK(false))
ACTIVE(geq(s(z0), s(z1))) → c4(MARK(geq(z0, z1)), GEQ(z0, z1))
ACTIVE(div(0, s(z0))) → c5(MARK(0))
ACTIVE(div(s(z0), s(z1))) → c6(MARK(if(geq(z0, z1), s(div(minus(z0, z1), s(z1))), 0)), IF(geq(z0, z1), s(div(minus(z0, z1), s(z1))), 0), GEQ(z0, z1), S(div(minus(z0, z1), s(z1))), DIV(minus(z0, z1), s(z1)), MINUS(z0, z1), S(z1))
ACTIVE(if(true, z0, z1)) → c7(MARK(z0))
ACTIVE(if(false, z0, z1)) → c8(MARK(z1))
MARK(minus(z0, z1)) → c9(ACTIVE(minus(z0, z1)), MINUS(z0, z1))
MARK(s(z0)) → c11(ACTIVE(s(mark(z0))), S(mark(z0)), MARK(z0))
MARK(geq(z0, z1)) → c12(ACTIVE(geq(z0, z1)), GEQ(z0, z1))
MARK(div(z0, z1)) → c15(ACTIVE(div(mark(z0), z1)), DIV(mark(z0), z1), MARK(z0))
MARK(if(z0, z1, z2)) → c16(ACTIVE(if(mark(z0), z1, z2)), IF(mark(z0), z1, z2), MARK(z0))
MINUS(mark(z0), z1) → c17(MINUS(z0, z1))
MINUS(z0, mark(z1)) → c18(MINUS(z0, z1))
MINUS(active(z0), z1) → c19(MINUS(z0, z1))
MINUS(z0, active(z1)) → c20(MINUS(z0, z1))
S(mark(z0)) → c21(S(z0))
S(active(z0)) → c22(S(z0))
GEQ(mark(z0), z1) → c23(GEQ(z0, z1))
GEQ(z0, mark(z1)) → c24(GEQ(z0, z1))
GEQ(active(z0), z1) → c25(GEQ(z0, z1))
GEQ(z0, active(z1)) → c26(GEQ(z0, z1))
DIV(mark(z0), z1) → c27(DIV(z0, z1))
DIV(z0, mark(z1)) → c28(DIV(z0, z1))
DIV(active(z0), z1) → c29(DIV(z0, z1))
DIV(z0, active(z1)) → c30(DIV(z0, z1))
IF(mark(z0), z1, z2) → c31(IF(z0, z1, z2))
IF(z0, mark(z1), z2) → c32(IF(z0, z1, z2))
IF(z0, z1, mark(z2)) → c33(IF(z0, z1, z2))
IF(active(z0), z1, z2) → c34(IF(z0, z1, z2))
IF(z0, active(z1), z2) → c35(IF(z0, z1, z2))
IF(z0, z1, active(z2)) → c36(IF(z0, z1, z2))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(minus(0, z0)) → mark(0)
active(minus(s(z0), s(z1))) → mark(minus(z0, z1))
active(geq(z0, 0)) → mark(true)
active(geq(0, s(z0))) → mark(false)
active(geq(s(z0), s(z1))) → mark(geq(z0, z1))
active(div(0, s(z0))) → mark(0)
active(div(s(z0), s(z1))) → mark(if(geq(z0, z1), s(div(minus(z0, z1), s(z1))), 0))
active(if(true, z0, z1)) → mark(z0)
active(if(false, z0, z1)) → mark(z1)
mark(minus(z0, z1)) → active(minus(z0, z1))
mark(0) → active(0)
mark(s(z0)) → active(s(mark(z0)))
mark(geq(z0, z1)) → active(geq(z0, z1))
mark(true) → active(true)
mark(false) → active(false)
mark(div(z0, z1)) → active(div(mark(z0), z1))
mark(if(z0, z1, z2)) → active(if(mark(z0), z1, z2))
minus(mark(z0), z1) → minus(z0, z1)
minus(z0, mark(z1)) → minus(z0, z1)
minus(active(z0), z1) → minus(z0, z1)
minus(z0, active(z1)) → minus(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
geq(mark(z0), z1) → geq(z0, z1)
geq(z0, mark(z1)) → geq(z0, z1)
geq(active(z0), z1) → geq(z0, z1)
geq(z0, active(z1)) → geq(z0, z1)
div(mark(z0), z1) → div(z0, z1)
div(z0, mark(z1)) → div(z0, z1)
div(active(z0), z1) → div(z0, z1)
div(z0, active(z1)) → div(z0, z1)
if(mark(z0), z1, z2) → if(z0, z1, z2)
if(z0, mark(z1), z2) → if(z0, z1, z2)
if(z0, z1, mark(z2)) → if(z0, z1, z2)
if(active(z0), z1, z2) → if(z0, z1, z2)
if(z0, active(z1), z2) → if(z0, z1, z2)
if(z0, z1, active(z2)) → if(z0, z1, z2)
Tuples:
MARK(0) → c10(ACTIVE(0))
MARK(true) → c13(ACTIVE(true))
MARK(false) → c14(ACTIVE(false))
S tuples:
MARK(0) → c10(ACTIVE(0))
MARK(true) → c13(ACTIVE(true))
MARK(false) → c14(ACTIVE(false))
K tuples:none
Defined Rule Symbols:
active, mark, minus, s, geq, div, if
Defined Pair Symbols:
MARK
Compound Symbols:
c10, c13, c14
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing nodes:
MARK(false) → c14(ACTIVE(false))
MARK(true) → c13(ACTIVE(true))
MARK(0) → c10(ACTIVE(0))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(minus(0, z0)) → mark(0)
active(minus(s(z0), s(z1))) → mark(minus(z0, z1))
active(geq(z0, 0)) → mark(true)
active(geq(0, s(z0))) → mark(false)
active(geq(s(z0), s(z1))) → mark(geq(z0, z1))
active(div(0, s(z0))) → mark(0)
active(div(s(z0), s(z1))) → mark(if(geq(z0, z1), s(div(minus(z0, z1), s(z1))), 0))
active(if(true, z0, z1)) → mark(z0)
active(if(false, z0, z1)) → mark(z1)
mark(minus(z0, z1)) → active(minus(z0, z1))
mark(0) → active(0)
mark(s(z0)) → active(s(mark(z0)))
mark(geq(z0, z1)) → active(geq(z0, z1))
mark(true) → active(true)
mark(false) → active(false)
mark(div(z0, z1)) → active(div(mark(z0), z1))
mark(if(z0, z1, z2)) → active(if(mark(z0), z1, z2))
minus(mark(z0), z1) → minus(z0, z1)
minus(z0, mark(z1)) → minus(z0, z1)
minus(active(z0), z1) → minus(z0, z1)
minus(z0, active(z1)) → minus(z0, z1)
s(mark(z0)) → s(z0)
s(active(z0)) → s(z0)
geq(mark(z0), z1) → geq(z0, z1)
geq(z0, mark(z1)) → geq(z0, z1)
geq(active(z0), z1) → geq(z0, z1)
geq(z0, active(z1)) → geq(z0, z1)
div(mark(z0), z1) → div(z0, z1)
div(z0, mark(z1)) → div(z0, z1)
div(active(z0), z1) → div(z0, z1)
div(z0, active(z1)) → div(z0, z1)
if(mark(z0), z1, z2) → if(z0, z1, z2)
if(z0, mark(z1), z2) → if(z0, z1, z2)
if(z0, z1, mark(z2)) → if(z0, z1, z2)
if(active(z0), z1, z2) → if(z0, z1, z2)
if(z0, active(z1), z2) → if(z0, z1, z2)
if(z0, z1, active(z2)) → if(z0, z1, z2)
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
active, mark, minus, s, geq, div, if
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))