YES(O(1), O(n^1)) 2.40/1.10 YES(O(1), O(n^1)) 2.84/1.16 2.84/1.16 2.84/1.16 2.84/1.16 2.84/1.16 2.84/1.16 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 2.84/1.16 2.84/1.16 2.84/1.16
2.84/1.16
2.84/1.16
2.84/1.16
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxRelTRS
2.84/1.16 
↳1 CpxRelTrsToCDT (UPPER BOUND (ID))
2.84/1.16 
↳2 CdtProblem
2.84/1.16 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
2.84/1.16 
↳4 CdtProblem
2.84/1.16 
↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication)
2.84/1.16 
↳6 CdtProblem
2.84/1.16 
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
2.84/1.16 
↳8 CdtProblem
2.84/1.16 
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))
2.84/1.16 
↳10 CdtProblem
2.84/1.16 
↳11 SIsEmptyProof (BOTH BOUNDS(ID, ID))
2.84/1.16 
↳12 BOUNDS(O(1), O(1))
2.84/1.16
2.84/1.16 2.84/1.16
2.84/1.16
2.84/1.16

(0) Obligation:

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

subst(x, a, App(e1, e2)) → mkapp(subst(x, a, e1), subst(x, a, e2)) 2.84/1.16
subst(x, a, Lam(var, exp)) → subst[Ite][False][Ite][True][Ite](eqTerm(x, V(var)), x, a, Lam(var, exp)) 2.84/1.16
red(App(e1, e2)) → red[Ite][False][Ite][False][Let](App(e1, e2), red(e1)) 2.84/1.16
red(Lam(int, term)) → Lam(int, term) 2.84/1.16
subst(x, a, V(int)) → subst[Ite][True][Ite](eqTerm(x, V(int)), x, a, V(int)) 2.84/1.16
red(V(int)) → V(int) 2.84/1.16
eqTerm(App(t11, t12), App(t21, t22)) → and(eqTerm(t11, t21), eqTerm(t12, t22)) 2.84/1.16
eqTerm(App(t11, t12), Lam(i2, l2)) → False 2.84/1.16
eqTerm(App(t11, t12), V(v2)) → False 2.84/1.16
eqTerm(Lam(i1, l1), App(t21, t22)) → False 2.84/1.16
eqTerm(Lam(i1, l1), Lam(i2, l2)) → and(!EQ(i1, i2), eqTerm(l1, l2)) 2.84/1.16
eqTerm(Lam(i1, l1), V(v2)) → False 2.84/1.16
eqTerm(V(v1), App(t21, t22)) → False 2.84/1.16
eqTerm(V(v1), Lam(i2, l2)) → False 2.84/1.16
eqTerm(V(v1), V(v2)) → !EQ(v1, v2) 2.84/1.16
mklam(V(name), e) → Lam(name, e) 2.84/1.16
lamvar(Lam(var, exp)) → V(var) 2.84/1.16
lambody(Lam(var, exp)) → exp 2.84/1.16
isvar(App(t1, t2)) → False 2.84/1.16
isvar(Lam(int, term)) → False 2.84/1.16
isvar(V(int)) → True 2.84/1.16
islam(App(t1, t2)) → False 2.84/1.16
islam(Lam(int, term)) → True 2.84/1.16
islam(V(int)) → False 2.84/1.16
appe2(App(e1, e2)) → e2 2.84/1.16
appe1(App(e1, e2)) → e1 2.84/1.16
mkapp(e1, e2) → App(e1, e2) 2.84/1.16
lambdaint(e) → red(e)

The (relative) TRS S consists of the following rules:

and(False, False) → False 2.84/1.16
and(True, False) → False 2.84/1.16
and(False, True) → False 2.84/1.16
and(True, True) → True 2.84/1.16
!EQ(S(x), S(y)) → !EQ(x, y) 2.84/1.16
!EQ(0, S(y)) → False 2.84/1.16
!EQ(S(x), 0) → False 2.84/1.16
!EQ(0, 0) → True 2.84/1.16
subst[Ite][True][Ite](False, x, a, e) → e 2.84/1.16
subst[Ite][True][Ite](True, x, a, e) → a

Rewrite Strategy: INNERMOST
2.84/1.16
2.84/1.16

(1) CpxRelTrsToCDT (UPPER BOUND (ID) transformation)

