78.18/34.71 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml

78.18/34.71

78.18/34.71
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), INFINITE).

0 CpxTRS

78.18/34.71

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))

78.18/34.71

↳2 CdtProblem

78.18/34.71

↳3 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

78.18/34.71

↳4 CdtProblem

78.18/34.71

↳5 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

78.18/34.71

↳6 CdtProblem

78.18/34.71

↳7 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

78.18/34.71

↳8 CdtProblem

78.18/34.71

78.18/34.71 78.18/34.71

78.18/34.71

(0) Obligation:

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

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

Rewrite Strategy: INNERMOST

78.18/34.71

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

78.18/34.71

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(lambda(z0), z1) → lambda(a(z0, p(1, a(z1, t)))) 78.18/34.71
a(p(z0, z1), z2) → p(a(z0, z2), a(z1, z2)) 78.18/34.71
a(a(z0, z1), z2) → a(z0, a(z1, z2)) 78.18/34.71
a(id, z0) → z0 78.18/34.71
a(1, id) → 1 78.18/34.71
a(t, id) → t 78.18/34.71
a(1, p(z0, z1)) → z0 78.18/34.71
a(t, p(z0, z1)) → z1

Tuples:

A(lambda(z0), z1) → c(A(z0, p(1, a(z1, t))), A(z1, t)) 78.18/34.71
A(p(z0, z1), z2) → c1(A(z0, z2), A(z1, z2)) 78.18/34.71
A(a(z0, z1), z2) → c2(A(z0, a(z1, z2)), A(z1, z2))

S tuples:

A(lambda(z0), z1) → c(A(z0, p(1, a(z1, t))), A(z1, t)) 78.18/34.72
A(p(z0, z1), z2) → c1(A(z0, z2), A(z1, z2)) 78.18/34.72
A(a(z0, z1), z2) → c2(A(z0, a(z1, z2)), A(z1, z2))

K tuples:none
Defined Rule Symbols:

a

Defined Pair Symbols:

A

Compound Symbols:

c, c1, c2

78.18/34.72

(3) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace A(p(z0, z1), z2) → c1(A(z0, z2), A(z1, z2)) by

A(p(lambda(y0), z1), z2) → c1(A(lambda(y0), z2), A(z1, z2)) 78.18/34.72
A(p(z0, lambda(y0)), z2) → c1(A(z0, z2), A(lambda(y0), z2)) 78.18/34.72
A(p(p(y0, y1), z1), z2) → c1(A(p(y0, y1), z2), A(z1, z2)) 78.18/34.72
A(p(z0, p(y0, y1)), z2) → c1(A(z0, z2), A(p(y0, y1), z2)) 78.18/34.72
A(p(a(y0, y1), z1), z2) → c1(A(a(y0, y1), z2), A(z1, z2)) 78.18/34.72
A(p(z0, a(y0, y1)), z2) → c1(A(z0, z2), A(a(y0, y1), z2))

78.18/34.72

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(lambda(z0), z1) → lambda(a(z0, p(1, a(z1, t)))) 78.18/34.72
a(p(z0, z1), z2) → p(a(z0, z2), a(z1, z2)) 78.18/34.72
a(a(z0, z1), z2) → a(z0, a(z1, z2)) 78.18/34.72
a(id, z0) → z0 78.18/34.72
a(1, id) → 1 78.18/34.72
a(t, id) → t 78.18/34.72
a(1, p(z0, z1)) → z0 78.18/34.72
a(t, p(z0, z1)) → z1

Tuples:

A(lambda(z0), z1) → c(A(z0, p(1, a(z1, t))), A(z1, t)) 78.18/34.72
A(a(z0, z1), z2) → c2(A(z0, a(z1, z2)), A(z1, z2)) 78.18/34.72
A(p(lambda(y0), z1), z2) → c1(A(lambda(y0), z2), A(z1, z2)) 78.18/34.72
A(p(z0, lambda(y0)), z2) → c1(A(z0, z2), A(lambda(y0), z2)) 78.18/34.72
A(p(p(y0, y1), z1), z2) → c1(A(p(y0, y1), z2), A(z1, z2)) 78.18/34.72
A(p(z0, p(y0, y1)), z2) → c1(A(z0, z2), A(p(y0, y1), z2)) 78.18/34.72
A(p(a(y0, y1), z1), z2) → c1(A(a(y0, y1), z2), A(z1, z2)) 78.18/34.72
A(p(z0, a(y0, y1)), z2) → c1(A(z0, z2), A(a(y0, y1), z2))

S tuples:

