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

a(lambda(x), y) → lambda(a(x, p(1, a(y, t))))
a(p(x, y), z) → p(a(x, z), a(y, z))
a(a(x, y), z) → a(x, a(y, z))
a(id, x) → x
a(1, id) → 1
a(t, id) → t
a(1, p(x, y)) → x
a(t, p(x, y)) → y

Rewrite Strategy: INNERMOST

Renamed function symbols to avoid clashes with predefined symbol.

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

a'(lambda'(x), y) → lambda'(a'(x, p'(1', a'(y, t'))))
a'(p'(x, y), z) → p'(a'(x, z), a'(y, z))
a'(a'(x, y), z) → a'(x, a'(y, z))
a'(id', x) → x
a'(1', id') → 1'
a'(t', id') → t'
a'(1', p'(x, y)) → x
a'(t', p'(x, y)) → y

Rewrite Strategy: INNERMOST

Infered types.

Rules:
a'(lambda'(x), y) → lambda'(a'(x, p'(1', a'(y, t'))))
a'(p'(x, y), z) → p'(a'(x, z), a'(y, z))
a'(a'(x, y), z) → a'(x, a'(y, z))
a'(id', x) → x
a'(1', id') → 1'
a'(t', id') → t'
a'(1', p'(x, y)) → x
a'(t', p'(x, y)) → y

Types:
a' :: lambda':1':t':p':id' → lambda':1':t':p':id' → lambda':1':t':p':id'
lambda' :: lambda':1':t':p':id' → lambda':1':t':p':id'
p' :: lambda':1':t':p':id' → lambda':1':t':p':id' → lambda':1':t':p':id'
1' :: lambda':1':t':p':id'
t' :: lambda':1':t':p':id'
id' :: lambda':1':t':p':id'
_hole_lambda':1':t':p':id'1 :: lambda':1':t':p':id'
_gen_lambda':1':t':p':id'2 :: Nat → lambda':1':t':p':id'

Heuristically decided to analyse the following defined symbols:
a'

Generator Equations:
_gen_lambda':1':t':p':id'2(0) ⇔ 1'
_gen_lambda':1':t':p':id'2(+(x, 1)) ⇔ lambda'(_gen_lambda':1':t':p':id'2(x))

The following defined symbols remain to be analysed:
a'

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

The following conjecture could not be proven:

a'(_gen_lambda':1':t':p':id'2(1), _gen_lambda':1':t':p':id'2(_n4)) →^? _*3

Generator Equations:
_gen_lambda':1':t':p':id'2(0) ⇔ 1'
_gen_lambda':1':t':p':id'2(+(x, 1)) ⇔ lambda'(_gen_lambda':1':t':p':id'2(x))

No more defined symbols left to analyse.