Relative innermost TRS to CDT Problem.
2.84/1.16
2.84/1.16

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 2.84/1.16
and(True, False) → False 2.84/1.16
and(False, True) → False 2.84/1.16
and(True, True) → True 2.84/1.16
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 2.84/1.16
!EQ(0, S(z0)) → False 2.84/1.16
!EQ(S(z0), 0) → False 2.84/1.16
!EQ(0, 0) → True 2.84/1.16
subst[Ite][True][Ite](False, z0, z1, z2) → z2 2.84/1.16
subst[Ite][True][Ite](True, z0, z1, z2) → z1 2.84/1.16
subst(z0, z1, App(z2, z3)) → mkapp(subst(z0, z1, z2), subst(z0, z1, z3)) 2.84/1.16
subst(z0, z1, Lam(z2, z3)) → subst[Ite][False][Ite][True][Ite](eqTerm(z0, V(z2)), z0, z1, Lam(z2, z3)) 2.84/1.16
subst(z0, z1, V(z2)) → subst[Ite][True][Ite](eqTerm(z0, V(z2)), z0, z1, V(z2)) 2.84/1.16
red(App(z0, z1)) → red[Ite][False][Ite][False][Let](App(z0, z1), red(z0)) 2.84/1.16
red(Lam(z0, z1)) → Lam(z0, z1) 2.84/1.16
red(V(z0)) → V(z0) 2.84/1.16
eqTerm(App(z0, z1), App(z2, z3)) → and(eqTerm(z0, z2), eqTerm(z1, z3)) 2.84/1.16
eqTerm(App(z0, z1), Lam(z2, z3)) → False 2.84/1.16
eqTerm(App(z0, z1), V(z2)) → False 2.84/1.16
eqTerm(Lam(z0, z1), App(z2, z3)) → False 2.84/1.16
eqTerm(Lam(z0, z1), Lam(z2, z3)) → and(!EQ(z0, z2), eqTerm(z1, z3)) 2.84/1.16
eqTerm(Lam(z0, z1), V(z2)) → False 2.84/1.16
eqTerm(V(z0), App(z1, z2)) → False 2.84/1.16
eqTerm(V(z0), Lam(z1, z2)) → False 2.84/1.16
eqTerm(V(z0), V(z1)) → !EQ(z0, z1) 2.84/1.16
mklam(V(z0), z1) → Lam(z0, z1) 2.84/1.16
lamvar(Lam(z0, z1)) → V(z0) 2.84/1.16
lambody(Lam(z0, z1)) → z1 2.84/1.16
isvar(App(z0, z1)) → False 2.84/1.16
isvar(Lam(z0, z1)) → False 2.84/1.16
isvar(V(z0)) → True 2.84/1.16
islam(App(z0, z1)) → False 2.84/1.16
islam(Lam(z0, z1)) → True 2.84/1.16
islam(V(z0)) → False 2.84/1.16
appe2(App(z0, z1)) → z1 2.84/1.16
appe1(App(z0, z1)) → z0 2.84/1.16
mkapp(z0, z1) → App(z0, z1) 2.84/1.16
lambdaint(z0) → red(z0)
Tuples:

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1)) 2.84/1.16
SUBST(z0, z1, App(z2, z3)) → c10(MKAPP(subst(z0, z1, z2), subst(z0, z1, z3)), SUBST(z0, z1, z2), SUBST(z0, z1, z3)) 2.84/1.16
SUBST(z0, z1, Lam(z2, z3)) → c11(EQTERM(z0, V(z2))) 2.84/1.16
SUBST(z0, z1, V(z2)) → c12(SUBST[ITE][TRUE][ITE](eqTerm(z0, V(z2)), z0, z1, V(z2)), EQTERM(z0, V(z2))) 2.84/1.16
RED(App(z0, z1)) → c13(RED(z0)) 2.84/1.16
EQTERM(App(z0, z1), App(z2, z3)) → c16(AND(eqTerm(z0, z2), eqTerm(z1, z3)), EQTERM(z0, z2), EQTERM(z1, z3)) 2.84/1.16
EQTERM(Lam(z0, z1), Lam(z2, z3)) → c20(AND(!EQ(z0, z2), eqTerm(z1, z3)), !EQ'(z0, z2), EQTERM(z1, z3)) 2.84/1.16
EQTERM(V(z0), V(z1)) → c24(!EQ'(z0, z1)) 2.84/1.16
LAMBDAINT(z0) → c37(RED(z0))
S tuples:

SUBST(z0, z1, App(z2, z3)) → c10(MKAPP(subst(z0, z1, z2), subst(z0, z1, z3)), SUBST(z0, z1, z2), SUBST(z0, z1, z3)) 2.84/1.16
SUBST(z0, z1, Lam(z2, z3)) → c11(EQTERM(z0, V(z2))) 2.84/1.16
SUBST(z0, z1, V(z2)) → c12(SUBST[ITE][TRUE][ITE](eqTerm(z0, V(z2)), z0, z1, V(z2)), EQTERM(z0, V(z2))) 2.84/1.16
RED(App(z0, z1)) → c13(RED(z0)) 2.84/1.16
EQTERM(App(z0, z1), App(z2, z3)) → c16(AND(eqTerm(z0, z2), eqTerm(z1, z3)), EQTERM(z0, z2), EQTERM(z1, z3)) 2.84/1.16
EQTERM(Lam(z0, z1), Lam(z2, z3)) → c20(AND(!EQ(z0, z2), eqTerm(z1, z3)), !EQ'(z0, z2), EQTERM(z1, z3)) 2.84/1.16
EQTERM(V(z0), V(z1)) → c24(!EQ'(z0, z1)) 2.84/1.16
LAMBDAINT(z0) → c37(RED(z0))
K tuples:none
Defined Rule Symbols:

subst, red, eqTerm, mklam, lamvar, lambody, isvar, islam, appe2, appe1, mkapp, lambdaint, and, !EQ, subst[Ite][True][Ite]

Defined Pair Symbols:

!EQ', SUBST, RED, EQTERM, LAMBDAINT

Compound Symbols:

c4, c10, c11, c12, c13, c16, c20, c24, c37

2.84/1.16
2.84/1.16

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

Removed 4 trailing tuple parts
2.84/1.16
2.84/1.16

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 2.84/1.16
and(True, False) → False 2.84/1.16
and(False, True) → False 2.84/1.16
and(True, True) → True 2.84/1.16
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 2.84/1.16
!EQ(0, S(z0)) → False 2.84/1.16
!EQ(S(z0), 0) → False 2.84/1.16
!EQ(0, 0) → True 2.84/1.16
subst[Ite][True][Ite](False, z0, z1, z2) → z2 2.84/1.16
subst[Ite][True][Ite](True, z0, z1, z2) → z1 2.84/1.16
subst(z0, z1, App(z2, z3)) → mkapp(subst(z0, z1, z2), subst(z0, z1, z3)) 2.84/1.16
subst(z0, z1, Lam(z2, z3)) → subst[Ite][False][Ite][True][Ite](eqTerm(z0, V(z2)), z0, z1, Lam(z2, z3)) 2.84/1.16
subst(z0, z1, V(z2)) → subst[Ite][True][Ite](eqTerm(z0, V(z2)), z0, z1, V(z2)) 2.84/1.16
red(App(z0, z1)) → red[Ite][False][Ite][False][Let](App(z0, z1), red(z0)) 2.84/1.16
red(Lam(z0, z1)) → Lam(z0, z1) 2.84/1.16
red(V(z0)) → V(z0) 2.84/1.16
eqTerm(App(z0, z1), App(z2, z3)) → and(eqTerm(z0, z2), eqTerm(z1, z3)) 2.84/1.16
eqTerm(App(z0, z1), Lam(z2, z3)) → False 2.84/1.16
eqTerm(App(z0, z1), V(z2)) → False 2.84/1.16
eqTerm(Lam(z0, z1), App(z2, z3)) → False 2.84/1.16
eqTerm(Lam(z0, z1), Lam(z2, z3)) → and(!EQ(z0, z2), eqTerm(z1, z3)) 2.84/1.16
eqTerm(Lam(z0, z1), V(z2)) → False 2.84/1.16
eqTerm(V(z0), App(z1, z2)) → False 2.84/1.16
eqTerm(V(z0), Lam(z1, z2)) → False 2.84/1.16
eqTerm(V(z0), V(z1)) → !EQ(z0, z1) 2.84/1.16
mklam(V(z0), z1) → Lam(z0, z1) 2.84/1.16
lamvar(Lam(z0, z1)) → V(z0) 2.84/1.16
lambody(Lam(z0, z1)) → z1 2.84/1.16
isvar(App(z0, z1)) → False 2.84/1.16
isvar(Lam(z0, z1)) → False 2.84/1.16
isvar(V(z0)) → True 2.84/1.16
islam(App(z0, z1)) → False 2.84/1.16
islam(Lam(z0, z1)) → True 2.84/1.16
islam(V(z0)) → False 2.84/1.17
appe2(App(z0, z1)) → z1 2.84/1.17
appe1(App(z0, z1)) → z0 2.84/1.17
mkapp(z0, z1) → App(z0, z1) 2.84/1.17
lambdaint(z0) → red(z0)
Tuples:

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1)) 2.84/1.17
SUBST(z0, z1, Lam(z2, z3)) → c11(EQTERM(z0, V(z2))) 2.84/1.17
RED(App(z0, z1)) → c13(RED(z0)) 2.84/1.17
EQTERM(V(z0), V(z1)) → c24(!EQ'(z0, z1)) 2.84/1.17
LAMBDAINT(z0) → c37(RED(z0)) 2.84/1.17
SUBST(z0, z1, App(z2, z3)) → c10(SUBST(z0, z1, z2), SUBST(z0, z1, z3)) 2.84/1.17
SUBST(z0, z1, V(z2)) → c12(EQTERM(z0, V(z2))) 2.84/1.17
EQTERM(App(z0, z1), App(z2, z3)) → c16(EQTERM(z0, z2), EQTERM(z1, z3)) 2.84/1.17
EQTERM(Lam(z0, z1), Lam(z2, z3)) → c20(!EQ'(z0, z2), EQTERM(z1, z3))
S tuples:

SUBST(z0, z1, Lam(z2, z3)) → c11(EQTERM(z0, V(z2))) 2.84/1.17
RED(App(z0, z1)) → c13(RED(z0)) 2.84/1.17
EQTERM(V(z0), V(z1)) → c24(!EQ'(z0, z1)) 2.84/1.17
LAMBDAINT(z0) → c37(RED(z0)) 2.84/1.17
SUBST(z0, z1, App(z2, z3)) → c10(SUBST(z0, z1, z2), SUBST(z0, z1, z3)) 2.84/1.17
SUBST(z0, z1, V(z2)) → c12(EQTERM(z0, V(z2))) 2.84/1.17
EQTERM(App(z0, z1), App(z2, z3)) → c16(EQTERM(z0, z2), EQTERM(z1, z3)) 2.84/1.17
EQTERM(Lam(z0, z1), Lam(z2, z3)) → c20(!EQ'(z0, z2), EQTERM(z1, z3))
K tuples:none
Defined Rule Symbols:

subst, red, eqTerm, mklam, lamvar, lambody, isvar, islam, appe2, appe1, mkapp, lambdaint, and, !EQ, subst[Ite][True][Ite]

Defined Pair Symbols:

!EQ', SUBST, RED, EQTERM, LAMBDAINT

Compound Symbols:

c4, c11, c13, c24, c37, c10, c12, c16, c20

2.84/1.17
2.84/1.17

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

LAMBDAINT(z0) → c37(RED(z0))
2.84/1.17
2.84/1.17

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 2.84/1.17
and(True, False) → False 2.84/1.17
and(False, True) → False 2.84/1.17
and(True, True) → True 2.84/1.17
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 2.84/1.17
!EQ(0, S(z0)) → False 2.84/1.17
!EQ(S(z0), 0) → False 2.84/1.17
!EQ(0, 0) → True 2.84/1.17
subst[Ite][True][Ite](False, z0, z1, z2) → z2 2.84/1.17
subst[Ite][True][Ite](True, z0, z1, z2) → z1 2.84/1.17
subst(z0, z1, App(z2, z3)) → mkapp(subst(z0, z1, z2), subst(z0, z1, z3)) 2.84/1.17
subst(z0, z1, Lam(z2, z3)) → subst[Ite][False][Ite][True][Ite](eqTerm(z0, V(z2)), z0, z1, Lam(z2, z3)) 2.84/1.17
subst(z0, z1, V(z2)) → subst[Ite][True][Ite](eqTerm(z0, V(z2)), z0, z1, V(z2)) 2.84/1.17
red(App(z0, z1)) → red[Ite][False][Ite][False][Let](App(z0, z1), red(z0)) 2.84/1.17
red(Lam(z0, z1)) → Lam(z0, z1) 2.84/1.17
red(V(z0)) → V(z0) 2.84/1.17
eqTerm(App(z0, z1), App(z2, z3)) → and(eqTerm(z0, z2), eqTerm(z1, z3)) 2.84/1.17
eqTerm(App(z0, z1), Lam(z2, z3)) → False 2.84/1.17
eqTerm(App(z0, z1), V(z2)) → False 2.84/1.17
eqTerm(Lam(z0, z1), App(z2, z3)) → False 2.84/1.17
eqTerm(Lam(z0, z1), Lam(z2, z3)) → and(!EQ(z0, z2), eqTerm(z1, z3)) 2.84/1.17
eqTerm(Lam(z0, z1), V(z2)) → False 2.84/1.17
eqTerm(V(z0), App(z1, z2)) → False 2.84/1.17
eqTerm(V(z0), Lam(z1, z2)) → False 2.84/1.17
eqTerm(V(z0), V(z1)) → !EQ(z0, z1) 2.84/1.17
mklam(V(z0), z1) → Lam(z0, z1) 2.84/1.17
lamvar(Lam(z0, z1)) → V(z0) 2.84/1.17
lambody(Lam(z0, z1)) → z1 2.84/1.17
isvar(App(z0, z1)) → False 2.84/1.17
isvar(Lam(z0, z1)) → False 2.84/1.17
isvar(V(z0)) → True 2.84/1.17
islam(App(z0, z1)) → False 2.84/1.17
islam(Lam(z0, z1)) → True 2.84/1.17
islam(V(z0)) → False 2.84/1.17
appe2(App(z0, z1)) → z1 2.84/1.17
appe1(App(z0, z1)) → z0 2.84/1.17
mkapp(z0, z1) → App(z0, z1) 2.84/1.17
lambdaint(z0) → red(z0)
Tuples:

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1)) 2.84/1.17
SUBST(z0, z1, Lam(z2, z3)) → c11(EQTERM(z0, V(z2))) 2.84/1.17
RED(App(z0, z1)) → c13(RED(z0)) 2.84/1.17
EQTERM(V(z0), V(z1)) → c24(!EQ'(z0, z1)) 2.84/1.17
SUBST(z0, z1, App(z2, z3)) → c10(SUBST(z0, z1, z2), SUBST(z0, z1, z3)) 2.84/1.17
SUBST(z0, z1, V(z2)) → c12(EQTERM(z0, V(z2))) 2.84/1.17
EQTERM(App(z0, z1), App(z2, z3)) → c16(EQTERM(z0, z2), EQTERM(z1, z3)) 2.84/1.17
EQTERM(Lam(z0, z1), Lam(z2, z3)) → c20(!EQ'(z0, z2), EQTERM(z1, z3))
S tuples:

SUBST(z0, z1, Lam(z2, z3)) → c11(EQTERM(z0, V(z2))) 2.84/1.17
RED(App(z0, z1)) → c13(RED(z0)) 2.84/1.17
EQTERM(V(z0), V(z1)) → c24(!EQ'(z0, z1)) 2.84/1.17
SUBST(z0, z1, App(z2, z3)) → c10(SUBST(z0, z1, z2), SUBST(z0, z1, z3)) 2.84/1.17
SUBST(z0, z1, V(z2)) → c12(EQTERM(z0, V(z2))) 2.84/1.17
EQTERM(App(z0, z1), App(z2, z3)) → c16(EQTERM(z0, z2), EQTERM(z1, z3)) 2.84/1.17
EQTERM(Lam(z0, z1), Lam(z2, z3)) → c20(!EQ'(z0, z2), EQTERM(z1, z3))
K tuples:none
Defined Rule Symbols:

subst, red, eqTerm, mklam, lamvar, lambody, isvar, islam, appe2, appe1, mkapp, lambdaint, and, !EQ, subst[Ite][True][Ite]

Defined Pair Symbols:

!EQ', SUBST, RED, EQTERM

Compound Symbols:

c4, c11, c13, c24, c10, c12, c16, c20

2.84/1.17
2.84/1.17

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

SUBST(z0, z1, Lam(z2, z3)) → c11(EQTERM(z0, V(z2))) 2.84/1.17
RED(App(z0, z1)) → c13(RED(z0)) 2.84/1.17
EQTERM(V(z0), V(z1)) → c24(!EQ'(z0, z1)) 2.84/1.17
SUBST(z0, z1, V(z2)) → c12(EQTERM(z0, V(z2))) 2.84/1.17
EQTERM(App(z0, z1), App(z2, z3)) → c16(EQTERM(z0, z2), EQTERM(z1, z3)) 2.84/1.17
EQTERM(Lam(z0, z1), Lam(z2, z3)) → c20(!EQ'(z0, z2), EQTERM(z1, z3))
We considered the (Usable) Rules:none
And the Tuples:

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1)) 2.84/1.17
SUBST(z0, z1, Lam(z2, z3)) → c11(EQTERM(z0, V(z2))) 2.84/1.17
RED(App(z0, z1)) → c13(RED(z0)) 2.84/1.17
EQTERM(V(z0), V(z1)) → c24(!EQ'(z0, z1)) 2.84/1.17
SUBST(z0, z1, App(z2, z3)) → c10(SUBST(z0, z1, z2), SUBST(z0, z1, z3)) 2.84/1.17
SUBST(z0, z1, V(z2)) → c12(EQTERM(z0, V(z2))) 2.84/1.17
EQTERM(App(z0, z1), App(z2, z3)) → c16(EQTERM(z0, z2), EQTERM(z1, z3)) 2.84/1.17
EQTERM(Lam(z0, z1), Lam(z2, z3)) → c20(!EQ'(z0, z2), EQTERM(z1, z3))
The order we found is given by the following interpretation:
Polynomial interpretation : 2.84/1.17

POL(!EQ'(x1, x2)) = [2] + [2]x2    2.84/1.17
POL(App(x1, x2)) = [1] + x1 + x2    2.84/1.17
POL(EQTERM(x1, x2)) = [4]x2    2.84/1.17
POL(Lam(x1, x2)) = [3] + x1 + x2    2.84/1.17
POL(RED(x1)) = x1    2.84/1.17
POL(S(x1)) = x1    2.84/1.17
POL(SUBST(x1, x2, x3)) = [4] + [4]x3    2.84/1.17
POL(V(x1)) = [3] + x1    2.84/1.17
POL(c10(x1, x2)) = x1 + x2    2.84/1.17
POL(c11(x1)) = x1    2.84/1.17
POL(c12(x1)) = x1    2.84/1.17
POL(c13(x1)) = x1    2.84/1.17
POL(c16(x1, x2)) = x1 + x2    2.84/1.17
POL(c20(x1, x2)) = x1 + x2    2.84/1.17
POL(c24(x1)) = x1    2.84/1.17
POL(c4(x1)) = x1   
2.84/1.17
2.84/1.17

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 2.84/1.17
and(True, False) → False 2.84/1.17
and(False, True) → False 2.84/1.17
and(True, True) → True 2.84/1.17
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 2.84/1.17
!EQ(0, S(z0)) → False 2.84/1.17
!EQ(S(z0), 0) → False 2.84/1.17
!EQ(0, 0) → True 2.84/1.17
subst[Ite][True][Ite](False, z0, z1, z2) → z2 2.84/1.17
subst[Ite][True][Ite](True, z0, z1, z2) → z1 2.84/1.17
subst(z0, z1, App(z2, z3)) → mkapp(subst(z0, z1, z2), subst(z0, z1, z3)) 2.84/1.17
subst(z0, z1, Lam(z2, z3)) → subst[Ite][False][Ite][True][Ite](eqTerm(z0, V(z2)), z0, z1, Lam(z2, z3)) 2.84/1.17
subst(z0, z1, V(z2)) → subst[Ite][True][Ite](eqTerm(z0, V(z2)), z0, z1, V(z2)) 2.84/1.17
red(App(z0, z1)) → red[Ite][False][Ite][False][Let](App(z0, z1), red(z0)) 2.84/1.17
red(Lam(z0, z1)) → Lam(z0, z1) 2.84/1.17
red(V(z0)) → V(z0) 2.84/1.17
eqTerm(App(z0, z1), App(z2, z3)) → and(eqTerm(z0, z2), eqTerm(z1, z3)) 2.84/1.17
eqTerm(App(z0, z1), Lam(z2, z3)) → False 2.84/1.17
eqTerm(App(z0, z1), V(z2)) → False 2.84/1.17
eqTerm(Lam(z0, z1), App(z2, z3)) → False 2.84/1.17
eqTerm(Lam(z0, z1), Lam(z2, z3)) → and(!EQ(z0, z2), eqTerm(z1, z3)) 2.84/1.17
eqTerm(Lam(z0, z1), V(z2)) → False 2.84/1.17
eqTerm(V(z0), App(z1, z2)) → False 2.84/1.17
eqTerm(V(z0), Lam(z1, z2)) → False 2.84/1.17
eqTerm(V(z0), V(z1)) → !EQ(z0, z1) 2.84/1.17
mklam(V(z0), z1) → Lam(z0, z1) 2.84/1.17
lamvar(Lam(z0, z1)) → V(z0) 2.84/1.17
lambody(Lam(z0, z1)) → z1 2.84/1.17
isvar(App(z0, z1)) → False 2.84/1.17
isvar(Lam(z0, z1)) → False 2.84/1.17
isvar(V(z0)) → True 2.84/1.17
islam(App(z0, z1)) → False 2.84/1.17
islam(Lam(z0, z1)) → True 2.84/1.17
islam(V(z0)) → False 2.84/1.17
appe2(App(z0, z1)) → z1 2.84/1.17
appe1(App(z0, z1)) → z0 2.84/1.17
mkapp(z0, z1) → App(z0, z1) 2.84/1.17
lambdaint(z0) → red(z0)
Tuples:

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1)) 2.84/1.17
SUBST(z0, z1, Lam(z2, z3)) → c11(EQTERM(z0, V(z2))) 2.84/1.17
RED(App(z0, z1)) → c13(RED(z0)) 2.84/1.17
EQTERM(V(z0), V(z1)) → c24(!EQ'(z0, z1)) 2.84/1.17
SUBST(z0, z1, App(z2, z3)) → c10(SUBST(z0, z1, z2), SUBST(z0, z1, z3)) 2.84/1.17
SUBST(z0, z1, V(z2)) → c12(EQTERM(z0, V(z2))) 2.84/1.17
EQTERM(App(z0, z1), App(z2, z3)) → c16(EQTERM(z0, z2), EQTERM(z1, z3)) 2.84/1.17
EQTERM(Lam(z0, z1), Lam(z2, z3)) → c20(!EQ'(z0, z2), EQTERM(z1, z3))
S tuples:

SUBST(z0, z1, App(z2, z3)) → c10(SUBST(z0, z1, z2), SUBST(z0, z1, z3))
K tuples:

SUBST(z0, z1, Lam(z2, z3)) → c11(EQTERM(z0, V(z2))) 2.84/1.17
RED(App(z0, z1)) → c13(RED(z0)) 2.84/1.17
EQTERM(V(z0), V(z1)) → c24(!EQ'(z0, z1)) 2.84/1.17
SUBST(z0, z1, V(z2)) → c12(EQTERM(z0, V(z2))) 2.84/1.17
EQTERM(App(z0, z1), App(z2, z3)) → c16(EQTERM(z0, z2), EQTERM(z1, z3)) 2.84/1.17
EQTERM(Lam(z0, z1), Lam(z2, z3)) → c20(!EQ'(z0, z2), EQTERM(z1, z3))
Defined Rule Symbols:

subst, red, eqTerm, mklam, lamvar, lambody, isvar, islam, appe2, appe1, mkapp, lambdaint, and, !EQ, subst[Ite][True][Ite]

Defined Pair Symbols:

!EQ', SUBST, RED, EQTERM

Compound Symbols:

c4, c11, c13, c24, c10, c12, c16, c20

2.84/1.17
2.84/1.17

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

SUBST(z0, z1, App(z2, z3)) → c10(SUBST(z0, z1, z2), SUBST(z0, z1, z3))
We considered the (Usable) Rules:none
And the Tuples:

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1)) 2.84/1.17
SUBST(z0, z1, Lam(z2, z3)) → c11(EQTERM(z0, V(z2))) 2.84/1.17
RED(App(z0, z1)) → c13(RED(z0)) 2.84/1.17
EQTERM(V(z0), V(z1)) → c24(!EQ'(z0, z1)) 2.84/1.17
SUBST(z0, z1, App(z2, z3)) → c10(SUBST(z0, z1, z2), SUBST(z0, z1, z3)) 2.84/1.17
SUBST(z0, z1, V(z2)) → c12(EQTERM(z0, V(z2))) 2.84/1.17
EQTERM(App(z0, z1), App(z2, z3)) → c16(EQTERM(z0, z2), EQTERM(z1, z3)) 2.84/1.17
EQTERM(Lam(z0, z1), Lam(z2, z3)) → c20(!EQ'(z0, z2), EQTERM(z1, z3))
The order we found is given by the following interpretation:
Polynomial interpretation : 2.84/1.17

POL(!EQ'(x1, x2)) = [2]    2.84/1.17
POL(App(x1, x2)) = [1] + x1 + x2    2.84/1.17
POL(EQTERM(x1, x2)) = [2] + [4]x2    2.84/1.17
POL(Lam(x1, x2)) = [3] + x1 + x2    2.84/1.17
POL(RED(x1)) = [3]x1    2.84/1.17
POL(S(x1)) = x1    2.84/1.17
POL(SUBST(x1, x2, x3)) = [1] + [5]x3    2.84/1.17
POL(V(x1)) = [3]    2.84/1.17
POL(c10(x1, x2)) = x1 + x2    2.84/1.17
POL(c11(x1)) = x1    2.84/1.17
POL(c12(x1)) = x1    2.84/1.17
POL(c13(x1)) = x1    2.84/1.17
POL(c16(x1, x2)) = x1 + x2    2.84/1.17
POL(c20(x1, x2)) = x1 + x2    2.84/1.17
POL(c24(x1)) = x1    2.84/1.17
POL(c4(x1)) = x1   
2.84/1.17
2.84/1.17

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

and(False, False) → False 2.84/1.17
and(True, False) → False 2.84/1.17
and(False, True) → False 2.84/1.17
and(True, True) → True 2.84/1.17
!EQ(S(z0), S(z1)) → !EQ(z0, z1) 2.84/1.17
!EQ(0, S(z0)) → False 2.84/1.17
!EQ(S(z0), 0) → False 2.84/1.17
!EQ(0, 0) → True 2.84/1.17
subst[Ite][True][Ite](False, z0, z1, z2) → z2 2.84/1.17
subst[Ite][True][Ite](True, z0, z1, z2) → z1 2.84/1.17
subst(z0, z1, App(z2, z3)) → mkapp(subst(z0, z1, z2), subst(z0, z1, z3)) 2.84/1.17
subst(z0, z1, Lam(z2, z3)) → subst[Ite][False][Ite][True][Ite](eqTerm(z0, V(z2)), z0, z1, Lam(z2, z3)) 2.84/1.17
subst(z0, z1, V(z2)) → subst[Ite][True][Ite](eqTerm(z0, V(z2)), z0, z1, V(z2)) 2.84/1.17
red(App(z0, z1)) → red[Ite][False][Ite][False][Let](App(z0, z1), red(z0)) 2.84/1.17
red(Lam(z0, z1)) → Lam(z0, z1) 2.84/1.17
red(V(z0)) → V(z0) 2.84/1.17
eqTerm(App(z0, z1), App(z2, z3)) → and(eqTerm(z0, z2), eqTerm(z1, z3)) 2.84/1.17
eqTerm(App(z0, z1), Lam(z2, z3)) → False 2.84/1.17
eqTerm(App(z0, z1), V(z2)) → False 2.84/1.17
eqTerm(Lam(z0, z1), App(z2, z3)) → False 2.84/1.17
eqTerm(Lam(z0, z1), Lam(z2, z3)) → and(!EQ(z0, z2), eqTerm(z1, z3)) 2.84/1.17
eqTerm(Lam(z0, z1), V(z2)) → False 2.84/1.17
eqTerm(V(z0), App(z1, z2)) → False 2.84/1.17
eqTerm(V(z0), Lam(z1, z2)) → False 2.84/1.17
eqTerm(V(z0), V(z1)) → !EQ(z0, z1) 2.84/1.17
mklam(V(z0), z1) → Lam(z0, z1) 2.84/1.17
lamvar(Lam(z0, z1)) → V(z0) 2.84/1.17
lambody(Lam(z0, z1)) → z1 2.84/1.17
isvar(App(z0, z1)) → False 2.84/1.17
isvar(Lam(z0, z1)) → False 2.84/1.17
isvar(V(z0)) → True 2.84/1.17
islam(App(z0, z1)) → False 2.84/1.17
islam(Lam(z0, z1)) → True 2.84/1.17
islam(V(z0)) → False 2.84/1.17
appe2(App(z0, z1)) → z1 2.84/1.17
appe1(App(z0, z1)) → z0 2.84/1.17
mkapp(z0, z1) → App(z0, z1) 2.84/1.17
lambdaint(z0) → red(z0)
Tuples:

!EQ'(S(z0), S(z1)) → c4(!EQ'(z0, z1)) 2.84/1.17
SUBST(z0, z1, Lam(z2, z3)) → c11(EQTERM(z0, V(z2))) 2.84/1.17
RED(App(z0, z1)) → c13(RED(z0)) 2.84/1.17
EQTERM(V(z0), V(z1)) → c24(!EQ'(z0, z1)) 2.84/1.17
SUBST(z0, z1, App(z2, z3)) → c10(SUBST(z0, z1, z2), SUBST(z0, z1, z3)) 2.84/1.17
SUBST(z0, z1, V(z2)) → c12(EQTERM(z0, V(z2))) 2.84/1.17
EQTERM(App(z0, z1), App(z2, z3)) → c16(EQTERM(z0, z2), EQTERM(z1, z3)) 2.84/1.17
EQTERM(Lam(z0, z1), Lam(z2, z3)) → c20(!EQ'(z0, z2), EQTERM(z1, z3))
S tuples:none
K tuples:

SUBST(z0, z1, Lam(z2, z3)) → c11(EQTERM(z0, V(z2))) 2.84/1.17
RED(App(z0, z1)) → c13(RED(z0)) 2.84/1.17
EQTERM(V(z0), V(z1)) → c24(!EQ'(z0, z1)) 2.84/1.17
SUBST(z0, z1, V(z2)) → c12(EQTERM(z0, V(z2))) 2.84/1.17
EQTERM(App(z0, z1), App(z2, z3)) → c16(EQTERM(z0, z2), EQTERM(z1, z3)) 2.84/1.17
EQTERM(Lam(z0, z1), Lam(z2, z3)) → c20(!EQ'(z0, z2), EQTERM(z1, z3)) 2.84/1.17
SUBST(z0, z1, App(z2, z3)) → c10(SUBST(z0, z1, z2), SUBST(z0, z1, z3))
Defined Rule Symbols:

subst, red, eqTerm, mklam, lamvar, lambody, isvar, islam, appe2, appe1, mkapp, lambdaint, and, !EQ, subst[Ite][True][Ite]

Defined Pair Symbols:

!EQ', SUBST, RED, EQTERM

Compound Symbols:

c4, c11, c13, c24, c10, c12, c16, c20

2.84/1.17
2.84/1.17

(11) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty
2.84/1.17
2.84/1.17

(12) BOUNDS(O(1), O(1))

2.84/1.17
2.84/1.17
3.11/1.21 EOF