f(cons(nil, y)) → y
f(cons(f(cons(nil, y)), z)) → copy(n, y, z)
copy(0, y, z) → f(z)
copy(s(x), y, z) → copy(x, y, cons(f(y), z))
Renamed function symbols to avoid clashes with predefined symbol.
Runtime Complexity TRS:
The TRS R consists of the following rules:
f'(cons'(nil', y)) → y
f'(cons'(f'(cons'(nil', y)), z)) → copy'(n', y, z)
copy'(0', y, z) → f'(z)
copy'(s'(x), y, z) → copy'(x, y, cons'(f'(y), z))
Infered types.
Rules:
f'(cons'(nil', y)) → y
f'(cons'(f'(cons'(nil', y)), z)) → copy'(n', y, z)
copy'(0', y, z) → f'(z)
copy'(s'(x), y, z) → copy'(x, y, cons'(f'(y), z))
Types:
f' :: nil':cons' → nil':cons'
cons' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
copy' :: n':0':s' → nil':cons' → nil':cons' → nil':cons'
n' :: n':0':s'
0' :: n':0':s'
s' :: n':0':s' → n':0':s'
_hole_nil':cons'1 :: nil':cons'
_hole_n':0':s'2 :: n':0':s'
_gen_nil':cons'3 :: Nat → nil':cons'
_gen_n':0':s'4 :: Nat → n':0':s'
Heuristically decided to analyse the following defined symbols:
f', copy'
They will be analysed ascendingly in the following order:
f' = copy'
Rules:
f'(cons'(nil', y)) → y
f'(cons'(f'(cons'(nil', y)), z)) → copy'(n', y, z)
copy'(0', y, z) → f'(z)
copy'(s'(x), y, z) → copy'(x, y, cons'(f'(y), z))
Types:
f' :: nil':cons' → nil':cons'
cons' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
copy' :: n':0':s' → nil':cons' → nil':cons' → nil':cons'
n' :: n':0':s'
0' :: n':0':s'
s' :: n':0':s' → n':0':s'
_hole_nil':cons'1 :: nil':cons'
_hole_n':0':s'2 :: n':0':s'
_gen_nil':cons'3 :: Nat → nil':cons'
_gen_n':0':s'4 :: Nat → n':0':s'
Generator Equations:
_gen_nil':cons'3(0) ⇔ nil'
_gen_nil':cons'3(+(x, 1)) ⇔ cons'(nil', _gen_nil':cons'3(x))
_gen_n':0':s'4(0) ⇔ 0'
_gen_n':0':s'4(+(x, 1)) ⇔ s'(_gen_n':0':s'4(x))
The following defined symbols remain to be analysed:
copy', f'
They will be analysed ascendingly in the following order:
f' = copy'
Could not prove a rewrite lemma for the defined symbol copy'.
The following conjecture could not be proven:
copy'(_gen_n':0':s'4(_n6), _gen_nil':cons'3(1), _gen_nil':cons'3(c)) →? _*5
Rules:
f'(cons'(nil', y)) → y
f'(cons'(f'(cons'(nil', y)), z)) → copy'(n', y, z)
copy'(0', y, z) → f'(z)
copy'(s'(x), y, z) → copy'(x, y, cons'(f'(y), z))
Types:
f' :: nil':cons' → nil':cons'
cons' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
copy' :: n':0':s' → nil':cons' → nil':cons' → nil':cons'
n' :: n':0':s'
0' :: n':0':s'
s' :: n':0':s' → n':0':s'
_hole_nil':cons'1 :: nil':cons'
_hole_n':0':s'2 :: n':0':s'
_gen_nil':cons'3 :: Nat → nil':cons'
_gen_n':0':s'4 :: Nat → n':0':s'
Generator Equations:
_gen_nil':cons'3(0) ⇔ nil'
_gen_nil':cons'3(+(x, 1)) ⇔ cons'(nil', _gen_nil':cons'3(x))
_gen_n':0':s'4(0) ⇔ 0'
_gen_n':0':s'4(+(x, 1)) ⇔ s'(_gen_n':0':s'4(x))
The following defined symbols remain to be analysed:
f'
They will be analysed ascendingly in the following order:
f' = copy'
Could not prove a rewrite lemma for the defined symbol f'.
Rules:
f'(cons'(nil', y)) → y
f'(cons'(f'(cons'(nil', y)), z)) → copy'(n', y, z)
copy'(0', y, z) → f'(z)
copy'(s'(x), y, z) → copy'(x, y, cons'(f'(y), z))
Types:
f' :: nil':cons' → nil':cons'
cons' :: nil':cons' → nil':cons' → nil':cons'
nil' :: nil':cons'
copy' :: n':0':s' → nil':cons' → nil':cons' → nil':cons'
n' :: n':0':s'
0' :: n':0':s'
s' :: n':0':s' → n':0':s'
_hole_nil':cons'1 :: nil':cons'
_hole_n':0':s'2 :: n':0':s'
_gen_nil':cons'3 :: Nat → nil':cons'
_gen_n':0':s'4 :: Nat → n':0':s'
Generator Equations:
_gen_nil':cons'3(0) ⇔ nil'
_gen_nil':cons'3(+(x, 1)) ⇔ cons'(nil', _gen_nil':cons'3(x))
_gen_n':0':s'4(0) ⇔ 0'
_gen_n':0':s'4(+(x, 1)) ⇔ s'(_gen_n':0':s'4(x))
No more defined symbols left to analyse.