A(lambda(z0), z1) → c(A(z0, p(1, a(z1, t))), A(z1, t)) 78.18/34.72
A(a(z0, z1), z2) → c2(A(z0, a(z1, z2)), A(z1, z2)) 78.18/34.72
A(p(lambda(y0), z1), z2) → c1(A(lambda(y0), z2), A(z1, z2)) 78.18/34.72
A(p(z0, lambda(y0)), z2) → c1(A(z0, z2), A(lambda(y0), z2)) 78.18/34.72
A(p(p(y0, y1), z1), z2) → c1(A(p(y0, y1), z2), A(z1, z2)) 78.18/34.72
A(p(z0, p(y0, y1)), z2) → c1(A(z0, z2), A(p(y0, y1), z2)) 78.18/34.72
A(p(a(y0, y1), z1), z2) → c1(A(a(y0, y1), z2), A(z1, z2)) 78.18/34.72
A(p(z0, a(y0, y1)), z2) → c1(A(z0, z2), A(a(y0, y1), z2))

K tuples:none
Defined Rule Symbols:

a

Defined Pair Symbols:

A

Compound Symbols:

c, c2, c1

78.18/34.72

(5) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace A(p(p(y0, y1), z1), z2) → c1(A(p(y0, y1), z2), A(z1, z2)) by

A(p(p(z0, z1), lambda(y0)), z3) → c1(A(p(z0, z1), z3), A(lambda(y0), z3)) 78.18/34.72
A(p(p(z0, z1), a(y0, y1)), z3) → c1(A(p(z0, z1), z3), A(a(y0, y1), z3)) 78.18/34.72
A(p(p(lambda(y0), z1), z2), z3) → c1(A(p(lambda(y0), z1), z3), A(z2, z3)) 78.18/34.72
A(p(p(z0, z1), p(lambda(y0), y1)), z3) → c1(A(p(z0, z1), z3), A(p(lambda(y0), y1), z3)) 78.18/34.72
A(p(p(z0, lambda(y1)), z2), z3) → c1(A(p(z0, lambda(y1)), z3), A(z2, z3)) 78.18/34.72
A(p(p(z0, z1), p(y0, lambda(y1))), z3) → c1(A(p(z0, z1), z3), A(p(y0, lambda(y1)), z3)) 78.18/34.72
A(p(p(p(y0, y1), z1), z2), z3) → c1(A(p(p(y0, y1), z1), z3), A(z2, z3)) 78.18/34.72
A(p(p(z0, z1), p(p(y0, y1), y2)), z3) → c1(A(p(z0, z1), z3), A(p(p(y0, y1), y2), z3)) 78.18/34.72
A(p(p(z0, p(y1, y2)), z2), z3) → c1(A(p(z0, p(y1, y2)), z3), A(z2, z3)) 78.18/34.72
A(p(p(z0, z1), p(y0, p(y1, y2))), z3) → c1(A(p(z0, z1), z3), A(p(y0, p(y1, y2)), z3)) 78.18/34.72
A(p(p(a(y0, y1), z1), z2), z3) → c1(A(p(a(y0, y1), z1), z3), A(z2, z3)) 78.18/34.72
A(p(p(z0, z1), p(a(y0, y1), y2)), z3) → c1(A(p(z0, z1), z3), A(p(a(y0, y1), y2), z3)) 78.18/34.72
A(p(p(z0, a(y1, y2)), z2), z3) → c1(A(p(z0, a(y1, y2)), z3), A(z2, z3)) 78.18/34.72
A(p(p(z0, z1), p(y0, a(y1, y2))), z3) → c1(A(p(z0, z1), z3), A(p(y0, a(y1, y2)), z3))

78.18/34.72

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(lambda(z0), z1) → lambda(a(z0, p(1, a(z1, t)))) 78.18/34.72
a(p(z0, z1), z2) → p(a(z0, z2), a(z1, z2)) 78.18/34.72
a(a(z0, z1), z2) → a(z0, a(z1, z2)) 78.18/34.72
a(id, z0) → z0 78.18/34.72
a(1, id) → 1 78.18/34.72
a(t, id) → t 78.18/34.72
a(1, p(z0, z1)) → z0 78.18/34.72
a(t, p(z0, z1)) → z1

Tuples:

