f(g(X), Y) → f(X, n__f(n__g(X), activate(Y)))
f(X1, X2) → n__f(X1, X2)
g(X) → n__g(X)
activate(n__f(X1, X2)) → f(activate(X1), X2)
activate(n__g(X)) → g(activate(X))
activate(X) → X
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
f'(g'(X), Y) → f'(X, n__f'(n__g'(X), activate'(Y)))
f'(X1, X2) → n__f'(X1, X2)
g'(X) → n__g'(X)
activate'(n__f'(X1, X2)) → f'(activate'(X1), X2)
activate'(n__g'(X)) → g'(activate'(X))
activate'(X) → X
Infered types.
Rules:
f'(g'(X), Y) → f'(X, n__f'(n__g'(X), activate'(Y)))
f'(X1, X2) → n__f'(X1, X2)
g'(X) → n__g'(X)
activate'(n__f'(X1, X2)) → f'(activate'(X1), X2)
activate'(n__g'(X)) → g'(activate'(X))
activate'(X) → X
Types:
f' :: n__g':n__f' → n__g':n__f' → n__g':n__f'
g' :: n__g':n__f' → n__g':n__f'
n__f' :: n__g':n__f' → n__g':n__f' → n__g':n__f'
n__g' :: n__g':n__f' → n__g':n__f'
activate' :: n__g':n__f' → n__g':n__f'
_hole_n__g':n__f'1 :: n__g':n__f'
_gen_n__g':n__f'2 :: Nat → n__g':n__f'
Heuristically decided to analyse the following defined symbols:
f', activate'
They will be analysed ascendingly in the following order:
f' = activate'
Rules:
f'(g'(X), Y) → f'(X, n__f'(n__g'(X), activate'(Y)))
f'(X1, X2) → n__f'(X1, X2)
g'(X) → n__g'(X)
activate'(n__f'(X1, X2)) → f'(activate'(X1), X2)
activate'(n__g'(X)) → g'(activate'(X))
activate'(X) → X
Types:
f' :: n__g':n__f' → n__g':n__f' → n__g':n__f'
g' :: n__g':n__f' → n__g':n__f'
n__f' :: n__g':n__f' → n__g':n__f' → n__g':n__f'
n__g' :: n__g':n__f' → n__g':n__f'
activate' :: n__g':n__f' → n__g':n__f'
_hole_n__g':n__f'1 :: n__g':n__f'
_gen_n__g':n__f'2 :: Nat → n__g':n__f'
Generator Equations:
_gen_n__g':n__f'2(0) ⇔ _hole_n__g':n__f'1
_gen_n__g':n__f'2(+(x, 1)) ⇔ n__f'(_gen_n__g':n__f'2(x), _hole_n__g':n__f'1)
The following defined symbols remain to be analysed:
activate', f'
They will be analysed ascendingly in the following order:
f' = activate'
Proved the following rewrite lemma:
activate'(_gen_n__g':n__f'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Induction Base:
activate'(_gen_n__g':n__f'2(+(1, 0)))
Induction Step:
activate'(_gen_n__g':n__f'2(+(1, +(_$n5, 1)))) →RΩ(1)
f'(activate'(_gen_n__g':n__f'2(+(1, _$n5))), _hole_n__g':n__f'1) →IH
f'(_*3, _hole_n__g':n__f'1)
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
f'(g'(X), Y) → f'(X, n__f'(n__g'(X), activate'(Y)))
f'(X1, X2) → n__f'(X1, X2)
g'(X) → n__g'(X)
activate'(n__f'(X1, X2)) → f'(activate'(X1), X2)
activate'(n__g'(X)) → g'(activate'(X))
activate'(X) → X
Types:
f' :: n__g':n__f' → n__g':n__f' → n__g':n__f'
g' :: n__g':n__f' → n__g':n__f'
n__f' :: n__g':n__f' → n__g':n__f' → n__g':n__f'
n__g' :: n__g':n__f' → n__g':n__f'
activate' :: n__g':n__f' → n__g':n__f'
_hole_n__g':n__f'1 :: n__g':n__f'
_gen_n__g':n__f'2 :: Nat → n__g':n__f'
Lemmas:
activate'(_gen_n__g':n__f'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Generator Equations:
_gen_n__g':n__f'2(0) ⇔ _hole_n__g':n__f'1
_gen_n__g':n__f'2(+(x, 1)) ⇔ n__f'(_gen_n__g':n__f'2(x), _hole_n__g':n__f'1)
The following defined symbols remain to be analysed:
f'
They will be analysed ascendingly in the following order:
f' = activate'
Could not prove a rewrite lemma for the defined symbol f'.
Rules:
f'(g'(X), Y) → f'(X, n__f'(n__g'(X), activate'(Y)))
f'(X1, X2) → n__f'(X1, X2)
g'(X) → n__g'(X)
activate'(n__f'(X1, X2)) → f'(activate'(X1), X2)
activate'(n__g'(X)) → g'(activate'(X))
activate'(X) → X
Types:
f' :: n__g':n__f' → n__g':n__f' → n__g':n__f'
g' :: n__g':n__f' → n__g':n__f'
n__f' :: n__g':n__f' → n__g':n__f' → n__g':n__f'
n__g' :: n__g':n__f' → n__g':n__f'
activate' :: n__g':n__f' → n__g':n__f'
_hole_n__g':n__f'1 :: n__g':n__f'
_gen_n__g':n__f'2 :: Nat → n__g':n__f'
Lemmas:
activate'(_gen_n__g':n__f'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)
Generator Equations:
_gen_n__g':n__f'2(0) ⇔ _hole_n__g':n__f'1
_gen_n__g':n__f'2(+(x, 1)) ⇔ n__f'(_gen_n__g':n__f'2(x), _hole_n__g':n__f'1)
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
activate'(_gen_n__g':n__f'2(+(1, _n4))) → _*3, rt ∈ Ω(n4)