a(lambda(

a(p(

a(a(

a(id,

a(1, id) -> 1

a(t, id) -> t

a(1, p(

a(t, p(

R

↳Dependency Pair Analysis

A(lambda(x),y) -> A(x, p(1, a(y, t)))

A(lambda(x),y) -> A(y, t)

A(p(x,y),z) -> A(x,z)

A(p(x,y),z) -> A(y,z)

A(a(x,y),z) -> A(x, a(y,z))

A(a(x,y),z) -> A(y,z)

Furthermore,

R

↳DPs

→DP Problem 1

↳Remaining Obligation(s)

The following remains to be proven:

**A(a( x, y), z) -> A(y, z)**

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

innermost

The Proof could not be continued due to a Timeout.

Duration:

1:00 minutes