A(lambda(z0), z1) → c(A(z0, p(1, a(z1, t))), A(z1, t)) 78.18/34.72
A(a(z0, z1), z2) → c2(A(z0, a(z1, z2)), A(z1, z2)) 78.18/34.72
A(p(lambda(y0), z1), z2) → c1(A(lambda(y0), z2), A(z1, z2)) 78.18/34.72
A(p(z0, lambda(y0)), z2) → c1(A(z0, z2), A(lambda(y0), z2)) 78.18/34.72
A(p(z0, p(y0, y1)), z2) → c1(A(z0, z2), A(p(y0, y1), z2)) 78.18/34.72
A(p(a(y0, y1), z1), z2) → c1(A(a(y0, y1), z2), A(z1, z2)) 78.18/34.72
A(p(z0, a(y0, y1)), z2) → c1(A(z0, z2), A(a(y0, y1), z2)) 78.18/34.72
A(p(p(z0, z1), lambda(y0)), z3) → c1(A(p(z0, z1), z3), A(lambda(y0), z3)) 78.18/34.72
A(p(p(z0, z1), a(y0, y1)), z3) → c1(A(p(z0, z1), z3), A(a(y0, y1), z3)) 78.18/34.72
A(p(p(lambda(y0), z1), z2), z3) → c1(A(p(lambda(y0), z1), z3), A(z2, z3)) 78.18/34.72
A(p(p(z0, z1), p(lambda(y0), y1)), z3) → c1(A(p(z0, z1), z3), A(p(lambda(y0), y1), z3)) 78.18/34.72
A(p(p(z0, lambda(y1)), z2), z3) → c1(A(p(z0, lambda(y1)), z3), A(z2, z3)) 78.18/34.72
A(p(p(z0, z1), p(y0, lambda(y1))), z3) → c1(A(p(z0, z1), z3), A(p(y0, lambda(y1)), z3)) 78.18/34.72
A(p(p(p(y0, y1), z1), z2), z3) → c1(A(p(p(y0, y1), z1), z3), A(z2, z3)) 78.18/34.72
A(p(p(z0, z1), p(p(y0, y1), y2)), z3) → c1(A(p(z0, z1), z3), A(p(p(y0, y1), y2), z3)) 78.18/34.72
A(p(p(z0, p(y1, y2)), z2), z3) → c1(A(p(z0, p(y1, y2)), z3), A(z2, z3)) 78.18/34.72
A(p(p(z0, z1), p(y0, p(y1, y2))), z3) → c1(A(p(z0, z1), z3), A(p(y0, p(y1, y2)), z3)) 78.18/34.72
A(p(p(a(y0, y1), z1), z2), z3) → c1(A(p(a(y0, y1), z1), z3), A(z2, z3)) 78.18/34.72
A(p(p(z0, z1), p(a(y0, y1), y2)), z3) → c1(A(p(z0, z1), z3), A(p(a(y0, y1), y2), z3)) 78.18/34.72
A(p(p(z0, a(y1, y2)), z2), z3) → c1(A(p(z0, a(y1, y2)), z3), A(z2, z3)) 78.18/34.73
A(p(p(z0, z1), p(y0, a(y1, y2))), z3) → c1(A(p(z0, z1), z3), A(p(y0, a(y1, y2)), z3))

S tuples:

A(lambda(z0), z1) → c(A(z0, p(1, a(z1, t))), A(z1, t)) 78.18/34.73
A(a(z0, z1), z2) → c2(A(z0, a(z1, z2)), A(z1, z2)) 78.18/34.73
A(p(lambda(y0), z1), z2) → c1(A(lambda(y0), z2), A(z1, z2)) 78.18/34.73
A(p(z0, lambda(y0)), z2) → c1(A(z0, z2), A(lambda(y0), z2)) 78.18/34.73
A(p(z0, p(y0, y1)), z2) → c1(A(z0, z2), A(p(y0, y1), z2)) 78.18/34.73
A(p(a(y0, y1), z1), z2) → c1(A(a(y0, y1), z2), A(z1, z2)) 78.18/34.73
A(p(z0, a(y0, y1)), z2) → c1(A(z0, z2), A(a(y0, y1), z2)) 78.18/34.73
A(p(p(z0, z1), lambda(y0)), z3) → c1(A(p(z0, z1), z3), A(lambda(y0), z3)) 78.18/34.73
A(p(p(z0, z1), a(y0, y1)), z3) → c1(A(p(z0, z1), z3), A(a(y0, y1), z3)) 78.18/34.73
A(p(p(lambda(y0), z1), z2), z3) → c1(A(p(lambda(y0), z1), z3), A(z2, z3)) 78.18/34.73
A(p(p(z0, z1), p(lambda(y0), y1)), z3) → c1(A(p(z0, z1), z3), A(p(lambda(y0), y1), z3)) 78.18/34.73
A(p(p(z0, lambda(y1)), z2), z3) → c1(A(p(z0, lambda(y1)), z3), A(z2, z3)) 78.18/34.73
A(p(p(z0, z1), p(y0, lambda(y1))), z3) → c1(A(p(z0, z1), z3), A(p(y0, lambda(y1)), z3)) 78.18/34.73
A(p(p(p(y0, y1), z1), z2), z3) → c1(A(p(p(y0, y1), z1), z3), A(z2, z3)) 78.18/34.73
A(p(p(z0, z1), p(p(y0, y1), y2)), z3) → c1(A(p(z0, z1), z3), A(p(p(y0, y1), y2), z3)) 78.18/34.73
A(p(p(z0, p(y1, y2)), z2), z3) → c1(A(p(z0, p(y1, y2)), z3), A(z2, z3)) 78.18/34.73
A(p(p(z0, z1), p(y0, p(y1, y2))), z3) → c1(A(p(z0, z1), z3), A(p(y0, p(y1, y2)), z3)) 78.18/34.73
A(p(p(a(y0, y1), z1), z2), z3) → c1(A(p(a(y0, y1), z1), z3), A(z2, z3)) 78.18/34.73
A(p(p(z0, z1), p(a(y0, y1), y2)), z3) → c1(A(p(z0, z1), z3), A(p(a(y0, y1), y2), z3)) 78.18/34.73
A(p(p(z0, a(y1, y2)), z2), z3) → c1(A(p(z0, a(y1, y2)), z3), A(z2, z3)) 78.18/34.73
A(p(p(z0, z1), p(y0, a(y1, y2))), z3) → c1(A(p(z0, z1), z3), A(p(y0, a(y1, y2)), z3))

