a__fact(X) → a__if(a__zero(mark(X)), s(0), prod(X, fact(p(X))))
a__add(0, X) → mark(X)
a__add(s(X), Y) → s(a__add(mark(X), mark(Y)))
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(add(X1, X2)) → a__add(mark(X1), mark(X2))
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)
a__add(X1, X2) → add(X1, X2)
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__add'(0', X) → mark'(X)
a__add'(s'(X), Y) → s'(a__add'(mark'(X), mark'(Y)))
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'(add'(X1, X2)) → a__add'(mark'(X1), mark'(X2))
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)
a__add'(X1, X2) → add'(X1, X2)
Infered types.
Rules:
a__fact'(X) → a__if'(a__zero'(mark'(X)), s'(0'), prod'(X, fact'(p'(X))))
a__add'(0', X) → mark'(X)
a__add'(s'(X), Y) → s'(a__add'(mark'(X), mark'(Y)))
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'(add'(X1, X2)) → a__add'(mark'(X1), mark'(X2))
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)
a__add'(X1, X2) → add'(X1, X2)
Types:
a__fact' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__if' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__zero' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
mark' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
s' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
0' :: 0':s':p':fact':prod':true':false':if':zero':add'
prod' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
fact' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
p' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__add' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__prod' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
true' :: 0':s':p':fact':prod':true':false':if':zero':add'
false' :: 0':s':p':fact':prod':true':false':if':zero':add'
a__p' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
if' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
zero' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
add' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
_hole_0':s':p':fact':prod':true':false':if':zero':add'1 :: 0':s':p':fact':prod':true':false':if':zero':add'
_gen_0':s':p':fact':prod':true':false':if':zero':add'2 :: Nat → 0':s':p':fact':prod':true':false':if':zero':add'
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__add'
a__fact' = a__prod'
a__fact' = a__p'
a__if' = mark'
a__if' = a__add'
a__if' = a__prod'
a__if' = a__p'
mark' = a__add'
mark' = a__prod'
mark' = a__p'
a__add' = a__prod'
a__add' = a__p'
a__prod' = a__p'
Rules:
a__fact'(X) → a__if'(a__zero'(mark'(X)), s'(0'), prod'(X, fact'(p'(X))))
a__add'(0', X) → mark'(X)
a__add'(s'(X), Y) → s'(a__add'(mark'(X), mark'(Y)))
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'(add'(X1, X2)) → a__add'(mark'(X1), mark'(X2))
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)
a__add'(X1, X2) → add'(X1, X2)
Types:
a__fact' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__if' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__zero' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
mark' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
s' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
0' :: 0':s':p':fact':prod':true':false':if':zero':add'
prod' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
fact' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
p' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__add' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__prod' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
true' :: 0':s':p':fact':prod':true':false':if':zero':add'
false' :: 0':s':p':fact':prod':true':false':if':zero':add'
a__p' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
if' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
zero' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
add' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
_hole_0':s':p':fact':prod':true':false':if':zero':add'1 :: 0':s':p':fact':prod':true':false':if':zero':add'
_gen_0':s':p':fact':prod':true':false':if':zero':add'2 :: Nat → 0':s':p':fact':prod':true':false':if':zero':add'
Generator Equations:
_gen_0':s':p':fact':prod':true':false':if':zero':add'2(0) ⇔ 0'
_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(x, 1)) ⇔ s'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(x))
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__add'
a__fact' = a__prod'
a__fact' = a__p'
a__if' = mark'
a__if' = a__add'
a__if' = a__prod'
a__if' = a__p'
mark' = a__add'
mark' = a__prod'
mark' = a__p'
a__add' = a__prod'
a__add' = 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__add'(0', X) → mark'(X)
a__add'(s'(X), Y) → s'(a__add'(mark'(X), mark'(Y)))
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'(add'(X1, X2)) → a__add'(mark'(X1), mark'(X2))
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)
a__add'(X1, X2) → add'(X1, X2)
Types:
a__fact' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__if' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__zero' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
mark' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
s' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
0' :: 0':s':p':fact':prod':true':false':if':zero':add'
prod' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
fact' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
p' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__add' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__prod' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
true' :: 0':s':p':fact':prod':true':false':if':zero':add'
false' :: 0':s':p':fact':prod':true':false':if':zero':add'
a__p' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
if' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
zero' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
add' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
_hole_0':s':p':fact':prod':true':false':if':zero':add'1 :: 0':s':p':fact':prod':true':false':if':zero':add'
_gen_0':s':p':fact':prod':true':false':if':zero':add'2 :: Nat → 0':s':p':fact':prod':true':false':if':zero':add'
Generator Equations:
_gen_0':s':p':fact':prod':true':false':if':zero':add'2(0) ⇔ 0'
_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(x, 1)) ⇔ s'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(x))
The following defined symbols remain to be analysed:
mark', a__fact', 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__add'
a__fact' = a__prod'
a__fact' = a__p'
a__if' = mark'
a__if' = a__add'
a__if' = a__prod'
a__if' = a__p'
mark' = a__add'
mark' = a__prod'
mark' = a__p'
a__add' = a__prod'
a__add' = a__p'
a__prod' = a__p'
Proved the following rewrite lemma:
mark'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_n46)) → _gen_0':s':p':fact':prod':true':false':if':zero':add'2(_n46), rt ∈ Ω(1 + n46)
Induction Base:
mark'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(0)) →RΩ(1)
0'
Induction Step:
mark'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(_$n47, 1))) →RΩ(1)
s'(mark'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n47))) →IH
s'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n47))
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__add'(0', X) → mark'(X)
a__add'(s'(X), Y) → s'(a__add'(mark'(X), mark'(Y)))
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'(add'(X1, X2)) → a__add'(mark'(X1), mark'(X2))
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)
a__add'(X1, X2) → add'(X1, X2)
Types:
a__fact' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__if' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__zero' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
mark' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
s' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
0' :: 0':s':p':fact':prod':true':false':if':zero':add'
prod' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
fact' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
p' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__add' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
a__prod' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
true' :: 0':s':p':fact':prod':true':false':if':zero':add'
false' :: 0':s':p':fact':prod':true':false':if':zero':add'
a__p' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
if' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
zero' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
add' :: 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add' → 0':s':p':fact':prod':true':false':if':zero':add'
_hole_0':s':p':fact':prod':true':false':if':zero':add'1 :: 0':s':p':fact':prod':true':false':if':zero':add'
_gen_0':s':p':fact':prod':true':false':if':zero':add'2 :: Nat → 0':s':p':fact':prod':true':false':if':zero':add'
Lemmas:
mark'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_n46)) → _gen_0':s':p':fact':prod':true':false':if':zero':add'2(_n46), rt ∈ Ω(1 + n46)
Generator Equations:
_gen_0':s':p':fact':prod':true':false':if':zero':add'2(0) ⇔ 0'
_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(x, 1)) ⇔ s'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(x))
The following defined symbols remain to be analysed:
a__fact', a__if', 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__add'
a__fact' = a__prod'
a__fact' = a__p'
a__if' = mark'
a__if' = a__add'
a__if' = a__prod'
a__if' = a__p'
mark' = a__add'
mark' = a__prod'
mark' = a__p'
a__add' = a__prod'
a__add' = 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:
a__fact'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(0))
Induction Step:
a__fact'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(_$n3032, 1))) →RΩ(1)
a__if'(a__zero'(mark'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(_$n3032, 1)))), s'(0'), prod'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(_$n3032, 1)), fact'(p'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(_$n3032, 1)))))) →LΩ(2 + $n3032)
a__if'(a__zero'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032))), s'(0'), prod'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)), fact'(p'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)))))) →RΩ(1)
a__if'(false', s'(0'), prod'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)), fact'(p'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)))))) →RΩ(1)
mark'(prod'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)), fact'(p'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)))))) →RΩ(1)
a__prod'(mark'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032))), mark'(fact'(p'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)))))) →LΩ(2 + $n3032)
a__prod'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)), mark'(fact'(p'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)))))) →RΩ(1)
a__prod'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)), a__fact'(mark'(p'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)))))) →RΩ(1)
a__prod'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)), a__fact'(a__p'(mark'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)))))) →LΩ(2 + $n3032)
a__prod'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)), a__fact'(a__p'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032))))) →RΩ(1)
a__prod'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)), a__fact'(mark'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032)))) →LΩ(1 + $n3032)
a__prod'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)), a__fact'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032))) →RΩ(1)
a__prod'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(+(1, _$n3032)), fact'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032))) →RΩ(1)
a__add'(mark'(fact'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032))), a__prod'(mark'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032)), mark'(fact'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032))))) →RΩ(1)
a__add'(a__fact'(mark'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032))), a__prod'(mark'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032)), mark'(fact'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032))))) →LΩ(1 + $n3032)
a__add'(a__fact'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032)), a__prod'(mark'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032)), mark'(fact'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032))))) →IH
a__add'(_*3, a__prod'(mark'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032)), mark'(fact'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032))))) →LΩ(1 + $n3032)
a__add'(_*3, a__prod'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032), mark'(fact'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032))))) →RΩ(1)
a__add'(_*3, a__prod'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032), a__fact'(mark'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032))))) →LΩ(1 + $n3032)
a__add'(_*3, a__prod'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032), a__fact'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032)))) →IH
a__add'(_*3, a__prod'(_gen_0':s':p':fact':prod':true':false':if':zero':add'2(_$n3032), _*3))
We have rt ∈ Ω(2n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(2n)