Runtime Complexity TRS:
The TRS R consists of the following rules:

a__fact(X) → a__if(a__zero(mark(X)), s(0), prod(X, fact(p(X))))
a__prod(0, X) → 0
a__prod(s(X), Y) → a__add(mark(Y), a__prod(mark(X), mark(Y)))
a__if(true, X, Y) → mark(X)
a__if(false, X, Y) → mark(Y)
a__zero(0) → true
a__zero(s(X)) → false
a__p(s(X)) → mark(X)
mark(fact(X)) → a__fact(mark(X))
mark(if(X1, X2, X3)) → a__if(mark(X1), X2, X3)
mark(zero(X)) → a__zero(mark(X))
mark(prod(X1, X2)) → a__prod(mark(X1), mark(X2))
mark(p(X)) → a__p(mark(X))
mark(s(X)) → s(mark(X))
mark(0) → 0
mark(true) → true
mark(false) → false
a__fact(X) → fact(X)
a__if(X1, X2, X3) → if(X1, X2, X3)
a__zero(X) → zero(X)
a__prod(X1, X2) → prod(X1, X2)
a__p(X) → p(X)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:

a__fact'(X) → a__if'(a__zero'(mark'(X)), s'(0'), prod'(X, fact'(p'(X))))
a__prod'(0', X) → 0'
a__prod'(s'(X), Y) → a__add'(mark'(Y), a__prod'(mark'(X), mark'(Y)))
a__if'(true', X, Y) → mark'(X)
a__if'(false', X, Y) → mark'(Y)
a__zero'(0') → true'
a__zero'(s'(X)) → false'
a__p'(s'(X)) → mark'(X)
mark'(fact'(X)) → a__fact'(mark'(X))
mark'(if'(X1, X2, X3)) → a__if'(mark'(X1), X2, X3)
mark'(zero'(X)) → a__zero'(mark'(X))
mark'(prod'(X1, X2)) → a__prod'(mark'(X1), mark'(X2))
mark'(p'(X)) → a__p'(mark'(X))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(true') → true'
mark'(false') → false'
a__fact'(X) → fact'(X)
a__if'(X1, X2, X3) → if'(X1, X2, X3)
a__zero'(X) → zero'(X)
a__prod'(X1, X2) → prod'(X1, X2)
a__p'(X) → p'(X)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a__fact'(X) → a__if'(a__zero'(mark'(X)), s'(0'), prod'(X, fact'(p'(X))))
a__prod'(0', X) → 0'
a__prod'(s'(X), Y) → a__add'(mark'(Y), a__prod'(mark'(X), mark'(Y)))
a__if'(true', X, Y) → mark'(X)
a__if'(false', X, Y) → mark'(Y)
a__zero'(0') → true'
a__zero'(s'(X)) → false'
a__p'(s'(X)) → mark'(X)
mark'(fact'(X)) → a__fact'(mark'(X))
mark'(if'(X1, X2, X3)) → a__if'(mark'(X1), X2, X3)
mark'(zero'(X)) → a__zero'(mark'(X))
mark'(prod'(X1, X2)) → a__prod'(mark'(X1), mark'(X2))
mark'(p'(X)) → a__p'(mark'(X))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(true') → true'
mark'(false') → false'
a__fact'(X) → fact'(X)
a__if'(X1, X2, X3) → if'(X1, X2, X3)
a__zero'(X) → zero'(X)
a__prod'(X1, X2) → prod'(X1, X2)
a__p'(X) → p'(X)

Types:

Heuristically decided to analyse the following defined symbols:
a__fact', a__if', mark', a__add', a__prod', a__p'

They will be analysed ascendingly in the following order:
a__fact' = a__if'
a__fact' = mark'
a__fact' = a__prod'
a__fact' = a__p'
a__if' = mark'
a__if' = a__prod'
a__if' = a__p'
mark' = a__prod'
mark' = a__p'
a__prod' = a__p'

Rules:
a__fact'(X) → a__if'(a__zero'(mark'(X)), s'(0'), prod'(X, fact'(p'(X))))
a__prod'(0', X) → 0'
a__prod'(s'(X), Y) → a__add'(mark'(Y), a__prod'(mark'(X), mark'(Y)))
a__if'(true', X, Y) → mark'(X)
a__if'(false', X, Y) → mark'(Y)
a__zero'(0') → true'
a__zero'(s'(X)) → false'
a__p'(s'(X)) → mark'(X)
mark'(fact'(X)) → a__fact'(mark'(X))
mark'(if'(X1, X2, X3)) → a__if'(mark'(X1), X2, X3)
mark'(zero'(X)) → a__zero'(mark'(X))
mark'(prod'(X1, X2)) → a__prod'(mark'(X1), mark'(X2))
mark'(p'(X)) → a__p'(mark'(X))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(true') → true'
mark'(false') → false'
a__fact'(X) → fact'(X)
a__if'(X1, X2, X3) → if'(X1, X2, X3)
a__zero'(X) → zero'(X)
a__prod'(X1, X2) → prod'(X1, X2)
a__p'(X) → p'(X)