K tuples:none
Defined Rule Symbols:

a

Defined Pair Symbols:

A

Compound Symbols:

c, c2, c1

78.18/34.73

(7) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace A(p(z0, p(y0, y1)), z2) → c1(A(z0, z2), A(p(y0, y1), z2)) by

A(p(lambda(y0), p(z1, z2)), z3) → c1(A(lambda(y0), z3), A(p(z1, z2), z3)) 78.18/34.73
A(p(a(y0, y1), p(z1, z2)), z3) → c1(A(a(y0, y1), z3), A(p(z1, z2), z3)) 78.18/34.73
A(p(p(lambda(y0), y1), p(z1, z2)), z3) → c1(A(p(lambda(y0), y1), z3), A(p(z1, z2), z3)) 78.18/34.73
A(p(z0, p(lambda(y0), z2)), z3) → c1(A(z0, z3), A(p(lambda(y0), z2), z3)) 78.18/34.73
A(p(p(y0, lambda(y1)), p(z1, z2)), z3) → c1(A(p(y0, lambda(y1)), z3), A(p(z1, z2), z3)) 78.18/34.73
A(p(z0, p(z1, lambda(y1))), z3) → c1(A(z0, z3), A(p(z1, lambda(y1)), z3)) 78.18/34.73
A(p(p(y0, p(y1, y2)), p(z1, z2)), z3) → c1(A(p(y0, p(y1, y2)), z3), A(p(z1, z2), z3)) 78.18/34.73
A(p(z0, p(z1, p(y1, y2))), z3) → c1(A(z0, z3), A(p(z1, p(y1, y2)), z3)) 78.18/34.73
A(p(p(a(y0, y1), y2), p(z1, z2)), z3) → c1(A(p(a(y0, y1), y2), z3), A(p(z1, z2), z3)) 78.18/34.73
A(p(z0, p(a(y0, y1), z2)), z3) → c1(A(z0, z3), A(p(a(y0, y1), z2), z3)) 78.18/34.73
A(p(p(y0, a(y1, y2)), p(z1, z2)), z3) → c1(A(p(y0, a(y1, y2)), z3), A(p(z1, z2), z3)) 78.18/34.73
A(p(z0, p(z1, a(y1, y2))), z3) → c1(A(z0, z3), A(p(z1, a(y1, y2)), z3)) 78.18/34.73
A(p(p(p(y0, y1), lambda(y2)), p(z1, z2)), z3) → c1(A(p(p(y0, y1), lambda(y2)), z3), A(p(z1, z2), z3)) 78.18/34.73
A(p(z0, p(p(y0, y1), lambda(y2))), z3) → c1(A(z0, z3), A(p(p(y0, y1), lambda(y2)), z3)) 78.18/34.73
A(p(p(p(y0, y1), a(y2, y3)), p(z1, z2)), z3) → c1(A(p(p(y0, y1), a(y2, y3)), z3), A(p(z1, z2), z3)) 78.18/34.73
A(p(z0, p(p(y0, y1), a(y2, y3))), z3) → c1(A(z0, z3), A(p(p(y0, y1), a(y2, y3)), z3)) 78.18/34.73
A(p(p(p(lambda(y0), y1), y2), p(z1, z2)), z3) → c1(A(p(p(lambda(y0), y1), y2), z3), A(p(z1, z2), z3)) 78.18/34.73
A(p(z0, p(p(lambda(y0), y1), z2)), z3) → c1(A(z0, z3), A(p(p(lambda(y0), y1), z2), z3)) 78.18/34.73
A(p(p(p(y0, y1), p(lambda(y2), y3)), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(lambda(y2), y3)), z3), A(p(z1, z2), z3)) 78.18/34.73
A(p(z0, p(p(y0, y1), p(lambda(y2), y3))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(lambda(y2), y3)), z3)) 78.18/34.73
A(p(p(p(y0, lambda(y1)), y2), p(z1, z2)), z3) → c1(A(p(p(y0, lambda(y1)), y2), z3), A(p(z1, z2), z3)) 78.18/34.73
A(p(z0, p(p(y0, lambda(y1)), z2)), z3) → c1(A(z0, z3), A(p(p(y0, lambda(y1)), z2), z3)) 78.18/34.73
A(p(p(p(y0, y1), p(y2, lambda(y3))), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(y2, lambda(y3))), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(y2, lambda(y3)))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(y2, lambda(y3))), z3)) 78.18/34.74
A(p(p(p(p(y0, y1), y2), y3), p(z1, z2)), z3) → c1(A(p(p(p(y0, y1), y2), y3), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(p(y0, y1), y2), z2)), z3) → c1(A(z0, z3), A(p(p(p(y0, y1), y2), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(p(y2, y3), y4)), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(p(y2, y3), y4)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(p(y2, y3), y4))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(p(y2, y3), y4)), z3)) 78.18/34.74
A(p(p(p(y0, p(y1, y2)), y3), p(z1, z2)), z3) → c1(A(p(p(y0, p(y1, y2)), y3), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, p(y1, y2)), z2)), z3) → c1(A(z0, z3), A(p(p(y0, p(y1, y2)), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(y2, p(y3, y4))), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(y2, p(y3, y4))), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(y2, p(y3, y4)))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(y2, p(y3, y4))), z3)) 78.18/34.74
A(p(p(p(a(y0, y1), y2), y3), p(z1, z2)), z3) → c1(A(p(p(a(y0, y1), y2), y3), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(a(y0, y1), y2), z2)), z3) → c1(A(z0, z3), A(p(p(a(y0, y1), y2), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(a(y2, y3), y4)), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(a(y2, y3), y4)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(a(y2, y3), y4))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(a(y2, y3), y4)), z3)) 78.18/34.74
A(p(p(p(y0, a(y1, y2)), y3), p(z1, z2)), z3) → c1(A(p(p(y0, a(y1, y2)), y3), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, a(y1, y2)), z2)), z3) → c1(A(z0, z3), A(p(p(y0, a(y1, y2)), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(y2, a(y3, y4))), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(y2, a(y3, y4))), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(y2, a(y3, y4)))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(y2, a(y3, y4))), z3))

