Runtime Complexity TRS:
The TRS R consists of the following rules:

anchored(Cons(x, xs), y) → anchored(xs, Cons(Cons(Nil, Nil), y))
anchored(Nil, y) → y
goal(x, y) → anchored(x, y)

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

Runtime Complexity TRS:
The TRS R consists of the following rules:


anchored'(Cons'(x, xs), y) → anchored'(xs, Cons'(Cons'(Nil', Nil'), y))
anchored'(Nil', y) → y
goal'(x, y) → anchored'(x, y)

Rewrite Strategy: INNERMOST

Sliced the following arguments:
Cons'/0

Runtime Complexity TRS:
The TRS R consists of the following rules:


anchored'(Cons'(xs), y) → anchored'(xs, Cons'(y))
anchored'(Nil', y) → y
goal'(x, y) → anchored'(x, y)

Rewrite Strategy: INNERMOST

Infered types.

Rules:
anchored'(Cons'(xs), y) → anchored'(xs, Cons'(y))
anchored'(Nil', y) → y
goal'(x, y) → anchored'(x, y)

Types:
anchored' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Heuristically decided to analyse the following defined symbols:
anchored'

Rules:
anchored'(Cons'(xs), y) → anchored'(xs, Cons'(y))
anchored'(Nil', y) → y
goal'(x, y) → anchored'(x, y)

Types:
anchored' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))

The following defined symbols remain to be analysed:
anchored'

Could not prove a rewrite lemma for the defined symbol anchored'.

The following conjecture could not be proven:

anchored'(_gen_Cons':Nil'2(_n4), _gen_Cons':Nil'2(b)) →? _gen_Cons':Nil'2(+(_n4, b))

Rules:
anchored'(Cons'(xs), y) → anchored'(xs, Cons'(y))
anchored'(Nil', y) → y
goal'(x, y) → anchored'(x, y)

Types:
anchored' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
Cons' :: Cons':Nil' → Cons':Nil'
Nil' :: Cons':Nil'
goal' :: Cons':Nil' → Cons':Nil' → Cons':Nil'
_hole_Cons':Nil'1 :: Cons':Nil'
_gen_Cons':Nil'2 :: Nat → Cons':Nil'

Generator Equations:
_gen_Cons':Nil'2(0) ⇔ Nil'
_gen_Cons':Nil'2(+(x, 1)) ⇔ Cons'(_gen_Cons':Nil'2(x))

No more defined symbols left to analyse.