U11(tt, M, N) → U12(tt, activate(M), activate(N))
U12(tt, M, N) → s(plus(activate(N), activate(M)))
U21(tt, M, N) → U22(tt, activate(M), activate(N))
U22(tt, M, N) → plus(x(activate(N), activate(M)), activate(N))
plus(N, 0) → N
plus(N, s(M)) → U11(tt, M, N)
x(N, 0) → 0
x(N, s(M)) → U21(tt, M, N)
activate(X) → X
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
U11'(tt', M, N) → U12'(tt', activate'(M), activate'(N))
U12'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U21'(tt', M, N) → U22'(tt', activate'(M), activate'(N))
U22'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
plus'(N, 0') → N
plus'(N, s'(M)) → U11'(tt', M, N)
x'(N, 0') → 0'
x'(N, s'(M)) → U21'(tt', M, N)
activate'(X) → X
Infered types.
Rules:
U11'(tt', M, N) → U12'(tt', activate'(M), activate'(N))
U12'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U21'(tt', M, N) → U22'(tt', activate'(M), activate'(N))
U22'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
plus'(N, 0') → N
plus'(N, s'(M)) → U11'(tt', M, N)
x'(N, 0') → 0'
x'(N, s'(M)) → U21'(tt', M, N)
activate'(X) → X
Types:
U11' :: tt' → s':0' → s':0' → s':0'
tt' :: tt'
U12' :: tt' → s':0' → s':0' → s':0'
activate' :: s':0' → s':0'
s' :: s':0' → s':0'
plus' :: s':0' → s':0' → s':0'
U21' :: tt' → s':0' → s':0' → s':0'
U22' :: tt' → s':0' → s':0' → s':0'
x' :: s':0' → s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_hole_tt'2 :: tt'
_gen_s':0'3 :: Nat → s':0'
Heuristically decided to analyse the following defined symbols:
plus', x'
They will be analysed ascendingly in the following order:
plus' < x'
Rules:
U11'(tt', M, N) → U12'(tt', activate'(M), activate'(N))
U12'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U21'(tt', M, N) → U22'(tt', activate'(M), activate'(N))
U22'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
plus'(N, 0') → N
plus'(N, s'(M)) → U11'(tt', M, N)
x'(N, 0') → 0'
x'(N, s'(M)) → U21'(tt', M, N)
activate'(X) → X
Types:
U11' :: tt' → s':0' → s':0' → s':0'
tt' :: tt'
U12' :: tt' → s':0' → s':0' → s':0'
activate' :: s':0' → s':0'
s' :: s':0' → s':0'
plus' :: s':0' → s':0' → s':0'
U21' :: tt' → s':0' → s':0' → s':0'
U22' :: tt' → s':0' → s':0' → s':0'
x' :: s':0' → s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_hole_tt'2 :: tt'
_gen_s':0'3 :: Nat → s':0'
Generator Equations:
_gen_s':0'3(0) ⇔ 0'
_gen_s':0'3(+(x, 1)) ⇔ s'(_gen_s':0'3(x))
The following defined symbols remain to be analysed:
plus', x'
They will be analysed ascendingly in the following order:
plus' < x'
Proved the following rewrite lemma:
plus'(_gen_s':0'3(a), _gen_s':0'3(_n5)) → _gen_s':0'3(+(_n5, a)), rt ∈ Ω(1 + n5)
Induction Base:
plus'(_gen_s':0'3(a), _gen_s':0'3(0)) →RΩ(1)
_gen_s':0'3(a)
Induction Step:
plus'(_gen_s':0'3(_a162), _gen_s':0'3(+(_$n6, 1))) →RΩ(1)
U11'(tt', _gen_s':0'3(_$n6), _gen_s':0'3(_a162)) →RΩ(1)
U12'(tt', activate'(_gen_s':0'3(_$n6)), activate'(_gen_s':0'3(_a162))) →RΩ(1)
U12'(tt', _gen_s':0'3(_$n6), activate'(_gen_s':0'3(_a162))) →RΩ(1)
U12'(tt', _gen_s':0'3(_$n6), _gen_s':0'3(_a162)) →RΩ(1)
s'(plus'(activate'(_gen_s':0'3(_a162)), activate'(_gen_s':0'3(_$n6)))) →RΩ(1)
s'(plus'(_gen_s':0'3(_a162), activate'(_gen_s':0'3(_$n6)))) →RΩ(1)
s'(plus'(_gen_s':0'3(_a162), _gen_s':0'3(_$n6))) →IH
s'(_gen_s':0'3(+(_$n6, _a162)))
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
U11'(tt', M, N) → U12'(tt', activate'(M), activate'(N))
U12'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U21'(tt', M, N) → U22'(tt', activate'(M), activate'(N))
U22'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
plus'(N, 0') → N
plus'(N, s'(M)) → U11'(tt', M, N)
x'(N, 0') → 0'
x'(N, s'(M)) → U21'(tt', M, N)
activate'(X) → X
Types:
U11' :: tt' → s':0' → s':0' → s':0'
tt' :: tt'
U12' :: tt' → s':0' → s':0' → s':0'
activate' :: s':0' → s':0'
s' :: s':0' → s':0'
plus' :: s':0' → s':0' → s':0'
U21' :: tt' → s':0' → s':0' → s':0'
U22' :: tt' → s':0' → s':0' → s':0'
x' :: s':0' → s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_hole_tt'2 :: tt'
_gen_s':0'3 :: Nat → s':0'
Lemmas:
plus'(_gen_s':0'3(a), _gen_s':0'3(_n5)) → _gen_s':0'3(+(_n5, a)), rt ∈ Ω(1 + n5)
Generator Equations:
_gen_s':0'3(0) ⇔ 0'
_gen_s':0'3(+(x, 1)) ⇔ s'(_gen_s':0'3(x))
The following defined symbols remain to be analysed:
x'
Proved the following rewrite lemma:
x'(_gen_s':0'3(a), _gen_s':0'3(_n1337)) → _gen_s':0'3(*(_n1337, a)), rt ∈ Ω(1 + a1614·n1337 + n1337)
Induction Base:
x'(_gen_s':0'3(a), _gen_s':0'3(0)) →RΩ(1)
0'
Induction Step:
x'(_gen_s':0'3(_a1614), _gen_s':0'3(+(_$n1338, 1))) →RΩ(1)
U21'(tt', _gen_s':0'3(_$n1338), _gen_s':0'3(_a1614)) →RΩ(1)
U22'(tt', activate'(_gen_s':0'3(_$n1338)), activate'(_gen_s':0'3(_a1614))) →RΩ(1)
U22'(tt', _gen_s':0'3(_$n1338), activate'(_gen_s':0'3(_a1614))) →RΩ(1)
U22'(tt', _gen_s':0'3(_$n1338), _gen_s':0'3(_a1614)) →RΩ(1)
plus'(x'(activate'(_gen_s':0'3(_a1614)), activate'(_gen_s':0'3(_$n1338))), activate'(_gen_s':0'3(_a1614))) →RΩ(1)
plus'(x'(_gen_s':0'3(_a1614), activate'(_gen_s':0'3(_$n1338))), activate'(_gen_s':0'3(_a1614))) →RΩ(1)
plus'(x'(_gen_s':0'3(_a1614), _gen_s':0'3(_$n1338)), activate'(_gen_s':0'3(_a1614))) →IH
plus'(_gen_s':0'3(*(_$n1338, _a1614)), activate'(_gen_s':0'3(_a1614))) →RΩ(1)
plus'(_gen_s':0'3(*(_$n1338, _a1614)), _gen_s':0'3(_a1614)) →LΩ(1 + a1614)
_gen_s':0'3(+(_a1614, *(_$n1338, _a1614)))
We have rt ∈ Ω(n2) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n2).
Rules:
U11'(tt', M, N) → U12'(tt', activate'(M), activate'(N))
U12'(tt', M, N) → s'(plus'(activate'(N), activate'(M)))
U21'(tt', M, N) → U22'(tt', activate'(M), activate'(N))
U22'(tt', M, N) → plus'(x'(activate'(N), activate'(M)), activate'(N))
plus'(N, 0') → N
plus'(N, s'(M)) → U11'(tt', M, N)
x'(N, 0') → 0'
x'(N, s'(M)) → U21'(tt', M, N)
activate'(X) → X
Types:
U11' :: tt' → s':0' → s':0' → s':0'
tt' :: tt'
U12' :: tt' → s':0' → s':0' → s':0'
activate' :: s':0' → s':0'
s' :: s':0' → s':0'
plus' :: s':0' → s':0' → s':0'
U21' :: tt' → s':0' → s':0' → s':0'
U22' :: tt' → s':0' → s':0' → s':0'
x' :: s':0' → s':0' → s':0'
0' :: s':0'
_hole_s':0'1 :: s':0'
_hole_tt'2 :: tt'
_gen_s':0'3 :: Nat → s':0'
Lemmas:
plus'(_gen_s':0'3(a), _gen_s':0'3(_n5)) → _gen_s':0'3(+(_n5, a)), rt ∈ Ω(1 + n5)
x'(_gen_s':0'3(a), _gen_s':0'3(_n1337)) → _gen_s':0'3(*(_n1337, a)), rt ∈ Ω(1 + a1614·n1337 + n1337)
Generator Equations:
_gen_s':0'3(0) ⇔ 0'
_gen_s':0'3(+(x, 1)) ⇔ s'(_gen_s':0'3(x))
No more defined symbols left to analyse.
The lowerbound Ω(n2) was proven with the following lemma:
x'(_gen_s':0'3(a), _gen_s':0'3(_n1337)) → _gen_s':0'3(*(_n1337, a)), rt ∈ Ω(1 + a1614·n1337 + n1337)