78.18/34.74

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

a(lambda(z0), z1) → lambda(a(z0, p(1, a(z1, t)))) 78.18/34.74
a(p(z0, z1), z2) → p(a(z0, z2), a(z1, z2)) 78.18/34.74
a(a(z0, z1), z2) → a(z0, a(z1, z2)) 78.18/34.74
a(id, z0) → z0 78.18/34.74
a(1, id) → 1 78.18/34.74
a(t, id) → t 78.18/34.74
a(1, p(z0, z1)) → z0 78.18/34.74
a(t, p(z0, z1)) → z1

Tuples:

A(lambda(z0), z1) → c(A(z0, p(1, a(z1, t))), A(z1, t)) 78.18/34.74
A(a(z0, z1), z2) → c2(A(z0, a(z1, z2)), A(z1, z2)) 78.18/34.74
A(p(lambda(y0), z1), z2) → c1(A(lambda(y0), z2), A(z1, z2)) 78.18/34.74
A(p(z0, lambda(y0)), z2) → c1(A(z0, z2), A(lambda(y0), z2)) 78.18/34.74
A(p(a(y0, y1), z1), z2) → c1(A(a(y0, y1), z2), A(z1, z2)) 78.18/34.74
A(p(z0, a(y0, y1)), z2) → c1(A(z0, z2), A(a(y0, y1), z2)) 78.18/34.74
A(p(p(z0, z1), lambda(y0)), z3) → c1(A(p(z0, z1), z3), A(lambda(y0), z3)) 78.18/34.74
A(p(p(z0, z1), a(y0, y1)), z3) → c1(A(p(z0, z1), z3), A(a(y0, y1), z3)) 78.18/34.74
A(p(p(lambda(y0), z1), z2), z3) → c1(A(p(lambda(y0), z1), z3), A(z2, z3)) 78.18/34.74
A(p(p(z0, z1), p(lambda(y0), y1)), z3) → c1(A(p(z0, z1), z3), A(p(lambda(y0), y1), z3)) 78.18/34.74
A(p(p(z0, lambda(y1)), z2), z3) → c1(A(p(z0, lambda(y1)), z3), A(z2, z3)) 78.18/34.74
A(p(p(z0, z1), p(y0, lambda(y1))), z3) → c1(A(p(z0, z1), z3), A(p(y0, lambda(y1)), z3)) 78.18/34.74
A(p(p(p(y0, y1), z1), z2), z3) → c1(A(p(p(y0, y1), z1), z3), A(z2, z3)) 78.18/34.74
A(p(p(z0, z1), p(p(y0, y1), y2)), z3) → c1(A(p(z0, z1), z3), A(p(p(y0, y1), y2), z3)) 78.18/34.74
A(p(p(z0, p(y1, y2)), z2), z3) → c1(A(p(z0, p(y1, y2)), z3), A(z2, z3)) 78.18/34.74
A(p(p(z0, z1), p(y0, p(y1, y2))), z3) → c1(A(p(z0, z1), z3), A(p(y0, p(y1, y2)), z3)) 78.18/34.74
A(p(p(a(y0, y1), z1), z2), z3) → c1(A(p(a(y0, y1), z1), z3), A(z2, z3)) 78.18/34.74
A(p(p(z0, z1), p(a(y0, y1), y2)), z3) → c1(A(p(z0, z1), z3), A(p(a(y0, y1), y2), z3)) 78.18/34.74
A(p(p(z0, a(y1, y2)), z2), z3) → c1(A(p(z0, a(y1, y2)), z3), A(z2, z3)) 78.18/34.74
A(p(p(z0, z1), p(y0, a(y1, y2))), z3) → c1(A(p(z0, z1), z3), A(p(y0, a(y1, y2)), z3)) 78.18/34.74
A(p(lambda(y0), p(z1, z2)), z3) → c1(A(lambda(y0), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(a(y0, y1), p(z1, z2)), z3) → c1(A(a(y0, y1), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(p(lambda(y0), y1), p(z1, z2)), z3) → c1(A(p(lambda(y0), y1), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(lambda(y0), z2)), z3) → c1(A(z0, z3), A(p(lambda(y0), z2), z3)) 78.18/34.74
A(p(p(y0, lambda(y1)), p(z1, z2)), z3) → c1(A(p(y0, lambda(y1)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(z1, lambda(y1))), z3) → c1(A(z0, z3), A(p(z1, lambda(y1)), z3)) 78.18/34.74
A(p(p(y0, p(y1, y2)), p(z1, z2)), z3) → c1(A(p(y0, p(y1, y2)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(z1, p(y1, y2))), z3) → c1(A(z0, z3), A(p(z1, p(y1, y2)), z3)) 78.18/34.74
A(p(p(a(y0, y1), y2), p(z1, z2)), z3) → c1(A(p(a(y0, y1), y2), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(a(y0, y1), z2)), z3) → c1(A(z0, z3), A(p(a(y0, y1), z2), z3)) 78.18/34.74
A(p(p(y0, a(y1, y2)), p(z1, z2)), z3) → c1(A(p(y0, a(y1, y2)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(z1, a(y1, y2))), z3) → c1(A(z0, z3), A(p(z1, a(y1, y2)), z3)) 78.18/34.74
A(p(p(p(y0, y1), lambda(y2)), p(z1, z2)), z3) → c1(A(p(p(y0, y1), lambda(y2)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), lambda(y2))), z3) → c1(A(z0, z3), A(p(p(y0, y1), lambda(y2)), z3)) 78.18/34.74
A(p(p(p(y0, y1), a(y2, y3)), p(z1, z2)), z3) → c1(A(p(p(y0, y1), a(y2, y3)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), a(y2, y3))), z3) → c1(A(z0, z3), A(p(p(y0, y1), a(y2, y3)), z3)) 78.18/34.74
A(p(p(p(lambda(y0), y1), y2), p(z1, z2)), z3) → c1(A(p(p(lambda(y0), y1), y2), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(lambda(y0), y1), z2)), z3) → c1(A(z0, z3), A(p(p(lambda(y0), y1), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(lambda(y2), y3)), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(lambda(y2), y3)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(lambda(y2), y3))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(lambda(y2), y3)), z3)) 78.18/34.74
A(p(p(p(y0, lambda(y1)), y2), p(z1, z2)), z3) → c1(A(p(p(y0, lambda(y1)), y2), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, lambda(y1)), z2)), z3) → c1(A(z0, z3), A(p(p(y0, lambda(y1)), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(y2, lambda(y3))), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(y2, lambda(y3))), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(y2, lambda(y3)))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(y2, lambda(y3))), z3)) 78.18/34.74
A(p(p(p(p(y0, y1), y2), y3), p(z1, z2)), z3) → c1(A(p(p(p(y0, y1), y2), y3), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(p(y0, y1), y2), z2)), z3) → c1(A(z0, z3), A(p(p(p(y0, y1), y2), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(p(y2, y3), y4)), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(p(y2, y3), y4)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(p(y2, y3), y4))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(p(y2, y3), y4)), z3)) 78.18/34.74
A(p(p(p(y0, p(y1, y2)), y3), p(z1, z2)), z3) → c1(A(p(p(y0, p(y1, y2)), y3), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, p(y1, y2)), z2)), z3) → c1(A(z0, z3), A(p(p(y0, p(y1, y2)), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(y2, p(y3, y4))), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(y2, p(y3, y4))), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(y2, p(y3, y4)))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(y2, p(y3, y4))), z3)) 78.18/34.74
A(p(p(p(a(y0, y1), y2), y3), p(z1, z2)), z3) → c1(A(p(p(a(y0, y1), y2), y3), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(a(y0, y1), y2), z2)), z3) → c1(A(z0, z3), A(p(p(a(y0, y1), y2), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(a(y2, y3), y4)), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(a(y2, y3), y4)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(a(y2, y3), y4))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(a(y2, y3), y4)), z3)) 78.18/34.74
A(p(p(p(y0, a(y1, y2)), y3), p(z1, z2)), z3) → c1(A(p(p(y0, a(y1, y2)), y3), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, a(y1, y2)), z2)), z3) → c1(A(z0, z3), A(p(p(y0, a(y1, y2)), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(y2, a(y3, y4))), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(y2, a(y3, y4))), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(y2, a(y3, y4)))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(y2, a(y3, y4))), z3))

S tuples:

A(lambda(z0), z1) → c(A(z0, p(1, a(z1, t))), A(z1, t)) 78.18/34.74
A(a(z0, z1), z2) → c2(A(z0, a(z1, z2)), A(z1, z2)) 78.18/34.74
A(p(lambda(y0), z1), z2) → c1(A(lambda(y0), z2), A(z1, z2)) 78.18/34.74
A(p(z0, lambda(y0)), z2) → c1(A(z0, z2), A(lambda(y0), z2)) 78.18/34.74
A(p(a(y0, y1), z1), z2) → c1(A(a(y0, y1), z2), A(z1, z2)) 78.18/34.74
A(p(z0, a(y0, y1)), z2) → c1(A(z0, z2), A(a(y0, y1), z2)) 78.18/34.74
A(p(p(z0, z1), lambda(y0)), z3) → c1(A(p(z0, z1), z3), A(lambda(y0), z3)) 78.18/34.74
A(p(p(z0, z1), a(y0, y1)), z3) → c1(A(p(z0, z1), z3), A(a(y0, y1), z3)) 78.18/34.74
A(p(p(lambda(y0), z1), z2), z3) → c1(A(p(lambda(y0), z1), z3), A(z2, z3)) 78.18/34.74
A(p(p(z0, z1), p(lambda(y0), y1)), z3) → c1(A(p(z0, z1), z3), A(p(lambda(y0), y1), z3)) 78.18/34.74
A(p(p(z0, lambda(y1)), z2), z3) → c1(A(p(z0, lambda(y1)), z3), A(z2, z3)) 78.18/34.74
A(p(p(z0, z1), p(y0, lambda(y1))), z3) → c1(A(p(z0, z1), z3), A(p(y0, lambda(y1)), z3)) 78.18/34.74
A(p(p(p(y0, y1), z1), z2), z3) → c1(A(p(p(y0, y1), z1), z3), A(z2, z3)) 78.18/34.74
A(p(p(z0, z1), p(p(y0, y1), y2)), z3) → c1(A(p(z0, z1), z3), A(p(p(y0, y1), y2), z3)) 78.18/34.74
A(p(p(z0, p(y1, y2)), z2), z3) → c1(A(p(z0, p(y1, y2)), z3), A(z2, z3)) 78.18/34.74
A(p(p(z0, z1), p(y0, p(y1, y2))), z3) → c1(A(p(z0, z1), z3), A(p(y0, p(y1, y2)), z3)) 78.18/34.74
A(p(p(a(y0, y1), z1), z2), z3) → c1(A(p(a(y0, y1), z1), z3), A(z2, z3)) 78.18/34.74
A(p(p(z0, z1), p(a(y0, y1), y2)), z3) → c1(A(p(z0, z1), z3), A(p(a(y0, y1), y2), z3)) 78.18/34.74
A(p(p(z0, a(y1, y2)), z2), z3) → c1(A(p(z0, a(y1, y2)), z3), A(z2, z3)) 78.18/34.74
A(p(p(z0, z1), p(y0, a(y1, y2))), z3) → c1(A(p(z0, z1), z3), A(p(y0, a(y1, y2)), z3)) 78.18/34.74
A(p(lambda(y0), p(z1, z2)), z3) → c1(A(lambda(y0), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(a(y0, y1), p(z1, z2)), z3) → c1(A(a(y0, y1), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(p(lambda(y0), y1), p(z1, z2)), z3) → c1(A(p(lambda(y0), y1), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(lambda(y0), z2)), z3) → c1(A(z0, z3), A(p(lambda(y0), z2), z3)) 78.18/34.74
A(p(p(y0, lambda(y1)), p(z1, z2)), z3) → c1(A(p(y0, lambda(y1)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(z1, lambda(y1))), z3) → c1(A(z0, z3), A(p(z1, lambda(y1)), z3)) 78.18/34.74
A(p(p(y0, p(y1, y2)), p(z1, z2)), z3) → c1(A(p(y0, p(y1, y2)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(z1, p(y1, y2))), z3) → c1(A(z0, z3), A(p(z1, p(y1, y2)), z3)) 78.18/34.74
A(p(p(a(y0, y1), y2), p(z1, z2)), z3) → c1(A(p(a(y0, y1), y2), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(a(y0, y1), z2)), z3) → c1(A(z0, z3), A(p(a(y0, y1), z2), z3)) 78.18/34.74
A(p(p(y0, a(y1, y2)), p(z1, z2)), z3) → c1(A(p(y0, a(y1, y2)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(z1, a(y1, y2))), z3) → c1(A(z0, z3), A(p(z1, a(y1, y2)), z3)) 78.18/34.74
A(p(p(p(y0, y1), lambda(y2)), p(z1, z2)), z3) → c1(A(p(p(y0, y1), lambda(y2)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), lambda(y2))), z3) → c1(A(z0, z3), A(p(p(y0, y1), lambda(y2)), z3)) 78.18/34.74
A(p(p(p(y0, y1), a(y2, y3)), p(z1, z2)), z3) → c1(A(p(p(y0, y1), a(y2, y3)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), a(y2, y3))), z3) → c1(A(z0, z3), A(p(p(y0, y1), a(y2, y3)), z3)) 78.18/34.74
A(p(p(p(lambda(y0), y1), y2), p(z1, z2)), z3) → c1(A(p(p(lambda(y0), y1), y2), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(lambda(y0), y1), z2)), z3) → c1(A(z0, z3), A(p(p(lambda(y0), y1), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(lambda(y2), y3)), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(lambda(y2), y3)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(lambda(y2), y3))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(lambda(y2), y3)), z3)) 78.18/34.74
A(p(p(p(y0, lambda(y1)), y2), p(z1, z2)), z3) → c1(A(p(p(y0, lambda(y1)), y2), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, lambda(y1)), z2)), z3) → c1(A(z0, z3), A(p(p(y0, lambda(y1)), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(y2, lambda(y3))), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(y2, lambda(y3))), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(y2, lambda(y3)))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(y2, lambda(y3))), z3)) 78.18/34.74
A(p(p(p(p(y0, y1), y2), y3), p(z1, z2)), z3) → c1(A(p(p(p(y0, y1), y2), y3), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(p(y0, y1), y2), z2)), z3) → c1(A(z0, z3), A(p(p(p(y0, y1), y2), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(p(y2, y3), y4)), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(p(y2, y3), y4)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(p(y2, y3), y4))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(p(y2, y3), y4)), z3)) 78.18/34.74
A(p(p(p(y0, p(y1, y2)), y3), p(z1, z2)), z3) → c1(A(p(p(y0, p(y1, y2)), y3), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, p(y1, y2)), z2)), z3) → c1(A(z0, z3), A(p(p(y0, p(y1, y2)), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(y2, p(y3, y4))), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(y2, p(y3, y4))), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(y2, p(y3, y4)))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(y2, p(y3, y4))), z3)) 78.18/34.74
A(p(p(p(a(y0, y1), y2), y3), p(z1, z2)), z3) → c1(A(p(p(a(y0, y1), y2), y3), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(a(y0, y1), y2), z2)), z3) → c1(A(z0, z3), A(p(p(a(y0, y1), y2), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(a(y2, y3), y4)), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(a(y2, y3), y4)), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(a(y2, y3), y4))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(a(y2, y3), y4)), z3)) 78.18/34.74
A(p(p(p(y0, a(y1, y2)), y3), p(z1, z2)), z3) → c1(A(p(p(y0, a(y1, y2)), y3), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, a(y1, y2)), z2)), z3) → c1(A(z0, z3), A(p(p(y0, a(y1, y2)), z2), z3)) 78.18/34.74
A(p(p(p(y0, y1), p(y2, a(y3, y4))), p(z1, z2)), z3) → c1(A(p(p(y0, y1), p(y2, a(y3, y4))), z3), A(p(z1, z2), z3)) 78.18/34.74
A(p(z0, p(p(y0, y1), p(y2, a(y3, y4)))), z3) → c1(A(z0, z3), A(p(p(y0, y1), p(y2, a(y3, y4))), z3))

K tuples:none
Defined Rule Symbols:

a

Defined Pair Symbols:

A

Compound Symbols:

c, c2, c1

78.18/34.74