(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
active(__(__(X, Y), Z)) → mark(__(X, __(Y, Z)))
active(__(X, nil)) → mark(X)
active(__(nil, X)) → mark(X)
active(and(tt, X)) → mark(X)
active(isList(V)) → mark(isNeList(V))
active(isList(nil)) → mark(tt)
active(isList(__(V1, V2))) → mark(and(isList(V1), isList(V2)))
active(isNeList(V)) → mark(isQid(V))
active(isNeList(__(V1, V2))) → mark(and(isList(V1), isNeList(V2)))
active(isNeList(__(V1, V2))) → mark(and(isNeList(V1), isList(V2)))
active(isNePal(V)) → mark(isQid(V))
active(isNePal(__(I, __(P, I)))) → mark(and(isQid(I), isPal(P)))
active(isPal(V)) → mark(isNePal(V))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(X1, X2)) → active(__(mark(X1), mark(X2)))
mark(nil) → active(nil)
mark(and(X1, X2)) → active(and(mark(X1), X2))
mark(tt) → active(tt)
mark(isList(X)) → active(isList(X))
mark(isNeList(X)) → active(isNeList(X))
mark(isQid(X)) → active(isQid(X))
mark(isNePal(X)) → active(isNePal(X))
mark(isPal(X)) → active(isPal(X))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(X1), X2) → __(X1, X2)
__(X1, mark(X2)) → __(X1, X2)
__(active(X1), X2) → __(X1, X2)
__(X1, active(X2)) → __(X1, X2)
and(mark(X1), X2) → and(X1, X2)
and(X1, mark(X2)) → and(X1, X2)
and(active(X1), X2) → and(X1, X2)
and(X1, active(X2)) → and(X1, X2)
isList(mark(X)) → isList(X)
isList(active(X)) → isList(X)
isNeList(mark(X)) → isNeList(X)
isNeList(active(X)) → isNeList(X)
isQid(mark(X)) → isQid(X)
isQid(active(X)) → isQid(X)
isNePal(mark(X)) → isNePal(X)
isNePal(active(X)) → isNePal(X)
isPal(mark(X)) → isPal(X)
isPal(active(X)) → isPal(X)
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(and(tt, z0)) → mark(z0)
active(isList(z0)) → mark(isNeList(z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(and(isList(z0), isList(z1)))
active(isNeList(z0)) → mark(isQid(z0))
active(isNeList(__(z0, z1))) → mark(and(isList(z0), isNeList(z1)))
active(isNeList(__(z0, z1))) → mark(and(isNeList(z0), isList(z1)))
active(isNePal(z0)) → mark(isQid(z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(and(isQid(z0), isPal(z1)))
active(isPal(z0)) → mark(isNePal(z0))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(isList(z0)) → active(isList(z0))
mark(isNeList(z0)) → active(isNeList(z0))
mark(isQid(z0)) → active(isQid(z0))
mark(isNePal(z0)) → active(isNePal(z0))
mark(isPal(z0)) → active(isPal(z0))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)
Tuples:
ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isList(nil)) → c5(MARK(tt))
ACTIVE(isList(__(z0, z1))) → c6(MARK(and(isList(z0), isList(z1))), AND(isList(z0), isList(z1)), ISLIST(z0), ISLIST(z1))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNeList(__(z0, z1))) → c8(MARK(and(isList(z0), isNeList(z1))), AND(isList(z0), isNeList(z1)), ISLIST(z0), ISNELIST(z1))
ACTIVE(isNeList(__(z0, z1))) → c9(MARK(and(isNeList(z0), isList(z1))), AND(isNeList(z0), isList(z1)), ISNELIST(z0), ISLIST(z1))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c11(MARK(and(isQid(z0), isPal(z1))), AND(isQid(z0), isPal(z1)), ISQID(z0), ISPAL(z1))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
ACTIVE(isPal(nil)) → c13(MARK(tt))
ACTIVE(isQid(a)) → c14(MARK(tt))
ACTIVE(isQid(e)) → c15(MARK(tt))
ACTIVE(isQid(i)) → c16(MARK(tt))
ACTIVE(isQid(o)) → c17(MARK(tt))
ACTIVE(isQid(u)) → c18(MARK(tt))
MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(nil) → c20(ACTIVE(nil))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(tt) → c22(ACTIVE(tt))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
MARK(a) → c28(ACTIVE(a))
MARK(e) → c29(ACTIVE(e))
MARK(i) → c30(ACTIVE(i))
MARK(o) → c31(ACTIVE(o))
MARK(u) → c32(ACTIVE(u))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
S tuples:
ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isList(nil)) → c5(MARK(tt))
ACTIVE(isList(__(z0, z1))) → c6(MARK(and(isList(z0), isList(z1))), AND(isList(z0), isList(z1)), ISLIST(z0), ISLIST(z1))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNeList(__(z0, z1))) → c8(MARK(and(isList(z0), isNeList(z1))), AND(isList(z0), isNeList(z1)), ISLIST(z0), ISNELIST(z1))
ACTIVE(isNeList(__(z0, z1))) → c9(MARK(and(isNeList(z0), isList(z1))), AND(isNeList(z0), isList(z1)), ISNELIST(z0), ISLIST(z1))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c11(MARK(and(isQid(z0), isPal(z1))), AND(isQid(z0), isPal(z1)), ISQID(z0), ISPAL(z1))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
ACTIVE(isPal(nil)) → c13(MARK(tt))
ACTIVE(isQid(a)) → c14(MARK(tt))
ACTIVE(isQid(e)) → c15(MARK(tt))
ACTIVE(isQid(i)) → c16(MARK(tt))
ACTIVE(isQid(o)) → c17(MARK(tt))
ACTIVE(isQid(u)) → c18(MARK(tt))
MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(nil) → c20(ACTIVE(nil))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(tt) → c22(ACTIVE(tt))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
MARK(a) → c28(ACTIVE(a))
MARK(e) → c29(ACTIVE(e))
MARK(i) → c30(ACTIVE(i))
MARK(o) → c31(ACTIVE(o))
MARK(u) → c32(ACTIVE(u))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
K tuples:none
Defined Rule Symbols:
active, mark, __, and, isList, isNeList, isQid, isNePal, isPal
Defined Pair Symbols:
ACTIVE, MARK, __', AND, ISLIST, ISNELIST, ISQID, ISNEPAL, ISPAL
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
ACTIVE(__(__(z0, z1), z2)) → c(MARK(__(z0, __(z1, z2))), __'(z0, __(z1, z2)), __'(z1, z2))
ACTIVE(__(z0, nil)) → c1(MARK(z0))
ACTIVE(__(nil, z0)) → c2(MARK(z0))
ACTIVE(and(tt, z0)) → c3(MARK(z0))
ACTIVE(isList(z0)) → c4(MARK(isNeList(z0)), ISNELIST(z0))
ACTIVE(isList(nil)) → c5(MARK(tt))
ACTIVE(isList(__(z0, z1))) → c6(MARK(and(isList(z0), isList(z1))), AND(isList(z0), isList(z1)), ISLIST(z0), ISLIST(z1))
ACTIVE(isNeList(z0)) → c7(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNeList(__(z0, z1))) → c8(MARK(and(isList(z0), isNeList(z1))), AND(isList(z0), isNeList(z1)), ISLIST(z0), ISNELIST(z1))
ACTIVE(isNeList(__(z0, z1))) → c9(MARK(and(isNeList(z0), isList(z1))), AND(isNeList(z0), isList(z1)), ISNELIST(z0), ISLIST(z1))
ACTIVE(isNePal(z0)) → c10(MARK(isQid(z0)), ISQID(z0))
ACTIVE(isNePal(__(z0, __(z1, z0)))) → c11(MARK(and(isQid(z0), isPal(z1))), AND(isQid(z0), isPal(z1)), ISQID(z0), ISPAL(z1))
ACTIVE(isPal(z0)) → c12(MARK(isNePal(z0)), ISNEPAL(z0))
ACTIVE(isPal(nil)) → c13(MARK(tt))
ACTIVE(isQid(a)) → c14(MARK(tt))
ACTIVE(isQid(e)) → c15(MARK(tt))
ACTIVE(isQid(i)) → c16(MARK(tt))
ACTIVE(isQid(o)) → c17(MARK(tt))
ACTIVE(isQid(u)) → c18(MARK(tt))
MARK(__(z0, z1)) → c19(ACTIVE(__(mark(z0), mark(z1))), __'(mark(z0), mark(z1)), MARK(z0), MARK(z1))
MARK(and(z0, z1)) → c21(ACTIVE(and(mark(z0), z1)), AND(mark(z0), z1), MARK(z0))
MARK(isList(z0)) → c23(ACTIVE(isList(z0)), ISLIST(z0))
MARK(isNeList(z0)) → c24(ACTIVE(isNeList(z0)), ISNELIST(z0))
MARK(isQid(z0)) → c25(ACTIVE(isQid(z0)), ISQID(z0))
MARK(isNePal(z0)) → c26(ACTIVE(isNePal(z0)), ISNEPAL(z0))
MARK(isPal(z0)) → c27(ACTIVE(isPal(z0)), ISPAL(z0))
__'(mark(z0), z1) → c33(__'(z0, z1))
__'(z0, mark(z1)) → c34(__'(z0, z1))
__'(active(z0), z1) → c35(__'(z0, z1))
__'(z0, active(z1)) → c36(__'(z0, z1))
AND(mark(z0), z1) → c37(AND(z0, z1))
AND(z0, mark(z1)) → c38(AND(z0, z1))
AND(active(z0), z1) → c39(AND(z0, z1))
AND(z0, active(z1)) → c40(AND(z0, z1))
ISLIST(mark(z0)) → c41(ISLIST(z0))
ISLIST(active(z0)) → c42(ISLIST(z0))
ISNELIST(mark(z0)) → c43(ISNELIST(z0))
ISNELIST(active(z0)) → c44(ISNELIST(z0))
ISQID(mark(z0)) → c45(ISQID(z0))
ISQID(active(z0)) → c46(ISQID(z0))
ISNEPAL(mark(z0)) → c47(ISNEPAL(z0))
ISNEPAL(active(z0)) → c48(ISNEPAL(z0))
ISPAL(mark(z0)) → c49(ISPAL(z0))
ISPAL(active(z0)) → c50(ISPAL(z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(and(tt, z0)) → mark(z0)
active(isList(z0)) → mark(isNeList(z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(and(isList(z0), isList(z1)))
active(isNeList(z0)) → mark(isQid(z0))
active(isNeList(__(z0, z1))) → mark(and(isList(z0), isNeList(z1)))
active(isNeList(__(z0, z1))) → mark(and(isNeList(z0), isList(z1)))
active(isNePal(z0)) → mark(isQid(z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(and(isQid(z0), isPal(z1)))
active(isPal(z0)) → mark(isNePal(z0))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(isList(z0)) → active(isList(z0))
mark(isNeList(z0)) → active(isNeList(z0))
mark(isQid(z0)) → active(isQid(z0))
mark(isNePal(z0)) → active(isNePal(z0))
mark(isPal(z0)) → active(isPal(z0))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)
Tuples:
MARK(nil) → c20(ACTIVE(nil))
MARK(tt) → c22(ACTIVE(tt))
MARK(a) → c28(ACTIVE(a))
MARK(e) → c29(ACTIVE(e))
MARK(i) → c30(ACTIVE(i))
MARK(o) → c31(ACTIVE(o))
MARK(u) → c32(ACTIVE(u))
S tuples:
MARK(nil) → c20(ACTIVE(nil))
MARK(tt) → c22(ACTIVE(tt))
MARK(a) → c28(ACTIVE(a))
MARK(e) → c29(ACTIVE(e))
MARK(i) → c30(ACTIVE(i))
MARK(o) → c31(ACTIVE(o))
MARK(u) → c32(ACTIVE(u))
K tuples:none
Defined Rule Symbols:
active, mark, __, and, isList, isNeList, isQid, isNePal, isPal
Defined Pair Symbols:
MARK
Compound Symbols:
c20, c22, c28, c29, c30, c31, c32
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 7 trailing nodes:
MARK(o) → c31(ACTIVE(o))
MARK(u) → c32(ACTIVE(u))
MARK(tt) → c22(ACTIVE(tt))
MARK(a) → c28(ACTIVE(a))
MARK(i) → c30(ACTIVE(i))
MARK(nil) → c20(ACTIVE(nil))
MARK(e) → c29(ACTIVE(e))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
active(__(__(z0, z1), z2)) → mark(__(z0, __(z1, z2)))
active(__(z0, nil)) → mark(z0)
active(__(nil, z0)) → mark(z0)
active(and(tt, z0)) → mark(z0)
active(isList(z0)) → mark(isNeList(z0))
active(isList(nil)) → mark(tt)
active(isList(__(z0, z1))) → mark(and(isList(z0), isList(z1)))
active(isNeList(z0)) → mark(isQid(z0))
active(isNeList(__(z0, z1))) → mark(and(isList(z0), isNeList(z1)))
active(isNeList(__(z0, z1))) → mark(and(isNeList(z0), isList(z1)))
active(isNePal(z0)) → mark(isQid(z0))
active(isNePal(__(z0, __(z1, z0)))) → mark(and(isQid(z0), isPal(z1)))
active(isPal(z0)) → mark(isNePal(z0))
active(isPal(nil)) → mark(tt)
active(isQid(a)) → mark(tt)
active(isQid(e)) → mark(tt)
active(isQid(i)) → mark(tt)
active(isQid(o)) → mark(tt)
active(isQid(u)) → mark(tt)
mark(__(z0, z1)) → active(__(mark(z0), mark(z1)))
mark(nil) → active(nil)
mark(and(z0, z1)) → active(and(mark(z0), z1))
mark(tt) → active(tt)
mark(isList(z0)) → active(isList(z0))
mark(isNeList(z0)) → active(isNeList(z0))
mark(isQid(z0)) → active(isQid(z0))
mark(isNePal(z0)) → active(isNePal(z0))
mark(isPal(z0)) → active(isPal(z0))
mark(a) → active(a)
mark(e) → active(e)
mark(i) → active(i)
mark(o) → active(o)
mark(u) → active(u)
__(mark(z0), z1) → __(z0, z1)
__(z0, mark(z1)) → __(z0, z1)
__(active(z0), z1) → __(z0, z1)
__(z0, active(z1)) → __(z0, z1)
and(mark(z0), z1) → and(z0, z1)
and(z0, mark(z1)) → and(z0, z1)
and(active(z0), z1) → and(z0, z1)
and(z0, active(z1)) → and(z0, z1)
isList(mark(z0)) → isList(z0)
isList(active(z0)) → isList(z0)
isNeList(mark(z0)) → isNeList(z0)
isNeList(active(z0)) → isNeList(z0)
isQid(mark(z0)) → isQid(z0)
isQid(active(z0)) → isQid(z0)
isNePal(mark(z0)) → isNePal(z0)
isNePal(active(z0)) → isNePal(z0)
isPal(mark(z0)) → isPal(z0)
isPal(active(z0)) → isPal(z0)
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
active, mark, __, and, isList, isNeList, isQid, isNePal, isPal
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))