Types:

Generator Equations:

The following defined symbols remain to be analysed:
a__if', a__fact', mark', a__add', a__prod', a__p'

They will be analysed ascendingly in the following order:
a__fact' = a__if'
a__fact' = mark'
a__fact' = a__prod'
a__fact' = a__p'
a__if' = mark'
a__if' = a__prod'
a__if' = a__p'
mark' = a__prod'
mark' = a__p'
a__prod' = a__p'

Could not prove a rewrite lemma for the defined symbol a__if'.

Rules:
a__fact'(X) → a__if'(a__zero'(mark'(X)), s'(0'), prod'(X, fact'(p'(X))))
a__prod'(0', X) → 0'
a__prod'(s'(X), Y) → a__add'(mark'(Y), a__prod'(mark'(X), mark'(Y)))
a__if'(true', X, Y) → mark'(X)
a__if'(false', X, Y) → mark'(Y)
a__zero'(0') → true'
a__zero'(s'(X)) → false'
a__p'(s'(X)) → mark'(X)
mark'(fact'(X)) → a__fact'(mark'(X))
mark'(if'(X1, X2, X3)) → a__if'(mark'(X1), X2, X3)
mark'(zero'(X)) → a__zero'(mark'(X))
mark'(prod'(X1, X2)) → a__prod'(mark'(X1), mark'(X2))
mark'(p'(X)) → a__p'(mark'(X))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(true') → true'
mark'(false') → false'
a__fact'(X) → fact'(X)
a__if'(X1, X2, X3) → if'(X1, X2, X3)
a__zero'(X) → zero'(X)
a__prod'(X1, X2) → prod'(X1, X2)
a__p'(X) → p'(X)

Types:

Generator Equations:

The following defined symbols remain to be analysed:

They will be analysed ascendingly in the following order:
a__fact' = a__if'
a__fact' = mark'
a__fact' = a__prod'
a__fact' = a__p'
a__if' = mark'
a__if' = a__prod'
a__if' = a__p'
mark' = a__prod'
mark' = a__p'
a__prod' = a__p'

Proved the following rewrite lemma:

Induction Base:
0'

Induction Step:

We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).

Rules:
a__fact'(X) → a__if'(a__zero'(mark'(X)), s'(0'), prod'(X, fact'(p'(X))))
a__prod'(0', X) → 0'
a__prod'(s'(X), Y) → a__add'(mark'(Y), a__prod'(mark'(X), mark'(Y)))
a__if'(true', X, Y) → mark'(X)
a__if'(false', X, Y) → mark'(Y)
a__zero'(0') → true'
a__zero'(s'(X)) → false'
a__p'(s'(X)) → mark'(X)
mark'(fact'(X)) → a__fact'(mark'(X))
mark'(if'(X1, X2, X3)) → a__if'(mark'(X1), X2, X3)
mark'(zero'(X)) → a__zero'(mark'(X))
mark'(prod'(X1, X2)) → a__prod'(mark'(X1), mark'(X2))
mark'(p'(X)) → a__p'(mark'(X))
mark'(s'(X)) → s'(mark'(X))
mark'(0') → 0'
mark'(true') → true'
mark'(false') → false'
a__fact'(X) → fact'(X)
a__if'(X1, X2, X3) → if'(X1, X2, X3)
a__zero'(X) → zero'(X)
a__prod'(X1, X2) → prod'(X1, X2)
a__p'(X) → p'(X)

Types:

Lemmas:

Generator Equations:

The following defined symbols remain to be analysed:

They will be analysed ascendingly in the following order:
a__fact' = a__if'
a__fact' = mark'
a__fact' = a__prod'
a__fact' = a__p'
a__if' = mark'
a__if' = a__prod'
a__if' = a__p'
mark' = a__prod'
mark' = a__p'
a__prod' = a__p'

Proved the following rewrite lemma:
a__fact'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_n3031)) → _*3, rt ∈ Ω(2n)

Induction Base:

Induction Step: