g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldf(x, nil) → x
foldf(x, cons(y, z)) → f(foldf(x, z), y)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, cons(C, c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldf(triple(cons(A, a), nil, c), b))
f''(triple(a, b, c)) → foldf(triple(a, b, nil), c)
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
g'(A') → A'
g'(B') → A'
g'(B') → B'
g'(C') → A'
g'(C') → B'
g'(C') → C'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(a, b, c), C') → triple'(a, b, cons'(C', c))
f'''(triple'(a, b, c), B') → f1(triple'(a, b, c), A')
f'''(triple'(a, b, c), A') → f''''(foldf'(triple'(cons'(A', a), nil', c), b))
f''''(triple'(a, b, c)) → foldf'(triple'(a, b, nil'), c)
Sliced the following arguments:
triple'/0
Runtime Complexity TRS:
The TRS R consists of the following rules:
g'(A') → A'
g'(B') → A'
g'(B') → B'
g'(C') → A'
g'(C') → B'
g'(C') → C'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)
Infered types.
Rules:
g'(A') → A'
g'(B') → A'
g'(B') → B'
g'(C') → A'
g'(C') → B'
g'(C') → C'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)
Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'
Heuristically decided to analyse the following defined symbols:
foldf', f1, f''', f''''
They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = f''''
f''' = f''''
Rules:
g'(A') → A'
g'(B') → A'
g'(B') → B'
g'(C') → A'
g'(C') → B'
g'(C') → C'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)
Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))
The following defined symbols remain to be analysed:
f1, foldf', f''', f''''
They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = f''''
f''' = f''''
Could not prove a rewrite lemma for the defined symbol f1.
Rules:
g'(A') → A'
g'(B') → A'
g'(B') → B'
g'(C') → A'
g'(C') → B'
g'(C') → C'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)
Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))
The following defined symbols remain to be analysed:
f''', foldf', f''''
They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = f''''
f''' = f''''
Could not prove a rewrite lemma for the defined symbol f'''.
Rules:
g'(A') → A'
g'(B') → A'
g'(B') → B'
g'(C') → A'
g'(C') → B'
g'(C') → C'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)
Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))
The following defined symbols remain to be analysed:
f'''', foldf'
They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = f''''
f''' = f''''
Could not prove a rewrite lemma for the defined symbol f''''.
Rules:
g'(A') → A'
g'(B') → A'
g'(B') → B'
g'(C') → A'
g'(C') → B'
g'(C') → C'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)
Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))
The following defined symbols remain to be analysed:
foldf'
They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = f''''
f''' = f''''
Proved the following rewrite lemma:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(_n224)) → triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), rt ∈ Ω(1 + n224)
Induction Base:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(0)) →RΩ(1)
triple'(nil', nil')
Induction Step:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(+(_$n225, 1))) →RΩ(1)
f1(foldf'(triple'(nil', nil'), _gen_nil':cons'4(_$n225)), A') →IH
f1(triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), A') →RΩ(1)
f'''(triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), g'(A')) →RΩ(1)
f'''(triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), A') →RΩ(1)
f''''(foldf'(triple'(nil', _gen_nil':cons'4(0)), _gen_nil':cons'4(0))) →RΩ(1)
f''''(triple'(nil', _gen_nil':cons'4(0))) →RΩ(1)
foldf'(triple'(nil', nil'), _gen_nil':cons'4(0)) →RΩ(1)
triple'(nil', nil')
We have rt ∈ Ω(n) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
Rules:
g'(A') → A'
g'(B') → A'
g'(B') → B'
g'(C') → A'
g'(C') → B'
g'(C') → C'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)
Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'
Lemmas:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(_n224)) → triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), rt ∈ Ω(1 + n224)
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))
The following defined symbols remain to be analysed:
f1, f''', f''''
They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = f''''
f''' = f''''
Could not prove a rewrite lemma for the defined symbol f1.
Rules:
g'(A') → A'
g'(B') → A'
g'(B') → B'
g'(C') → A'
g'(C') → B'
g'(C') → C'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)
Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'
Lemmas:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(_n224)) → triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), rt ∈ Ω(1 + n224)
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))
The following defined symbols remain to be analysed:
f''', f''''
They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = f''''
f''' = f''''
Could not prove a rewrite lemma for the defined symbol f'''.
Rules:
g'(A') → A'
g'(B') → A'
g'(B') → B'
g'(C') → A'
g'(C') → B'
g'(C') → C'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)
Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'
Lemmas:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(_n224)) → triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), rt ∈ Ω(1 + n224)
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))
The following defined symbols remain to be analysed:
f''''
They will be analysed ascendingly in the following order:
foldf' = f1
foldf' = f'''
foldf' = f''''
f1 = f'''
f1 = f''''
f''' = f''''
Could not prove a rewrite lemma for the defined symbol f''''.
Rules:
g'(A') → A'
g'(B') → A'
g'(B') → B'
g'(C') → A'
g'(C') → B'
g'(C') → C'
foldf'(x, nil') → x
foldf'(x, cons'(y, z)) → f1(foldf'(x, z), y)
f1(t, x) → f'''(t, g'(x))
f'''(triple'(b, c), C') → triple'(b, cons'(C', c))
f'''(triple'(b, c), B') → f1(triple'(b, c), A')
f'''(triple'(b, c), A') → f''''(foldf'(triple'(nil', c), b))
f''''(triple'(b, c)) → foldf'(triple'(b, nil'), c)
Types:
g' :: A':B':C' → A':B':C'
A' :: A':B':C'
B' :: A':B':C'
C' :: A':B':C'
foldf' :: triple' → nil':cons' → triple'
nil' :: nil':cons'
cons' :: A':B':C' → nil':cons' → nil':cons'
f1 :: triple' → A':B':C' → triple'
f''' :: triple' → A':B':C' → triple'
triple' :: nil':cons' → nil':cons' → triple'
f'''' :: triple' → triple'
_hole_A':B':C'1 :: A':B':C'
_hole_triple'2 :: triple'
_hole_nil':cons'3 :: nil':cons'
_gen_nil':cons'4 :: Nat → nil':cons'
Lemmas:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(_n224)) → triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), rt ∈ Ω(1 + n224)
Generator Equations:
_gen_nil':cons'4(0) ⇔ nil'
_gen_nil':cons'4(+(x, 1)) ⇔ cons'(A', _gen_nil':cons'4(x))
No more defined symbols left to analyse.
The lowerbound Ω(n) was proven with the following lemma:
foldf'(triple'(nil', nil'), _gen_nil':cons'4(_n224)) → triple'(_gen_nil':cons'4(0), _gen_nil':cons'4(0)), rt ∈ Ω(1 + n224)