WORST_CASE(?,O(n^1)) proof of input_nuLJt73yVD.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), 131 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) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 35 ms] (12) CdtProblem (13) CdtKnowledgeProof [FINISHED, 0 ms] (14) 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: disj(T) -> True disj(F) -> True conj(Or(o1, o2)) -> False conj(T) -> True conj(F) -> True disj(And(a1, a2)) -> conj(And(a1, a2)) disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) conj(And(t1, t2)) -> and(disj(t1), conj(t1)) bool(T) -> True bool(F) -> True bool(And(a1, a2)) -> False bool(Or(o1, o2)) -> False isConsTerm(T, T) -> True isConsTerm(T, F) -> False isConsTerm(T, And(y1, y2)) -> False isConsTerm(T, Or(x1, x2)) -> False isConsTerm(F, T) -> False isConsTerm(F, F) -> True isConsTerm(F, And(y1, y2)) -> False isConsTerm(F, Or(x1, x2)) -> False isConsTerm(And(a1, a2), T) -> False isConsTerm(And(a1, a2), F) -> False isConsTerm(And(a1, a2), And(y1, y2)) -> True isConsTerm(And(a1, a2), Or(x1, x2)) -> False isConsTerm(Or(o1, o2), T) -> False isConsTerm(Or(o1, o2), F) -> False isConsTerm(Or(o1, o2), And(y1, y2)) -> False isConsTerm(Or(o1, o2), Or(x1, x2)) -> True isOp(T) -> False isOp(F) -> False isOp(And(t1, t2)) -> True isOp(Or(t1, t2)) -> True isAnd(T) -> False isAnd(F) -> False isAnd(And(t1, t2)) -> True isAnd(Or(t1, t2)) -> False getSecond(And(t1, t2)) -> t1 getSecond(Or(t1, t2)) -> t1 getFirst(And(t1, t2)) -> t1 getFirst(Or(t1, t2)) -> t1 disjconj(p) -> disj(p) 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 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: disj(T) -> True disj(F) -> True conj(Or(o1, o2)) -> False conj(T) -> True conj(F) -> True disj(And(a1, a2)) -> conj(And(a1, a2)) disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) conj(And(t1, t2)) -> and(disj(t1), conj(t1)) bool(T) -> True bool(F) -> True bool(And(a1, a2)) -> False bool(Or(o1, o2)) -> False isConsTerm(T, T) -> True isConsTerm(T, F) -> False isConsTerm(T, And(y1, y2)) -> False isConsTerm(T, Or(x1, x2)) -> False isConsTerm(F, T) -> False isConsTerm(F, F) -> True isConsTerm(F, And(y1, y2)) -> False isConsTerm(F, Or(x1, x2)) -> False isConsTerm(And(a1, a2), T) -> False isConsTerm(And(a1, a2), F) -> False isConsTerm(And(a1, a2), And(y1, y2)) -> True isConsTerm(And(a1, a2), Or(x1, x2)) -> False isConsTerm(Or(o1, o2), T) -> False isConsTerm(Or(o1, o2), F) -> False isConsTerm(Or(o1, o2), And(y1, y2)) -> False isConsTerm(Or(o1, o2), Or(x1, x2)) -> True isOp(T) -> False isOp(F) -> False isOp(And(t1, t2)) -> True isOp(Or(t1, t2)) -> True isAnd(T) -> False isAnd(F) -> False isAnd(And(t1, t2)) -> True isAnd(Or(t1, t2)) -> False getSecond(And(t1, t2)) -> t1 getSecond(Or(t1, t2)) -> t1 getFirst(And(t1, t2)) -> t1 getFirst(Or(t1, t2)) -> t1 disjconj(p) -> disj(p) 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 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 disj(T) -> True disj(F) -> True disj(And(z0, z1)) -> conj(And(z0, z1)) disj(Or(z0, z1)) -> and(conj(z0), disj(z0)) conj(Or(z0, z1)) -> False conj(T) -> True conj(F) -> True conj(And(z0, z1)) -> and(disj(z0), conj(z0)) bool(T) -> True bool(F) -> True bool(And(z0, z1)) -> False bool(Or(z0, z1)) -> False isConsTerm(T, T) -> True isConsTerm(T, F) -> False isConsTerm(T, And(z0, z1)) -> False isConsTerm(T, Or(z0, z1)) -> False isConsTerm(F, T) -> False isConsTerm(F, F) -> True isConsTerm(F, And(z0, z1)) -> False isConsTerm(F, Or(z0, z1)) -> False isConsTerm(And(z0, z1), T) -> False isConsTerm(And(z0, z1), F) -> False isConsTerm(And(z0, z1), And(z2, z3)) -> True isConsTerm(And(z0, z1), Or(z2, z3)) -> False isConsTerm(Or(z0, z1), T) -> False isConsTerm(Or(z0, z1), F) -> False isConsTerm(Or(z0, z1), And(z2, z3)) -> False isConsTerm(Or(z0, z1), Or(z2, z3)) -> True isOp(T) -> False isOp(F) -> False isOp(And(z0, z1)) -> True isOp(Or(z0, z1)) -> True isAnd(T) -> False isAnd(F) -> False isAnd(And(z0, z1)) -> True isAnd(Or(z0, z1)) -> False getSecond(And(z0, z1)) -> z0 getSecond(Or(z0, z1)) -> z0 getFirst(And(z0, z1)) -> z0 getFirst(Or(z0, z1)) -> z0 disjconj(z0) -> disj(z0) Tuples: AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 DISJ(T) -> c4 DISJ(F) -> c5 DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1))) DISJ(Or(z0, z1)) -> c7(AND(conj(z0), disj(z0)), CONJ(z0)) DISJ(Or(z0, z1)) -> c8(AND(conj(z0), disj(z0)), DISJ(z0)) CONJ(Or(z0, z1)) -> c9 CONJ(T) -> c10 CONJ(F) -> c11 CONJ(And(z0, z1)) -> c12(AND(disj(z0), conj(z0)), DISJ(z0)) CONJ(And(z0, z1)) -> c13(AND(disj(z0), conj(z0)), CONJ(z0)) BOOL(T) -> c14 BOOL(F) -> c15 BOOL(And(z0, z1)) -> c16 BOOL(Or(z0, z1)) -> c17 ISCONSTERM(T, T) -> c18 ISCONSTERM(T, F) -> c19 ISCONSTERM(T, And(z0, z1)) -> c20 ISCONSTERM(T, Or(z0, z1)) -> c21 ISCONSTERM(F, T) -> c22 ISCONSTERM(F, F) -> c23 ISCONSTERM(F, And(z0, z1)) -> c24 ISCONSTERM(F, Or(z0, z1)) -> c25 ISCONSTERM(And(z0, z1), T) -> c26 ISCONSTERM(And(z0, z1), F) -> c27 ISCONSTERM(And(z0, z1), And(z2, z3)) -> c28 ISCONSTERM(And(z0, z1), Or(z2, z3)) -> c29 ISCONSTERM(Or(z0, z1), T) -> c30 ISCONSTERM(Or(z0, z1), F) -> c31 ISCONSTERM(Or(z0, z1), And(z2, z3)) -> c32 ISCONSTERM(Or(z0, z1), Or(z2, z3)) -> c33 ISOP(T) -> c34 ISOP(F) -> c35 ISOP(And(z0, z1)) -> c36 ISOP(Or(z0, z1)) -> c37 ISAND(T) -> c38 ISAND(F) -> c39 ISAND(And(z0, z1)) -> c40 ISAND(Or(z0, z1)) -> c41 GETSECOND(And(z0, z1)) -> c42 GETSECOND(Or(z0, z1)) -> c43 GETFIRST(And(z0, z1)) -> c44 GETFIRST(Or(z0, z1)) -> c45 DISJCONJ(z0) -> c46(DISJ(z0)) S tuples: DISJ(T) -> c4 DISJ(F) -> c5 DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1))) DISJ(Or(z0, z1)) -> c7(AND(conj(z0), disj(z0)), CONJ(z0)) DISJ(Or(z0, z1)) -> c8(AND(conj(z0), disj(z0)), DISJ(z0)) CONJ(Or(z0, z1)) -> c9 CONJ(T) -> c10 CONJ(F) -> c11 CONJ(And(z0, z1)) -> c12(AND(disj(z0), conj(z0)), DISJ(z0)) CONJ(And(z0, z1)) -> c13(AND(disj(z0), conj(z0)), CONJ(z0)) BOOL(T) -> c14 BOOL(F) -> c15 BOOL(And(z0, z1)) -> c16 BOOL(Or(z0, z1)) -> c17 ISCONSTERM(T, T) -> c18 ISCONSTERM(T, F) -> c19 ISCONSTERM(T, And(z0, z1)) -> c20 ISCONSTERM(T, Or(z0, z1)) -> c21 ISCONSTERM(F, T) -> c22 ISCONSTERM(F, F) -> c23 ISCONSTERM(F, And(z0, z1)) -> c24 ISCONSTERM(F, Or(z0, z1)) -> c25 ISCONSTERM(And(z0, z1), T) -> c26 ISCONSTERM(And(z0, z1), F) -> c27 ISCONSTERM(And(z0, z1), And(z2, z3)) -> c28 ISCONSTERM(And(z0, z1), Or(z2, z3)) -> c29 ISCONSTERM(Or(z0, z1), T) -> c30 ISCONSTERM(Or(z0, z1), F) -> c31 ISCONSTERM(Or(z0, z1), And(z2, z3)) -> c32 ISCONSTERM(Or(z0, z1), Or(z2, z3)) -> c33 ISOP(T) -> c34 ISOP(F) -> c35 ISOP(And(z0, z1)) -> c36 ISOP(Or(z0, z1)) -> c37 ISAND(T) -> c38 ISAND(F) -> c39 ISAND(And(z0, z1)) -> c40 ISAND(Or(z0, z1)) -> c41 GETSECOND(And(z0, z1)) -> c42 GETSECOND(Or(z0, z1)) -> c43 GETFIRST(And(z0, z1)) -> c44 GETFIRST(Or(z0, z1)) -> c45 DISJCONJ(z0) -> c46(DISJ(z0)) K tuples:none Defined Rule Symbols: disj_1, conj_1, bool_1, isConsTerm_2, isOp_1, isAnd_1, getSecond_1, getFirst_1, disjconj_1, and_2 Defined Pair Symbols: AND_2, DISJ_1, CONJ_1, BOOL_1, ISCONSTERM_2, ISOP_1, ISAND_1, GETSECOND_1, GETFIRST_1, DISJCONJ_1 Compound Symbols: c, c1, c2, c3, c4, c5, c6_1, c7_2, c8_2, c9, c10, c11, c12_2, c13_2, 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_1 ---------------------------------------- (5) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: DISJCONJ(z0) -> c46(DISJ(z0)) Removed 41 trailing nodes: ISAND(T) -> c38 ISCONSTERM(Or(z0, z1), And(z2, z3)) -> c32 ISAND(F) -> c39 ISCONSTERM(F, Or(z0, z1)) -> c25 CONJ(F) -> c11 GETSECOND(Or(z0, z1)) -> c43 ISAND(Or(z0, z1)) -> c41 CONJ(T) -> c10 ISCONSTERM(F, F) -> c23 GETFIRST(And(z0, z1)) -> c44 BOOL(Or(z0, z1)) -> c17 AND(False, True) -> c2 ISCONSTERM(T, F) -> c19 ISCONSTERM(F, T) -> c22 ISOP(And(z0, z1)) -> c36 AND(True, True) -> c3 ISCONSTERM(T, And(z0, z1)) -> c20 DISJ(F) -> c5 GETFIRST(Or(z0, z1)) -> c45 ISOP(T) -> c34 ISCONSTERM(And(z0, z1), F) -> c27 ISCONSTERM(Or(z0, z1), T) -> c30 ISCONSTERM(And(z0, z1), And(z2, z3)) -> c28 ISCONSTERM(Or(z0, z1), Or(z2, z3)) -> c33 BOOL(T) -> c14 DISJ(T) -> c4 ISCONSTERM(T, T) -> c18 ISOP(F) -> c35 ISCONSTERM(F, And(z0, z1)) -> c24 ISCONSTERM(Or(z0, z1), F) -> c31 ISCONSTERM(T, Or(z0, z1)) -> c21 ISOP(Or(z0, z1)) -> c37 ISCONSTERM(And(z0, z1), T) -> c26 GETSECOND(And(z0, z1)) -> c42 ISAND(And(z0, z1)) -> c40 BOOL(And(z0, z1)) -> c16 AND(False, False) -> c BOOL(F) -> c15 AND(True, False) -> c1 ISCONSTERM(And(z0, z1), Or(z2, z3)) -> c29 CONJ(Or(z0, z1)) -> c9 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True disj(T) -> True disj(F) -> True disj(And(z0, z1)) -> conj(And(z0, z1)) disj(Or(z0, z1)) -> and(conj(z0), disj(z0)) conj(Or(z0, z1)) -> False conj(T) -> True conj(F) -> True conj(And(z0, z1)) -> and(disj(z0), conj(z0)) bool(T) -> True bool(F) -> True bool(And(z0, z1)) -> False bool(Or(z0, z1)) -> False isConsTerm(T, T) -> True isConsTerm(T, F) -> False isConsTerm(T, And(z0, z1)) -> False isConsTerm(T, Or(z0, z1)) -> False isConsTerm(F, T) -> False isConsTerm(F, F) -> True isConsTerm(F, And(z0, z1)) -> False isConsTerm(F, Or(z0, z1)) -> False isConsTerm(And(z0, z1), T) -> False isConsTerm(And(z0, z1), F) -> False isConsTerm(And(z0, z1), And(z2, z3)) -> True isConsTerm(And(z0, z1), Or(z2, z3)) -> False isConsTerm(Or(z0, z1), T) -> False isConsTerm(Or(z0, z1), F) -> False isConsTerm(Or(z0, z1), And(z2, z3)) -> False isConsTerm(Or(z0, z1), Or(z2, z3)) -> True isOp(T) -> False isOp(F) -> False isOp(And(z0, z1)) -> True isOp(Or(z0, z1)) -> True isAnd(T) -> False isAnd(F) -> False isAnd(And(z0, z1)) -> True isAnd(Or(z0, z1)) -> False getSecond(And(z0, z1)) -> z0 getSecond(Or(z0, z1)) -> z0 getFirst(And(z0, z1)) -> z0 getFirst(Or(z0, z1)) -> z0 disjconj(z0) -> disj(z0) Tuples: DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1))) DISJ(Or(z0, z1)) -> c7(AND(conj(z0), disj(z0)), CONJ(z0)) DISJ(Or(z0, z1)) -> c8(AND(conj(z0), disj(z0)), DISJ(z0)) CONJ(And(z0, z1)) -> c12(AND(disj(z0), conj(z0)), DISJ(z0)) CONJ(And(z0, z1)) -> c13(AND(disj(z0), conj(z0)), CONJ(z0)) S tuples: DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1))) DISJ(Or(z0, z1)) -> c7(AND(conj(z0), disj(z0)), CONJ(z0)) DISJ(Or(z0, z1)) -> c8(AND(conj(z0), disj(z0)), DISJ(z0)) CONJ(And(z0, z1)) -> c12(AND(disj(z0), conj(z0)), DISJ(z0)) CONJ(And(z0, z1)) -> c13(AND(disj(z0), conj(z0)), CONJ(z0)) K tuples:none Defined Rule Symbols: disj_1, conj_1, bool_1, isConsTerm_2, isOp_1, isAnd_1, getSecond_1, getFirst_1, disjconj_1, and_2 Defined Pair Symbols: DISJ_1, CONJ_1 Compound Symbols: c6_1, c7_2, c8_2, c12_2, c13_2 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 4 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 disj(T) -> True disj(F) -> True disj(And(z0, z1)) -> conj(And(z0, z1)) disj(Or(z0, z1)) -> and(conj(z0), disj(z0)) conj(Or(z0, z1)) -> False conj(T) -> True conj(F) -> True conj(And(z0, z1)) -> and(disj(z0), conj(z0)) bool(T) -> True bool(F) -> True bool(And(z0, z1)) -> False bool(Or(z0, z1)) -> False isConsTerm(T, T) -> True isConsTerm(T, F) -> False isConsTerm(T, And(z0, z1)) -> False isConsTerm(T, Or(z0, z1)) -> False isConsTerm(F, T) -> False isConsTerm(F, F) -> True isConsTerm(F, And(z0, z1)) -> False isConsTerm(F, Or(z0, z1)) -> False isConsTerm(And(z0, z1), T) -> False isConsTerm(And(z0, z1), F) -> False isConsTerm(And(z0, z1), And(z2, z3)) -> True isConsTerm(And(z0, z1), Or(z2, z3)) -> False isConsTerm(Or(z0, z1), T) -> False isConsTerm(Or(z0, z1), F) -> False isConsTerm(Or(z0, z1), And(z2, z3)) -> False isConsTerm(Or(z0, z1), Or(z2, z3)) -> True isOp(T) -> False isOp(F) -> False isOp(And(z0, z1)) -> True isOp(Or(z0, z1)) -> True isAnd(T) -> False isAnd(F) -> False isAnd(And(z0, z1)) -> True isAnd(Or(z0, z1)) -> False getSecond(And(z0, z1)) -> z0 getSecond(Or(z0, z1)) -> z0 getFirst(And(z0, z1)) -> z0 getFirst(Or(z0, z1)) -> z0 disjconj(z0) -> disj(z0) Tuples: DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1))) DISJ(Or(z0, z1)) -> c7(CONJ(z0)) DISJ(Or(z0, z1)) -> c8(DISJ(z0)) CONJ(And(z0, z1)) -> c12(DISJ(z0)) CONJ(And(z0, z1)) -> c13(CONJ(z0)) S tuples: DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1))) DISJ(Or(z0, z1)) -> c7(CONJ(z0)) DISJ(Or(z0, z1)) -> c8(DISJ(z0)) CONJ(And(z0, z1)) -> c12(DISJ(z0)) CONJ(And(z0, z1)) -> c13(CONJ(z0)) K tuples:none Defined Rule Symbols: disj_1, conj_1, bool_1, isConsTerm_2, isOp_1, isAnd_1, getSecond_1, getFirst_1, disjconj_1, and_2 Defined Pair Symbols: DISJ_1, CONJ_1 Compound Symbols: c6_1, c7_1, c8_1, c12_1, c13_1 ---------------------------------------- (9) 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 disj(T) -> True disj(F) -> True disj(And(z0, z1)) -> conj(And(z0, z1)) disj(Or(z0, z1)) -> and(conj(z0), disj(z0)) conj(Or(z0, z1)) -> False conj(T) -> True conj(F) -> True conj(And(z0, z1)) -> and(disj(z0), conj(z0)) bool(T) -> True bool(F) -> True bool(And(z0, z1)) -> False bool(Or(z0, z1)) -> False isConsTerm(T, T) -> True isConsTerm(T, F) -> False isConsTerm(T, And(z0, z1)) -> False isConsTerm(T, Or(z0, z1)) -> False isConsTerm(F, T) -> False isConsTerm(F, F) -> True isConsTerm(F, And(z0, z1)) -> False isConsTerm(F, Or(z0, z1)) -> False isConsTerm(And(z0, z1), T) -> False isConsTerm(And(z0, z1), F) -> False isConsTerm(And(z0, z1), And(z2, z3)) -> True isConsTerm(And(z0, z1), Or(z2, z3)) -> False isConsTerm(Or(z0, z1), T) -> False isConsTerm(Or(z0, z1), F) -> False isConsTerm(Or(z0, z1), And(z2, z3)) -> False isConsTerm(Or(z0, z1), Or(z2, z3)) -> True isOp(T) -> False isOp(F) -> False isOp(And(z0, z1)) -> True isOp(Or(z0, z1)) -> True isAnd(T) -> False isAnd(F) -> False isAnd(And(z0, z1)) -> True isAnd(Or(z0, z1)) -> False getSecond(And(z0, z1)) -> z0 getSecond(Or(z0, z1)) -> z0 getFirst(And(z0, z1)) -> z0 getFirst(Or(z0, z1)) -> z0 disjconj(z0) -> disj(z0) ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1))) DISJ(Or(z0, z1)) -> c7(CONJ(z0)) DISJ(Or(z0, z1)) -> c8(DISJ(z0)) CONJ(And(z0, z1)) -> c12(DISJ(z0)) CONJ(And(z0, z1)) -> c13(CONJ(z0)) S tuples: DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1))) DISJ(Or(z0, z1)) -> c7(CONJ(z0)) DISJ(Or(z0, z1)) -> c8(DISJ(z0)) CONJ(And(z0, z1)) -> c12(DISJ(z0)) CONJ(And(z0, z1)) -> c13(CONJ(z0)) K tuples:none Defined Rule Symbols:none Defined Pair Symbols: DISJ_1, CONJ_1 Compound Symbols: c6_1, c7_1, c8_1, c12_1, c13_1 ---------------------------------------- (11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. DISJ(Or(z0, z1)) -> c7(CONJ(z0)) DISJ(Or(z0, z1)) -> c8(DISJ(z0)) CONJ(And(z0, z1)) -> c12(DISJ(z0)) CONJ(And(z0, z1)) -> c13(CONJ(z0)) We considered the (Usable) Rules:none And the Tuples: DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1))) DISJ(Or(z0, z1)) -> c7(CONJ(z0)) DISJ(Or(z0, z1)) -> c8(DISJ(z0)) CONJ(And(z0, z1)) -> c12(DISJ(z0)) CONJ(And(z0, z1)) -> c13(CONJ(z0)) The order we found is given by the following interpretation: Polynomial interpretation : POL(And(x_1, x_2)) = [1] + x_1 + x_2 POL(CONJ(x_1)) = x_1 POL(DISJ(x_1)) = x_1 POL(Or(x_1, x_2)) = [1] + x_1 POL(c12(x_1)) = x_1 POL(c13(x_1)) = x_1 POL(c6(x_1)) = x_1 POL(c7(x_1)) = x_1 POL(c8(x_1)) = x_1 ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules:none Tuples: DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1))) DISJ(Or(z0, z1)) -> c7(CONJ(z0)) DISJ(Or(z0, z1)) -> c8(DISJ(z0)) CONJ(And(z0, z1)) -> c12(DISJ(z0)) CONJ(And(z0, z1)) -> c13(CONJ(z0)) S tuples: DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1))) K tuples: DISJ(Or(z0, z1)) -> c7(CONJ(z0)) DISJ(Or(z0, z1)) -> c8(DISJ(z0)) CONJ(And(z0, z1)) -> c12(DISJ(z0)) CONJ(And(z0, z1)) -> c13(CONJ(z0)) Defined Rule Symbols:none Defined Pair Symbols: DISJ_1, CONJ_1 Compound Symbols: c6_1, c7_1, c8_1, c12_1, c13_1 ---------------------------------------- (13) CdtKnowledgeProof (FINISHED) The following tuples could be moved from S to K by knowledge propagation: DISJ(And(z0, z1)) -> c6(CONJ(And(z0, z1))) CONJ(And(z0, z1)) -> c12(DISJ(z0)) CONJ(And(z0, z1)) -> c13(CONJ(z0)) Now S is empty ---------------------------------------- (14) BOUNDS(1, 1)