WORST_CASE(?,O(n^1)) proof of input_IZiDMPee7I.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 928 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (6) CdtProblem (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (10) CdtProblem (11) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CdtProblem (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 82 ms] (14) CdtProblem (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 54 ms] (16) CdtProblem (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 32 ms] (18) CdtProblem (19) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (20) BOUNDS(1, 1) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: head(Cons(x, xs)) -> x e(Cons(F, Nil), b) -> False e(Cons(T, Nil), b) -> False e(Cons(B, Nil), b) -> False e(Cons(A, Nil), b) -> e[Match][Cons][Ite][True][Match](A, Nil, b) e(Cons(F, Cons(x, xs)), b) -> False e(Cons(T, Cons(x, xs)), b) -> False e(Cons(B, Cons(x, xs)), b) -> False e(Cons(A, Cons(x, xs)), b) -> False equal(F, F) -> True equal(F, T) -> False equal(F, B) -> False equal(F, A) -> False equal(T, F) -> False equal(T, T) -> True equal(T, B) -> False equal(T, A) -> False equal(B, F) -> False equal(B, T) -> False equal(B, B) -> True equal(B, A) -> False equal(A, F) -> False equal(A, T) -> False equal(A, B) -> False equal(A, A) -> True notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False e(Nil, b) -> False t(x, y) -> t[Ite](e(x, y), x, y) r(x, y) -> r[Ite](e(x, y), x, y) q(x, y) -> q[Ite](e(x, y), x, y) p(x, y) -> p[Ite](e(x, y), x, y) goal(x, y) -> q(x, y) The (relative) TRS S consists of the following rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True q[Ite](False, x', Cons(F, Cons(F, xs))) -> q[Ite][False][Ite][True][Ite](and(p(x', Cons(F, Cons(F, xs))), q(x', Cons(F, xs))), x', Cons(F, Cons(F, xs))) q[Ite](False, x, Cons(F, Cons(T, xs))) -> False q[Ite](False, x, Cons(F, Cons(B, xs))) -> False q[Ite](False, x, Cons(F, Cons(A, xs))) -> False q[Ite](False, x, Cons(T, Cons(F, xs))) -> False q[Ite](False, x, Cons(T, Cons(T, xs))) -> False q[Ite](False, x, Cons(T, Cons(B, xs))) -> False q[Ite](False, x, Cons(T, Cons(A, xs))) -> False q[Ite](False, x, Cons(B, Cons(F, xs))) -> False q[Ite](False, x, Cons(B, Cons(T, xs))) -> False q[Ite](False, x, Cons(B, Cons(B, xs))) -> False q[Ite](False, x, Cons(B, Cons(A, xs))) -> False q[Ite](False, x, Cons(A, Cons(F, xs))) -> False q[Ite](False, x, Cons(A, Cons(T, xs))) -> False q[Ite](False, x, Cons(A, Cons(B, xs))) -> False q[Ite](False, x, Cons(A, Cons(A, xs))) -> False q[Ite](False, x', Cons(F, Nil)) -> q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), x', Cons(F, Nil)) q[Ite](False, x', Cons(T, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(T, Nil)) q[Ite](False, x', Cons(B, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(B, Nil)) q[Ite](False, x', Cons(A, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(A, Nil)) r[Ite](False, x', Cons(F, xs)) -> r[Ite][False][Ite][True][Ite](and(q(x', xs), r(x', xs)), x', Cons(F, xs)) r[Ite](False, x, Cons(T, xs)) -> False r[Ite](False, x, Cons(B, xs)) -> False r[Ite](False, x, Cons(A, xs)) -> False p[Ite](False, x', Cons(F, xs)) -> and(r(x', Cons(F, xs)), p(x', xs)) p[Ite](False, x, Cons(T, xs)) -> False p[Ite](False, x, Cons(B, xs)) -> False p[Ite](False, x, Cons(A, xs)) -> False q[Ite][False][Ite](True, x', Cons(x, xs)) -> q[Ite][False][Ite][True][Ite](and(p(x', Cons(x, xs)), q(x', xs)), x', Cons(x, xs)) t[Ite](False, x, y) -> True t[Ite](True, x, y) -> True r[Ite](True, x, y) -> True q[Ite](True, x, y) -> True q[Ite][False][Ite](False, x, y) -> False p[Ite](True, x, y) -> True Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: head(Cons(x, xs)) -> x e(Cons(F, Nil), b) -> False e(Cons(T, Nil), b) -> False e(Cons(B, Nil), b) -> False e(Cons(A, Nil), b) -> e[Match][Cons][Ite][True][Match](A, Nil, b) e(Cons(F, Cons(x, xs)), b) -> False e(Cons(T, Cons(x, xs)), b) -> False e(Cons(B, Cons(x, xs)), b) -> False e(Cons(A, Cons(x, xs)), b) -> False equal(F, F) -> True equal(F, T) -> False equal(F, B) -> False equal(F, A) -> False equal(T, F) -> False equal(T, T) -> True equal(T, B) -> False equal(T, A) -> False equal(B, F) -> False equal(B, T) -> False equal(B, B) -> True equal(B, A) -> False equal(A, F) -> False equal(A, T) -> False equal(A, B) -> False equal(A, A) -> True notEmpty(Cons(x, xs)) -> True notEmpty(Nil) -> False e(Nil, b) -> False t(x, y) -> t[Ite](e(x, y), x, y) r(x, y) -> r[Ite](e(x, y), x, y) q(x, y) -> q[Ite](e(x, y), x, y) p(x, y) -> p[Ite](e(x, y), x, y) goal(x, y) -> q(x, y) The (relative) TRS S consists of the following rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True q[Ite](False, x', Cons(F, Cons(F, xs))) -> q[Ite][False][Ite][True][Ite](and(p(x', Cons(F, Cons(F, xs))), q(x', Cons(F, xs))), x', Cons(F, Cons(F, xs))) q[Ite](False, x, Cons(F, Cons(T, xs))) -> False q[Ite](False, x, Cons(F, Cons(B, xs))) -> False q[Ite](False, x, Cons(F, Cons(A, xs))) -> False q[Ite](False, x, Cons(T, Cons(F, xs))) -> False q[Ite](False, x, Cons(T, Cons(T, xs))) -> False q[Ite](False, x, Cons(T, Cons(B, xs))) -> False q[Ite](False, x, Cons(T, Cons(A, xs))) -> False q[Ite](False, x, Cons(B, Cons(F, xs))) -> False q[Ite](False, x, Cons(B, Cons(T, xs))) -> False q[Ite](False, x, Cons(B, Cons(B, xs))) -> False q[Ite](False, x, Cons(B, Cons(A, xs))) -> False q[Ite](False, x, Cons(A, Cons(F, xs))) -> False q[Ite](False, x, Cons(A, Cons(T, xs))) -> False q[Ite](False, x, Cons(A, Cons(B, xs))) -> False q[Ite](False, x, Cons(A, Cons(A, xs))) -> False q[Ite](False, x', Cons(F, Nil)) -> q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), x', Cons(F, Nil)) q[Ite](False, x', Cons(T, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(T, Nil)) q[Ite](False, x', Cons(B, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(B, Nil)) q[Ite](False, x', Cons(A, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(A, Nil)) r[Ite](False, x', Cons(F, xs)) -> r[Ite][False][Ite][True][Ite](and(q(x', xs), r(x', xs)), x', Cons(F, xs)) r[Ite](False, x, Cons(T, xs)) -> False r[Ite](False, x, Cons(B, xs)) -> False r[Ite](False, x, Cons(A, xs)) -> False p[Ite](False, x', Cons(F, xs)) -> and(r(x', Cons(F, xs)), p(x', xs)) p[Ite](False, x, Cons(T, xs)) -> False p[Ite](False, x, Cons(B, xs)) -> False p[Ite](False, x, Cons(A, xs)) -> False q[Ite][False][Ite](True, x', Cons(x, xs)) -> q[Ite][False][Ite][True][Ite](and(p(x', Cons(x, xs)), q(x', xs)), x', Cons(x, xs)) t[Ite](False, x, y) -> True t[Ite](True, x, y) -> True r[Ite](True, x, y) -> True q[Ite](True, x, y) -> True q[Ite][False][Ite](False, x, y) -> False p[Ite](True, x, y) -> True Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True q[Ite](False, z0, Cons(F, Cons(F, z1))) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), z0, Cons(F, Cons(F, z1))) q[Ite](False, z0, Cons(F, Cons(T, z1))) -> False q[Ite](False, z0, Cons(F, Cons(B, z1))) -> False q[Ite](False, z0, Cons(F, Cons(A, z1))) -> False q[Ite](False, z0, Cons(T, Cons(F, z1))) -> False q[Ite](False, z0, Cons(T, Cons(T, z1))) -> False q[Ite](False, z0, Cons(T, Cons(B, z1))) -> False q[Ite](False, z0, Cons(T, Cons(A, z1))) -> False q[Ite](False, z0, Cons(B, Cons(F, z1))) -> False q[Ite](False, z0, Cons(B, Cons(T, z1))) -> False q[Ite](False, z0, Cons(B, Cons(B, z1))) -> False q[Ite](False, z0, Cons(B, Cons(A, z1))) -> False q[Ite](False, z0, Cons(A, Cons(F, z1))) -> False q[Ite](False, z0, Cons(A, Cons(T, z1))) -> False q[Ite](False, z0, Cons(A, Cons(B, z1))) -> False q[Ite](False, z0, Cons(A, Cons(A, z1))) -> False q[Ite](False, z0, Cons(F, Nil)) -> q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), z0, Cons(F, Nil)) q[Ite](False, z0, Cons(T, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(T, Nil)) q[Ite](False, z0, Cons(B, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(B, Nil)) q[Ite](False, z0, Cons(A, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(A, Nil)) q[Ite](True, z0, z1) -> True r[Ite](False, z0, Cons(F, z1)) -> r[Ite][False][Ite][True][Ite](and(q(z0, z1), r(z0, z1)), z0, Cons(F, z1)) r[Ite](False, z0, Cons(T, z1)) -> False r[Ite](False, z0, Cons(B, z1)) -> False r[Ite](False, z0, Cons(A, z1)) -> False r[Ite](True, z0, z1) -> True p[Ite](False, z0, Cons(F, z1)) -> and(r(z0, Cons(F, z1)), p(z0, z1)) p[Ite](False, z0, Cons(T, z1)) -> False p[Ite](False, z0, Cons(B, z1)) -> False p[Ite](False, z0, Cons(A, z1)) -> False p[Ite](True, z0, z1) -> True q[Ite][False][Ite](True, z0, Cons(z1, z2)) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(z1, z2)), q(z0, z2)), z0, Cons(z1, z2)) q[Ite][False][Ite](False, z0, z1) -> False t[Ite](False, z0, z1) -> True t[Ite](True, z0, z1) -> True head(Cons(z0, z1)) -> z0 e(Cons(F, Nil), z0) -> False e(Cons(T, Nil), z0) -> False e(Cons(B, Nil), z0) -> False e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0) e(Cons(F, Cons(z0, z1)), z2) -> False e(Cons(T, Cons(z0, z1)), z2) -> False e(Cons(B, Cons(z0, z1)), z2) -> False e(Cons(A, Cons(z0, z1)), z2) -> False e(Nil, z0) -> False equal(F, F) -> True equal(F, T) -> False equal(F, B) -> False equal(F, A) -> False equal(T, F) -> False equal(T, T) -> True equal(T, B) -> False equal(T, A) -> False equal(B, F) -> False equal(B, T) -> False equal(B, B) -> True equal(B, A) -> False equal(A, F) -> False equal(A, T) -> False equal(A, B) -> False equal(A, A) -> True notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False t(z0, z1) -> t[Ite](e(z0, z1), z0, z1) r(z0, z1) -> r[Ite](e(z0, z1), z0, z1) q(z0, z1) -> q[Ite](e(z0, z1), z0, z1) p(z0, z1) -> p[Ite](e(z0, z1), z0, z1) goal(z0, z1) -> q(z0, z1) Tuples: AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(AND(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), P(z0, Cons(F, Cons(F, z1)))) Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(AND(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), Q(z0, Cons(F, z1))) Q[ITE](False, z0, Cons(F, Cons(T, z1))) -> c6 Q[ITE](False, z0, Cons(F, Cons(B, z1))) -> c7 Q[ITE](False, z0, Cons(F, Cons(A, z1))) -> c8 Q[ITE](False, z0, Cons(T, Cons(F, z1))) -> c9 Q[ITE](False, z0, Cons(T, Cons(T, z1))) -> c10 Q[ITE](False, z0, Cons(T, Cons(B, z1))) -> c11 Q[ITE](False, z0, Cons(T, Cons(A, z1))) -> c12 Q[ITE](False, z0, Cons(B, Cons(F, z1))) -> c13 Q[ITE](False, z0, Cons(B, Cons(T, z1))) -> c14 Q[ITE](False, z0, Cons(B, Cons(B, z1))) -> c15 Q[ITE](False, z0, Cons(B, Cons(A, z1))) -> c16 Q[ITE](False, z0, Cons(A, Cons(F, z1))) -> c17 Q[ITE](False, z0, Cons(A, Cons(T, z1))) -> c18 Q[ITE](False, z0, Cons(A, Cons(B, z1))) -> c19 Q[ITE](False, z0, Cons(A, Cons(A, z1))) -> c20 Q[ITE](False, z0, Cons(F, Nil)) -> c21(Q[ITE][FALSE][ITE](and(True, and(True, and(False, equal(head(Nil), F)))), z0, Cons(F, Nil)), AND(True, and(True, and(False, equal(head(Nil), F)))), AND(True, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil)) Q[ITE](False, z0, Cons(T, Nil)) -> c22(Q[ITE][FALSE][ITE](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(T, Nil)), AND(True, and(False, and(False, equal(head(Nil), F)))), AND(False, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil)) Q[ITE](False, z0, Cons(B, Nil)) -> c23(Q[ITE][FALSE][ITE](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(B, Nil)), AND(True, and(False, and(False, equal(head(Nil), F)))), AND(False, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil)) Q[ITE](False, z0, Cons(A, Nil)) -> c24(Q[ITE][FALSE][ITE](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(A, Nil)), AND(True, and(False, and(False, equal(head(Nil), F)))), AND(False, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil)) Q[ITE](True, z0, z1) -> c25 R[ITE](False, z0, Cons(F, z1)) -> c26(AND(q(z0, z1), r(z0, z1)), Q(z0, z1)) R[ITE](False, z0, Cons(F, z1)) -> c27(AND(q(z0, z1), r(z0, z1)), R(z0, z1)) R[ITE](False, z0, Cons(T, z1)) -> c28 R[ITE](False, z0, Cons(B, z1)) -> c29 R[ITE](False, z0, Cons(A, z1)) -> c30 R[ITE](True, z0, z1) -> c31 P[ITE](False, z0, Cons(F, z1)) -> c32(AND(r(z0, Cons(F, z1)), p(z0, z1)), R(z0, Cons(F, z1))) P[ITE](False, z0, Cons(F, z1)) -> c33(AND(r(z0, Cons(F, z1)), p(z0, z1)), P(z0, z1)) P[ITE](False, z0, Cons(T, z1)) -> c34 P[ITE](False, z0, Cons(B, z1)) -> c35 P[ITE](False, z0, Cons(A, z1)) -> c36 P[ITE](True, z0, z1) -> c37 Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c38(AND(p(z0, Cons(z1, z2)), q(z0, z2)), P(z0, Cons(z1, z2))) Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c39(AND(p(z0, Cons(z1, z2)), q(z0, z2)), Q(z0, z2)) Q[ITE][FALSE][ITE](False, z0, z1) -> c40 T[ITE](False, z0, z1) -> c41 T[ITE](True, z0, z1) -> c42 HEAD(Cons(z0, z1)) -> c43 E(Cons(F, Nil), z0) -> c44 E(Cons(T, Nil), z0) -> c45 E(Cons(B, Nil), z0) -> c46 E(Cons(A, Nil), z0) -> c47 E(Cons(F, Cons(z0, z1)), z2) -> c48 E(Cons(T, Cons(z0, z1)), z2) -> c49 E(Cons(B, Cons(z0, z1)), z2) -> c50 E(Cons(A, Cons(z0, z1)), z2) -> c51 E(Nil, z0) -> c52 EQUAL(F, F) -> c53 EQUAL(F, T) -> c54 EQUAL(F, B) -> c55 EQUAL(F, A) -> c56 EQUAL(T, F) -> c57 EQUAL(T, T) -> c58 EQUAL(T, B) -> c59 EQUAL(T, A) -> c60 EQUAL(B, F) -> c61 EQUAL(B, T) -> c62 EQUAL(B, B) -> c63 EQUAL(B, A) -> c64 EQUAL(A, F) -> c65 EQUAL(A, T) -> c66 EQUAL(A, B) -> c67 EQUAL(A, A) -> c68 NOTEMPTY(Cons(z0, z1)) -> c69 NOTEMPTY(Nil) -> c70 T'(z0, z1) -> c71(T[ITE](e(z0, z1), z0, z1), E(z0, z1)) R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1), E(z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1), E(z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1), E(z0, z1)) GOAL(z0, z1) -> c75(Q(z0, z1)) S tuples: HEAD(Cons(z0, z1)) -> c43 E(Cons(F, Nil), z0) -> c44 E(Cons(T, Nil), z0) -> c45 E(Cons(B, Nil), z0) -> c46 E(Cons(A, Nil), z0) -> c47 E(Cons(F, Cons(z0, z1)), z2) -> c48 E(Cons(T, Cons(z0, z1)), z2) -> c49 E(Cons(B, Cons(z0, z1)), z2) -> c50 E(Cons(A, Cons(z0, z1)), z2) -> c51 E(Nil, z0) -> c52 EQUAL(F, F) -> c53 EQUAL(F, T) -> c54 EQUAL(F, B) -> c55 EQUAL(F, A) -> c56 EQUAL(T, F) -> c57 EQUAL(T, T) -> c58 EQUAL(T, B) -> c59 EQUAL(T, A) -> c60 EQUAL(B, F) -> c61 EQUAL(B, T) -> c62 EQUAL(B, B) -> c63 EQUAL(B, A) -> c64 EQUAL(A, F) -> c65 EQUAL(A, T) -> c66 EQUAL(A, B) -> c67 EQUAL(A, A) -> c68 NOTEMPTY(Cons(z0, z1)) -> c69 NOTEMPTY(Nil) -> c70 T'(z0, z1) -> c71(T[ITE](e(z0, z1), z0, z1), E(z0, z1)) R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1), E(z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1), E(z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1), E(z0, z1)) GOAL(z0, z1) -> c75(Q(z0, z1)) K tuples:none Defined Rule Symbols: head_1, e_2, equal_2, notEmpty_1, t_2, r_2, q_2, p_2, goal_2, and_2, q[Ite]_3, r[Ite]_3, p[Ite]_3, q[Ite][False][Ite]_3, t[Ite]_3 Defined Pair Symbols: AND_2, Q[ITE]_3, R[ITE]_3, P[ITE]_3, Q[ITE][FALSE][ITE]_3, T[ITE]_3, HEAD_1, E_2, EQUAL_2, NOTEMPTY_1, T'_2, R_2, Q_2, P_2, GOAL_2 Compound Symbols: c, c1, c2, c3, c4_2, c5_2, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21_6, c22_6, c23_6, c24_6, c25, c26_2, c27_2, c28, c29, c30, c31, c32_2, c33_2, c34, c35, c36, c37, c38_2, c39_2, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c67, c68, c69, c70, c71_2, c72_2, c73_2, c74_2, c75_1 ---------------------------------------- (5) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: GOAL(z0, z1) -> c75(Q(z0, z1)) Removed 64 trailing nodes: E(Cons(B, Cons(z0, z1)), z2) -> c50 EQUAL(F, A) -> c56 Q[ITE](False, z0, Cons(B, Nil)) -> c23(Q[ITE][FALSE][ITE](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(B, Nil)), AND(True, and(False, and(False, equal(head(Nil), F)))), AND(False, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil)) Q[ITE](False, z0, Cons(T, Cons(A, z1))) -> c12 E(Cons(T, Cons(z0, z1)), z2) -> c49 P[ITE](False, z0, Cons(B, z1)) -> c35 AND(False, True) -> c2 EQUAL(F, B) -> c55 R[ITE](False, z0, Cons(T, z1)) -> c28 T'(z0, z1) -> c71(T[ITE](e(z0, z1), z0, z1), E(z0, z1)) Q[ITE](False, z0, Cons(F, Nil)) -> c21(Q[ITE][FALSE][ITE](and(True, and(True, and(False, equal(head(Nil), F)))), z0, Cons(F, Nil)), AND(True, and(True, and(False, equal(head(Nil), F)))), AND(True, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil)) Q[ITE](False, z0, Cons(T, Cons(B, z1))) -> c11 AND(True, False) -> c1 EQUAL(B, A) -> c64 AND(True, True) -> c3 NOTEMPTY(Nil) -> c70 E(Cons(A, Nil), z0) -> c47 EQUAL(F, T) -> c54 E(Cons(F, Cons(z0, z1)), z2) -> c48 NOTEMPTY(Cons(z0, z1)) -> c69 EQUAL(A, B) -> c67 R[ITE](False, z0, Cons(B, z1)) -> c29 Q[ITE](False, z0, Cons(F, Cons(B, z1))) -> c7 P[ITE](False, z0, Cons(T, z1)) -> c34 Q[ITE](False, z0, Cons(A, Cons(B, z1))) -> c19 EQUAL(T, B) -> c59 Q[ITE](False, z0, Cons(T, Cons(F, z1))) -> c9 T[ITE](False, z0, z1) -> c41 Q[ITE](True, z0, z1) -> c25 E(Cons(T, Nil), z0) -> c45 EQUAL(T, A) -> c60 EQUAL(A, A) -> c68 E(Cons(B, Nil), z0) -> c46 P[ITE](False, z0, Cons(A, z1)) -> c36 E(Cons(F, Nil), z0) -> c44 R[ITE](False, z0, Cons(A, z1)) -> c30 Q[ITE](False, z0, Cons(T, Cons(T, z1))) -> c10 Q[ITE](False, z0, Cons(A, Cons(A, z1))) -> c20 Q[ITE](False, z0, Cons(A, Cons(T, z1))) -> c18 Q[ITE](False, z0, Cons(A, Nil)) -> c24(Q[ITE][FALSE][ITE](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(A, Nil)), AND(True, and(False, and(False, equal(head(Nil), F)))), AND(False, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil)) EQUAL(T, F) -> c57 Q[ITE](False, z0, Cons(A, Cons(F, z1))) -> c17 AND(False, False) -> c E(Nil, z0) -> c52 Q[ITE](False, z0, Cons(B, Cons(F, z1))) -> c13 EQUAL(B, T) -> c62 R[ITE](True, z0, z1) -> c31 EQUAL(B, F) -> c61 EQUAL(F, F) -> c53 E(Cons(A, Cons(z0, z1)), z2) -> c51 Q[ITE](False, z0, Cons(B, Cons(B, z1))) -> c15 Q[ITE](False, z0, Cons(B, Cons(A, z1))) -> c16 EQUAL(T, T) -> c58 Q[ITE](False, z0, Cons(F, Cons(A, z1))) -> c8 EQUAL(A, T) -> c66 Q[ITE](False, z0, Cons(F, Cons(T, z1))) -> c6 Q[ITE][FALSE][ITE](False, z0, z1) -> c40 HEAD(Cons(z0, z1)) -> c43 EQUAL(A, F) -> c65 EQUAL(B, B) -> c63 Q[ITE](False, z0, Cons(T, Nil)) -> c22(Q[ITE][FALSE][ITE](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(T, Nil)), AND(True, and(False, and(False, equal(head(Nil), F)))), AND(False, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil)) T[ITE](True, z0, z1) -> c42 Q[ITE](False, z0, Cons(B, Cons(T, z1))) -> c14 P[ITE](True, z0, z1) -> c37 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True q[Ite](False, z0, Cons(F, Cons(F, z1))) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), z0, Cons(F, Cons(F, z1))) q[Ite](False, z0, Cons(F, Cons(T, z1))) -> False q[Ite](False, z0, Cons(F, Cons(B, z1))) -> False q[Ite](False, z0, Cons(F, Cons(A, z1))) -> False q[Ite](False, z0, Cons(T, Cons(F, z1))) -> False q[Ite](False, z0, Cons(T, Cons(T, z1))) -> False q[Ite](False, z0, Cons(T, Cons(B, z1))) -> False q[Ite](False, z0, Cons(T, Cons(A, z1))) -> False q[Ite](False, z0, Cons(B, Cons(F, z1))) -> False q[Ite](False, z0, Cons(B, Cons(T, z1))) -> False q[Ite](False, z0, Cons(B, Cons(B, z1))) -> False q[Ite](False, z0, Cons(B, Cons(A, z1))) -> False q[Ite](False, z0, Cons(A, Cons(F, z1))) -> False q[Ite](False, z0, Cons(A, Cons(T, z1))) -> False q[Ite](False, z0, Cons(A, Cons(B, z1))) -> False q[Ite](False, z0, Cons(A, Cons(A, z1))) -> False q[Ite](False, z0, Cons(F, Nil)) -> q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), z0, Cons(F, Nil)) q[Ite](False, z0, Cons(T, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(T, Nil)) q[Ite](False, z0, Cons(B, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(B, Nil)) q[Ite](False, z0, Cons(A, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(A, Nil)) q[Ite](True, z0, z1) -> True r[Ite](False, z0, Cons(F, z1)) -> r[Ite][False][Ite][True][Ite](and(q(z0, z1), r(z0, z1)), z0, Cons(F, z1)) r[Ite](False, z0, Cons(T, z1)) -> False r[Ite](False, z0, Cons(B, z1)) -> False r[Ite](False, z0, Cons(A, z1)) -> False r[Ite](True, z0, z1) -> True p[Ite](False, z0, Cons(F, z1)) -> and(r(z0, Cons(F, z1)), p(z0, z1)) p[Ite](False, z0, Cons(T, z1)) -> False p[Ite](False, z0, Cons(B, z1)) -> False p[Ite](False, z0, Cons(A, z1)) -> False p[Ite](True, z0, z1) -> True q[Ite][False][Ite](True, z0, Cons(z1, z2)) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(z1, z2)), q(z0, z2)), z0, Cons(z1, z2)) q[Ite][False][Ite](False, z0, z1) -> False t[Ite](False, z0, z1) -> True t[Ite](True, z0, z1) -> True head(Cons(z0, z1)) -> z0 e(Cons(F, Nil), z0) -> False e(Cons(T, Nil), z0) -> False e(Cons(B, Nil), z0) -> False e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0) e(Cons(F, Cons(z0, z1)), z2) -> False e(Cons(T, Cons(z0, z1)), z2) -> False e(Cons(B, Cons(z0, z1)), z2) -> False e(Cons(A, Cons(z0, z1)), z2) -> False e(Nil, z0) -> False equal(F, F) -> True equal(F, T) -> False equal(F, B) -> False equal(F, A) -> False equal(T, F) -> False equal(T, T) -> True equal(T, B) -> False equal(T, A) -> False equal(B, F) -> False equal(B, T) -> False equal(B, B) -> True equal(B, A) -> False equal(A, F) -> False equal(A, T) -> False equal(A, B) -> False equal(A, A) -> True notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False t(z0, z1) -> t[Ite](e(z0, z1), z0, z1) r(z0, z1) -> r[Ite](e(z0, z1), z0, z1) q(z0, z1) -> q[Ite](e(z0, z1), z0, z1) p(z0, z1) -> p[Ite](e(z0, z1), z0, z1) goal(z0, z1) -> q(z0, z1) Tuples: Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(AND(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), P(z0, Cons(F, Cons(F, z1)))) Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(AND(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), Q(z0, Cons(F, z1))) R[ITE](False, z0, Cons(F, z1)) -> c26(AND(q(z0, z1), r(z0, z1)), Q(z0, z1)) R[ITE](False, z0, Cons(F, z1)) -> c27(AND(q(z0, z1), r(z0, z1)), R(z0, z1)) P[ITE](False, z0, Cons(F, z1)) -> c32(AND(r(z0, Cons(F, z1)), p(z0, z1)), R(z0, Cons(F, z1))) P[ITE](False, z0, Cons(F, z1)) -> c33(AND(r(z0, Cons(F, z1)), p(z0, z1)), P(z0, z1)) Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c38(AND(p(z0, Cons(z1, z2)), q(z0, z2)), P(z0, Cons(z1, z2))) Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c39(AND(p(z0, Cons(z1, z2)), q(z0, z2)), Q(z0, z2)) R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1), E(z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1), E(z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1), E(z0, z1)) S tuples: R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1), E(z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1), E(z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1), E(z0, z1)) K tuples:none Defined Rule Symbols: head_1, e_2, equal_2, notEmpty_1, t_2, r_2, q_2, p_2, goal_2, and_2, q[Ite]_3, r[Ite]_3, p[Ite]_3, q[Ite][False][Ite]_3, t[Ite]_3 Defined Pair Symbols: Q[ITE]_3, R[ITE]_3, P[ITE]_3, Q[ITE][FALSE][ITE]_3, R_2, Q_2, P_2 Compound Symbols: c4_2, c5_2, c26_2, c27_2, c32_2, c33_2, c38_2, c39_2, c72_2, c73_2, c74_2 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 11 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True q[Ite](False, z0, Cons(F, Cons(F, z1))) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), z0, Cons(F, Cons(F, z1))) q[Ite](False, z0, Cons(F, Cons(T, z1))) -> False q[Ite](False, z0, Cons(F, Cons(B, z1))) -> False q[Ite](False, z0, Cons(F, Cons(A, z1))) -> False q[Ite](False, z0, Cons(T, Cons(F, z1))) -> False q[Ite](False, z0, Cons(T, Cons(T, z1))) -> False q[Ite](False, z0, Cons(T, Cons(B, z1))) -> False q[Ite](False, z0, Cons(T, Cons(A, z1))) -> False q[Ite](False, z0, Cons(B, Cons(F, z1))) -> False q[Ite](False, z0, Cons(B, Cons(T, z1))) -> False q[Ite](False, z0, Cons(B, Cons(B, z1))) -> False q[Ite](False, z0, Cons(B, Cons(A, z1))) -> False q[Ite](False, z0, Cons(A, Cons(F, z1))) -> False q[Ite](False, z0, Cons(A, Cons(T, z1))) -> False q[Ite](False, z0, Cons(A, Cons(B, z1))) -> False q[Ite](False, z0, Cons(A, Cons(A, z1))) -> False q[Ite](False, z0, Cons(F, Nil)) -> q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), z0, Cons(F, Nil)) q[Ite](False, z0, Cons(T, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(T, Nil)) q[Ite](False, z0, Cons(B, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(B, Nil)) q[Ite](False, z0, Cons(A, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(A, Nil)) q[Ite](True, z0, z1) -> True r[Ite](False, z0, Cons(F, z1)) -> r[Ite][False][Ite][True][Ite](and(q(z0, z1), r(z0, z1)), z0, Cons(F, z1)) r[Ite](False, z0, Cons(T, z1)) -> False r[Ite](False, z0, Cons(B, z1)) -> False r[Ite](False, z0, Cons(A, z1)) -> False r[Ite](True, z0, z1) -> True p[Ite](False, z0, Cons(F, z1)) -> and(r(z0, Cons(F, z1)), p(z0, z1)) p[Ite](False, z0, Cons(T, z1)) -> False p[Ite](False, z0, Cons(B, z1)) -> False p[Ite](False, z0, Cons(A, z1)) -> False p[Ite](True, z0, z1) -> True q[Ite][False][Ite](True, z0, Cons(z1, z2)) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(z1, z2)), q(z0, z2)), z0, Cons(z1, z2)) q[Ite][False][Ite](False, z0, z1) -> False t[Ite](False, z0, z1) -> True t[Ite](True, z0, z1) -> True head(Cons(z0, z1)) -> z0 e(Cons(F, Nil), z0) -> False e(Cons(T, Nil), z0) -> False e(Cons(B, Nil), z0) -> False e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0) e(Cons(F, Cons(z0, z1)), z2) -> False e(Cons(T, Cons(z0, z1)), z2) -> False e(Cons(B, Cons(z0, z1)), z2) -> False e(Cons(A, Cons(z0, z1)), z2) -> False e(Nil, z0) -> False equal(F, F) -> True equal(F, T) -> False equal(F, B) -> False equal(F, A) -> False equal(T, F) -> False equal(T, T) -> True equal(T, B) -> False equal(T, A) -> False equal(B, F) -> False equal(B, T) -> False equal(B, B) -> True equal(B, A) -> False equal(A, F) -> False equal(A, T) -> False equal(A, B) -> False equal(A, A) -> True notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False t(z0, z1) -> t[Ite](e(z0, z1), z0, z1) r(z0, z1) -> r[Ite](e(z0, z1), z0, z1) q(z0, z1) -> q[Ite](e(z0, z1), z0, z1) p(z0, z1) -> p[Ite](e(z0, z1), z0, z1) goal(z0, z1) -> q(z0, z1) Tuples: Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1)))) Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1))) R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1)) R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1)) P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1))) P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1)) Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c38(P(z0, Cons(z1, z2))) Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c39(Q(z0, z2)) R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) S tuples: R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) K tuples:none Defined Rule Symbols: head_1, e_2, equal_2, notEmpty_1, t_2, r_2, q_2, p_2, goal_2, and_2, q[Ite]_3, r[Ite]_3, p[Ite]_3, q[Ite][False][Ite]_3, t[Ite]_3 Defined Pair Symbols: Q[ITE]_3, R[ITE]_3, P[ITE]_3, Q[ITE][FALSE][ITE]_3, R_2, Q_2, P_2 Compound Symbols: c4_1, c5_1, c26_1, c27_1, c32_1, c33_1, c38_1, c39_1, c72_1, c73_1, c74_1 ---------------------------------------- (9) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 2 leading nodes: Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c38(P(z0, Cons(z1, z2))) Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c39(Q(z0, z2)) ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True q[Ite](False, z0, Cons(F, Cons(F, z1))) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), z0, Cons(F, Cons(F, z1))) q[Ite](False, z0, Cons(F, Cons(T, z1))) -> False q[Ite](False, z0, Cons(F, Cons(B, z1))) -> False q[Ite](False, z0, Cons(F, Cons(A, z1))) -> False q[Ite](False, z0, Cons(T, Cons(F, z1))) -> False q[Ite](False, z0, Cons(T, Cons(T, z1))) -> False q[Ite](False, z0, Cons(T, Cons(B, z1))) -> False q[Ite](False, z0, Cons(T, Cons(A, z1))) -> False q[Ite](False, z0, Cons(B, Cons(F, z1))) -> False q[Ite](False, z0, Cons(B, Cons(T, z1))) -> False q[Ite](False, z0, Cons(B, Cons(B, z1))) -> False q[Ite](False, z0, Cons(B, Cons(A, z1))) -> False q[Ite](False, z0, Cons(A, Cons(F, z1))) -> False q[Ite](False, z0, Cons(A, Cons(T, z1))) -> False q[Ite](False, z0, Cons(A, Cons(B, z1))) -> False q[Ite](False, z0, Cons(A, Cons(A, z1))) -> False q[Ite](False, z0, Cons(F, Nil)) -> q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), z0, Cons(F, Nil)) q[Ite](False, z0, Cons(T, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(T, Nil)) q[Ite](False, z0, Cons(B, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(B, Nil)) q[Ite](False, z0, Cons(A, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(A, Nil)) q[Ite](True, z0, z1) -> True r[Ite](False, z0, Cons(F, z1)) -> r[Ite][False][Ite][True][Ite](and(q(z0, z1), r(z0, z1)), z0, Cons(F, z1)) r[Ite](False, z0, Cons(T, z1)) -> False r[Ite](False, z0, Cons(B, z1)) -> False r[Ite](False, z0, Cons(A, z1)) -> False r[Ite](True, z0, z1) -> True p[Ite](False, z0, Cons(F, z1)) -> and(r(z0, Cons(F, z1)), p(z0, z1)) p[Ite](False, z0, Cons(T, z1)) -> False p[Ite](False, z0, Cons(B, z1)) -> False p[Ite](False, z0, Cons(A, z1)) -> False p[Ite](True, z0, z1) -> True q[Ite][False][Ite](True, z0, Cons(z1, z2)) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(z1, z2)), q(z0, z2)), z0, Cons(z1, z2)) q[Ite][False][Ite](False, z0, z1) -> False t[Ite](False, z0, z1) -> True t[Ite](True, z0, z1) -> True head(Cons(z0, z1)) -> z0 e(Cons(F, Nil), z0) -> False e(Cons(T, Nil), z0) -> False e(Cons(B, Nil), z0) -> False e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0) e(Cons(F, Cons(z0, z1)), z2) -> False e(Cons(T, Cons(z0, z1)), z2) -> False e(Cons(B, Cons(z0, z1)), z2) -> False e(Cons(A, Cons(z0, z1)), z2) -> False e(Nil, z0) -> False equal(F, F) -> True equal(F, T) -> False equal(F, B) -> False equal(F, A) -> False equal(T, F) -> False equal(T, T) -> True equal(T, B) -> False equal(T, A) -> False equal(B, F) -> False equal(B, T) -> False equal(B, B) -> True equal(B, A) -> False equal(A, F) -> False equal(A, T) -> False equal(A, B) -> False equal(A, A) -> True notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False t(z0, z1) -> t[Ite](e(z0, z1), z0, z1) r(z0, z1) -> r[Ite](e(z0, z1), z0, z1) q(z0, z1) -> q[Ite](e(z0, z1), z0, z1) p(z0, z1) -> p[Ite](e(z0, z1), z0, z1) goal(z0, z1) -> q(z0, z1) Tuples: Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1)))) Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1))) R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1)) R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1)) P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1))) P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1)) R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) S tuples: R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) K tuples:none Defined Rule Symbols: head_1, e_2, equal_2, notEmpty_1, t_2, r_2, q_2, p_2, goal_2, and_2, q[Ite]_3, r[Ite]_3, p[Ite]_3, q[Ite][False][Ite]_3, t[Ite]_3 Defined Pair Symbols: Q[ITE]_3, R[ITE]_3, P[ITE]_3, R_2, Q_2, P_2 Compound Symbols: c4_1, c5_1, c26_1, c27_1, c32_1, c33_1, c72_1, c73_1, c74_1 ---------------------------------------- (11) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True q[Ite](False, z0, Cons(F, Cons(F, z1))) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), z0, Cons(F, Cons(F, z1))) q[Ite](False, z0, Cons(F, Cons(T, z1))) -> False q[Ite](False, z0, Cons(F, Cons(B, z1))) -> False q[Ite](False, z0, Cons(F, Cons(A, z1))) -> False q[Ite](False, z0, Cons(T, Cons(F, z1))) -> False q[Ite](False, z0, Cons(T, Cons(T, z1))) -> False q[Ite](False, z0, Cons(T, Cons(B, z1))) -> False q[Ite](False, z0, Cons(T, Cons(A, z1))) -> False q[Ite](False, z0, Cons(B, Cons(F, z1))) -> False q[Ite](False, z0, Cons(B, Cons(T, z1))) -> False q[Ite](False, z0, Cons(B, Cons(B, z1))) -> False q[Ite](False, z0, Cons(B, Cons(A, z1))) -> False q[Ite](False, z0, Cons(A, Cons(F, z1))) -> False q[Ite](False, z0, Cons(A, Cons(T, z1))) -> False q[Ite](False, z0, Cons(A, Cons(B, z1))) -> False q[Ite](False, z0, Cons(A, Cons(A, z1))) -> False q[Ite](False, z0, Cons(F, Nil)) -> q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), z0, Cons(F, Nil)) q[Ite](False, z0, Cons(T, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(T, Nil)) q[Ite](False, z0, Cons(B, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(B, Nil)) q[Ite](False, z0, Cons(A, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(A, Nil)) q[Ite](True, z0, z1) -> True r[Ite](False, z0, Cons(F, z1)) -> r[Ite][False][Ite][True][Ite](and(q(z0, z1), r(z0, z1)), z0, Cons(F, z1)) r[Ite](False, z0, Cons(T, z1)) -> False r[Ite](False, z0, Cons(B, z1)) -> False r[Ite](False, z0, Cons(A, z1)) -> False r[Ite](True, z0, z1) -> True p[Ite](False, z0, Cons(F, z1)) -> and(r(z0, Cons(F, z1)), p(z0, z1)) p[Ite](False, z0, Cons(T, z1)) -> False p[Ite](False, z0, Cons(B, z1)) -> False p[Ite](False, z0, Cons(A, z1)) -> False p[Ite](True, z0, z1) -> True q[Ite][False][Ite](True, z0, Cons(z1, z2)) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(z1, z2)), q(z0, z2)), z0, Cons(z1, z2)) q[Ite][False][Ite](False, z0, z1) -> False t[Ite](False, z0, z1) -> True t[Ite](True, z0, z1) -> True head(Cons(z0, z1)) -> z0 equal(F, F) -> True equal(F, T) -> False equal(F, B) -> False equal(F, A) -> False equal(T, F) -> False equal(T, T) -> True equal(T, B) -> False equal(T, A) -> False equal(B, F) -> False equal(B, T) -> False equal(B, B) -> True equal(B, A) -> False equal(A, F) -> False equal(A, T) -> False equal(A, B) -> False equal(A, A) -> True notEmpty(Cons(z0, z1)) -> True notEmpty(Nil) -> False t(z0, z1) -> t[Ite](e(z0, z1), z0, z1) r(z0, z1) -> r[Ite](e(z0, z1), z0, z1) q(z0, z1) -> q[Ite](e(z0, z1), z0, z1) p(z0, z1) -> p[Ite](e(z0, z1), z0, z1) goal(z0, z1) -> q(z0, z1) ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: e(Cons(F, Nil), z0) -> False e(Cons(T, Nil), z0) -> False e(Cons(B, Nil), z0) -> False e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0) e(Cons(F, Cons(z0, z1)), z2) -> False e(Cons(T, Cons(z0, z1)), z2) -> False e(Cons(B, Cons(z0, z1)), z2) -> False e(Cons(A, Cons(z0, z1)), z2) -> False e(Nil, z0) -> False Tuples: Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1)))) Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1))) R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1)) R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1)) P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1))) P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1)) R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) S tuples: R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) K tuples:none Defined Rule Symbols: e_2 Defined Pair Symbols: Q[ITE]_3, R[ITE]_3, P[ITE]_3, R_2, Q_2, P_2 Compound Symbols: c4_1, c5_1, c26_1, c27_1, c32_1, c33_1, c72_1, c73_1, c74_1 ---------------------------------------- (13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) We considered the (Usable) Rules:none And the Tuples: Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1)))) Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1))) R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1)) R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1)) P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1))) P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1)) R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(A) = [3] POL(B) = [3] POL(Cons(x_1, x_2)) = [1] + x_2 POL(F) = 0 POL(False) = 0 POL(Nil) = 0 POL(P(x_1, x_2)) = x_2 POL(P[ITE](x_1, x_2, x_3)) = x_3 POL(Q(x_1, x_2)) = [1] + x_2 POL(Q[ITE](x_1, x_2, x_3)) = x_3 POL(R(x_1, x_2)) = x_2 POL(R[ITE](x_1, x_2, x_3)) = x_3 POL(T) = [3] POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c32(x_1)) = x_1 POL(c33(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c5(x_1)) = x_1 POL(c72(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c74(x_1)) = x_1 POL(e(x_1, x_2)) = [3]x_1 + [3]x_2 POL(e[Match][Cons][Ite][True][Match](x_1, x_2, x_3)) = [3] + x_1 + x_2 + x_3 ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules: e(Cons(F, Nil), z0) -> False e(Cons(T, Nil), z0) -> False e(Cons(B, Nil), z0) -> False e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0) e(Cons(F, Cons(z0, z1)), z2) -> False e(Cons(T, Cons(z0, z1)), z2) -> False e(Cons(B, Cons(z0, z1)), z2) -> False e(Cons(A, Cons(z0, z1)), z2) -> False e(Nil, z0) -> False Tuples: Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1)))) Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1))) R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1)) R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1)) P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1))) P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1)) R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) S tuples: R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) K tuples: Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) Defined Rule Symbols: e_2 Defined Pair Symbols: Q[ITE]_3, R[ITE]_3, P[ITE]_3, R_2, Q_2, P_2 Compound Symbols: c4_1, c5_1, c26_1, c27_1, c32_1, c33_1, c72_1, c73_1, c74_1 ---------------------------------------- (15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) We considered the (Usable) Rules:none And the Tuples: Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1)))) Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1))) R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1)) R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1)) P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1))) P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1)) R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(A) = [3] POL(B) = [3] POL(Cons(x_1, x_2)) = [2] + x_2 POL(F) = 0 POL(False) = 0 POL(Nil) = 0 POL(P(x_1, x_2)) = [1] + [2]x_2 POL(P[ITE](x_1, x_2, x_3)) = [2]x_3 POL(Q(x_1, x_2)) = [1] + [2]x_2 POL(Q[ITE](x_1, x_2, x_3)) = [1] + [2]x_3 POL(R(x_1, x_2)) = [2]x_2 POL(R[ITE](x_1, x_2, x_3)) = [2]x_3 POL(T) = [3] POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c32(x_1)) = x_1 POL(c33(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c5(x_1)) = x_1 POL(c72(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c74(x_1)) = x_1 POL(e(x_1, x_2)) = [3]x_1 + [3]x_2 POL(e[Match][Cons][Ite][True][Match](x_1, x_2, x_3)) = [3] + x_1 + x_2 + x_3 ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules: e(Cons(F, Nil), z0) -> False e(Cons(T, Nil), z0) -> False e(Cons(B, Nil), z0) -> False e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0) e(Cons(F, Cons(z0, z1)), z2) -> False e(Cons(T, Cons(z0, z1)), z2) -> False e(Cons(B, Cons(z0, z1)), z2) -> False e(Cons(A, Cons(z0, z1)), z2) -> False e(Nil, z0) -> False Tuples: Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1)))) Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1))) R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1)) R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1)) P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1))) P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1)) R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) S tuples: R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) K tuples: Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) Defined Rule Symbols: e_2 Defined Pair Symbols: Q[ITE]_3, R[ITE]_3, P[ITE]_3, R_2, Q_2, P_2 Compound Symbols: c4_1, c5_1, c26_1, c27_1, c32_1, c33_1, c72_1, c73_1, c74_1 ---------------------------------------- (17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) We considered the (Usable) Rules:none And the Tuples: Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1)))) Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1))) R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1)) R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1)) P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1))) P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1)) R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) The order we found is given by the following interpretation: Polynomial interpretation : POL(A) = [1] POL(B) = [1] POL(Cons(x_1, x_2)) = x_1 + x_2 POL(F) = [1] POL(False) = [1] POL(Nil) = [1] POL(P(x_1, x_2)) = [1] + x_1 + x_2 POL(P[ITE](x_1, x_2, x_3)) = [1] + x_2 + x_3 POL(Q(x_1, x_2)) = [1] + x_1 + x_2 POL(Q[ITE](x_1, x_2, x_3)) = [1] + x_2 + x_3 POL(R(x_1, x_2)) = [1] + x_1 + x_2 POL(R[ITE](x_1, x_2, x_3)) = x_2 + x_3 POL(T) = [1] POL(c26(x_1)) = x_1 POL(c27(x_1)) = x_1 POL(c32(x_1)) = x_1 POL(c33(x_1)) = x_1 POL(c4(x_1)) = x_1 POL(c5(x_1)) = x_1 POL(c72(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c74(x_1)) = x_1 POL(e(x_1, x_2)) = [1] + x_1 + x_2 POL(e[Match][Cons][Ite][True][Match](x_1, x_2, x_3)) = [1] + x_1 + x_3 ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules: e(Cons(F, Nil), z0) -> False e(Cons(T, Nil), z0) -> False e(Cons(B, Nil), z0) -> False e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0) e(Cons(F, Cons(z0, z1)), z2) -> False e(Cons(T, Cons(z0, z1)), z2) -> False e(Cons(B, Cons(z0, z1)), z2) -> False e(Cons(A, Cons(z0, z1)), z2) -> False e(Nil, z0) -> False Tuples: Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1)))) Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1))) R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1)) R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1)) P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1))) P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1)) R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) S tuples:none K tuples: Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) Defined Rule Symbols: e_2 Defined Pair Symbols: Q[ITE]_3, R[ITE]_3, P[ITE]_3, R_2, Q_2, P_2 Compound Symbols: c4_1, c5_1, c26_1, c27_1, c32_1, c33_1, c72_1, c73_1, c74_1 ---------------------------------------- (19) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (20) BOUNDS(1, 1)