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