a__f(b, X, c) → a__f(X, a__c, X)
a__c → b
mark(f(X1, X2, X3)) → a__f(X1, mark(X2), X3)
mark(c) → a__c
mark(b) → b
a__f(X1, X2, X3) → f(X1, X2, X3)
a__c → c
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
a__f'(b', X, c') → a__f'(X, a__c', X)
a__c' → b'
mark'(f'(X1, X2, X3)) → a__f'(X1, mark'(X2), X3)
mark'(c') → a__c'
mark'(b') → b'
a__f'(X1, X2, X3) → f'(X1, X2, X3)
a__c' → c'
Infered types.
Rules:
a__f'(b', X, c') → a__f'(X, a__c', X)
a__c' → b'
mark'(f'(X1, X2, X3)) → a__f'(X1, mark'(X2), X3)
mark'(c') → a__c'
mark'(b') → b'
a__f'(X1, X2, X3) → f'(X1, X2, X3)
a__c' → c'
Types:
a__f' :: b':c':f' → b':c':f' → b':c':f' → b':c':f'
b' :: b':c':f'
c' :: b':c':f'
a__c' :: b':c':f'
mark' :: b':c':f' → b':c':f'
f' :: b':c':f' → b':c':f' → b':c':f' → b':c':f'
_hole_b':c':f'1 :: b':c':f'
_gen_b':c':f'2 :: Nat → b':c':f'
Heuristically decided to analyse the following defined symbols:
a__f', mark'
They will be analysed ascendingly in the following order:
a__f' < mark'
Rules:
a__f'(b', X, c') → a__f'(X, a__c', X)
a__c' → b'
mark'(f'(X1, X2, X3)) → a__f'(X1, mark'(X2), X3)
mark'(c') → a__c'
mark'(b') → b'
a__f'(X1, X2, X3) → f'(X1, X2, X3)
a__c' → c'
Types:
a__f' :: b':c':f' → b':c':f' → b':c':f' → b':c':f'
b' :: b':c':f'
c' :: b':c':f'
a__c' :: b':c':f'
mark' :: b':c':f' → b':c':f'
f' :: b':c':f' → b':c':f' → b':c':f' → b':c':f'
_hole_b':c':f'1 :: b':c':f'
_gen_b':c':f'2 :: Nat → b':c':f'
Generator Equations:
_gen_b':c':f'2(0) ⇔ b'
_gen_b':c':f'2(+(x, 1)) ⇔ f'(b', _gen_b':c':f'2(x), b')
The following defined symbols remain to be analysed:
a__f', mark'
They will be analysed ascendingly in the following order:
a__f' < mark'
Could not prove a rewrite lemma for the defined symbol a__f'.
Rules:
a__f'(b', X, c') → a__f'(X, a__c', X)
a__c' → b'
mark'(f'(X1, X2, X3)) → a__f'(X1, mark'(X2), X3)
mark'(c') → a__c'
mark'(b') → b'
a__f'(X1, X2, X3) → f'(X1, X2, X3)
a__c' → c'
Types:
a__f' :: b':c':f' → b':c':f' → b':c':f' → b':c':f'
b' :: b':c':f'
c' :: b':c':f'
a__c' :: b':c':f'
mark' :: b':c':f' → b':c':f'
f' :: b':c':f' → b':c':f' → b':c':f' → b':c':f'
_hole_b':c':f'1 :: b':c':f'
_gen_b':c':f'2 :: Nat → b':c':f'
Generator Equations:
_gen_b':c':f'2(0) ⇔ b'
_gen_b':c':f'2(+(x, 1)) ⇔ f'(b', _gen_b':c':f'2(x), b')
The following defined symbols remain to be analysed:
mark'
Proved the following rewrite lemma:
mark'(_gen_b':c':f'2(_n26)) → _gen_b':c':f'2(_n26), rt ∈ Ω(1 + n26)
Induction Base:
mark'(_gen_b':c':f'2(0)) →RΩ(1)
b'
Induction Step:
mark'(_gen_b':c':f'2(+(_$n27, 1))) →RΩ(1)
a__f'(b', mark'(_gen_b':c':f'2(_$n27)), b') →IH
a__f'(b', _gen_b':c':f'2(_$n27), b') →RΩ(1)
f'(b', _gen_b':c':f'2(_$n27), b')
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
a__f'(b', X, c') → a__f'(X, a__c', X)
a__c' → b'
mark'(f'(X1, X2, X3)) → a__f'(X1, mark'(X2), X3)
mark'(c') → a__c'
mark'(b') → b'
a__f'(X1, X2, X3) → f'(X1, X2, X3)
a__c' → c'
Types:
a__f' :: b':c':f' → b':c':f' → b':c':f' → b':c':f'
b' :: b':c':f'
c' :: b':c':f'
a__c' :: b':c':f'
mark' :: b':c':f' → b':c':f'
f' :: b':c':f' → b':c':f' → b':c':f' → b':c':f'
_hole_b':c':f'1 :: b':c':f'
_gen_b':c':f'2 :: Nat → b':c':f'
Lemmas:
mark'(_gen_b':c':f'2(_n26)) → _gen_b':c':f'2(_n26), rt ∈ Ω(1 + n26)
Generator Equations:
_gen_b':c':f'2(0) ⇔ b'
_gen_b':c':f'2(+(x, 1)) ⇔ f'(b', _gen_b':c':f'2(x), b')
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
mark'(_gen_b':c':f'2(_n26)) → _gen_b':c':f'2(_n26), rt ∈ Ω(1 + n26)