WORST_CASE(Omega(n^1),O(n^2)) proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 818 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 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)), 98 ms] (12) CdtProblem (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 45 ms] (14) CdtProblem (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 428 ms] (16) CdtProblem (17) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (18) CdtProblem (19) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 426 ms] (20) CdtProblem (21) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 493 ms] (22) CdtProblem (23) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms] (24) BOUNDS(1, 1) (25) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (26) TRS for Loop Detection (27) DecreasingLoopProof [LOWER BOUND(ID), 0 ms] (28) BEST (29) proven lower bound (30) LowerBoundPropagationProof [FINISHED, 0 ms] (31) BOUNDS(n^1, INF) (32) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) OR(true, z0) -> c4 OR(false, z0) -> c5 UNION(empty, z0) -> c6 UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3)) REACH(z0, z1, empty, z2) -> c8 REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2)) IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3)) IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12 IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5)) IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5)) The (relative) TRS S consists of the following rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) or(true, z0) -> true or(false, z0) -> z0 union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) reach(z0, z1, empty, z2) -> false reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5) if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5) if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5)) if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)) Rewrite Strategy: INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) OR(true, z0) -> c4 OR(false, z0) -> c5 UNION(empty, z0) -> c6 UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3)) REACH(z0, z1, empty, z2) -> c8 REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2)) IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3)) IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12 IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5)) IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5)) The (relative) TRS S consists of the following rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) or(true, z0) -> true or(false, z0) -> z0 union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) reach(z0, z1, empty, z2) -> false reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5) if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5) if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5)) if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)) Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) or(true, z0) -> true or(false, z0) -> z0 union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) reach(z0, z1, empty, z2) -> false reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5) if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5) if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5)) if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)) EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) OR(true, z0) -> c4 OR(false, z0) -> c5 UNION(empty, z0) -> c6 UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3)) REACH(z0, z1, empty, z2) -> c8 REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2)) IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3)) IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12 IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5)) IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5)) Tuples: EQ'(0, 0) -> c15 EQ'(0, s(z0)) -> c16 EQ'(s(z0), 0) -> c17 EQ'(s(z0), s(z1)) -> c18(EQ'(z0, z1)) OR'(true, z0) -> c19 OR'(false, z0) -> c20 UNION'(empty, z0) -> c21 UNION'(edge(z0, z1, z2), z3) -> c22(UNION'(z2, z3)) REACH'(z0, z1, empty, z2) -> c23 REACH'(z0, z1, edge(z2, z3, z4), z5) -> c24(IF_REACH_1'(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2)) IF_REACH_1'(true, z0, z1, edge(z2, z3, z4), z5) -> c25(IF_REACH_2'(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3)) IF_REACH_1'(false, z0, z1, edge(z2, z3, z4), z5) -> c26(REACH'(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2'(true, z0, z1, edge(z2, z3, z4), z5) -> c27 IF_REACH_2'(false, z0, z1, edge(z2, z3, z4), z5) -> c28(OR'(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5)) EQ''(0, 0) -> c29 EQ''(0, s(z0)) -> c30 EQ''(s(z0), 0) -> c31 EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) OR''(true, z0) -> c33 OR''(false, z0) -> c34 UNION''(empty, z0) -> c35 UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, empty, z2) -> c37 REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2''(true, z0, z1, edge(z2, z3, z4), z5) -> c41 IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(OR''(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(OR''(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) S tuples: EQ''(0, 0) -> c29 EQ''(0, s(z0)) -> c30 EQ''(s(z0), 0) -> c31 EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) OR''(true, z0) -> c33 OR''(false, z0) -> c34 UNION''(empty, z0) -> c35 UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, empty, z2) -> c37 REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2''(true, z0, z1, edge(z2, z3, z4), z5) -> c41 IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(OR''(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(OR''(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) K tuples:none Defined Rule Symbols: EQ_2, OR_2, UNION_2, REACH_4, IF_REACH_1_5, IF_REACH_2_5, eq_2, or_2, union_2, reach_4, if_reach_1_5, if_reach_2_5 Defined Pair Symbols: EQ'_2, OR'_2, UNION'_2, REACH'_4, IF_REACH_1'_5, IF_REACH_2'_5, EQ''_2, OR''_2, UNION''_2, REACH''_4, IF_REACH_1''_5, IF_REACH_2''_5 Compound Symbols: c15, c16, c17, c18_1, c19, c20, c21, c22_1, c23, c24_2, c25_2, c26_1, c27, c28_4, c29, c30, c31, c32_1, c33, c34, c35, c36_1, c37, c38_3, c39_3, c40_1, c41, c42_5, c43_7 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 16 trailing nodes: UNION''(empty, z0) -> c35 OR'(false, z0) -> c20 EQ''(0, s(z0)) -> c30 OR''(false, z0) -> c34 IF_REACH_2'(true, z0, z1, edge(z2, z3, z4), z5) -> c27 EQ'(s(z0), 0) -> c17 OR''(true, z0) -> c33 EQ''(s(z0), 0) -> c31 IF_REACH_2''(true, z0, z1, edge(z2, z3, z4), z5) -> c41 EQ'(0, s(z0)) -> c16 REACH'(z0, z1, empty, z2) -> c23 EQ''(0, 0) -> c29 EQ'(0, 0) -> c15 UNION'(empty, z0) -> c21 REACH''(z0, z1, empty, z2) -> c37 OR'(true, z0) -> c19 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) or(true, z0) -> true or(false, z0) -> z0 union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) reach(z0, z1, empty, z2) -> false reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5) if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5) if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5)) if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)) EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) OR(true, z0) -> c4 OR(false, z0) -> c5 UNION(empty, z0) -> c6 UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3)) REACH(z0, z1, empty, z2) -> c8 REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2)) IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3)) IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12 IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5)) IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5)) Tuples: EQ'(s(z0), s(z1)) -> c18(EQ'(z0, z1)) UNION'(edge(z0, z1, z2), z3) -> c22(UNION'(z2, z3)) REACH'(z0, z1, edge(z2, z3, z4), z5) -> c24(IF_REACH_1'(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2)) IF_REACH_1'(true, z0, z1, edge(z2, z3, z4), z5) -> c25(IF_REACH_2'(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3)) IF_REACH_1'(false, z0, z1, edge(z2, z3, z4), z5) -> c26(REACH'(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2'(false, z0, z1, edge(z2, z3, z4), z5) -> c28(OR'(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5)) EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(OR''(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(OR''(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) S tuples: EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(OR''(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(OR''(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) K tuples:none Defined Rule Symbols: EQ_2, OR_2, UNION_2, REACH_4, IF_REACH_1_5, IF_REACH_2_5, eq_2, or_2, union_2, reach_4, if_reach_1_5, if_reach_2_5 Defined Pair Symbols: EQ'_2, UNION'_2, REACH'_4, IF_REACH_1'_5, IF_REACH_2'_5, EQ''_2, UNION''_2, REACH''_4, IF_REACH_1''_5, IF_REACH_2''_5 Compound Symbols: c18_1, c22_1, c24_2, c25_2, c26_1, c28_4, c32_1, c36_1, c38_3, c39_3, c40_1, c42_5, c43_7 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 3 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) or(true, z0) -> true or(false, z0) -> z0 union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) reach(z0, z1, empty, z2) -> false reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5) if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5) if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5)) if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)) EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) OR(true, z0) -> c4 OR(false, z0) -> c5 UNION(empty, z0) -> c6 UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3)) REACH(z0, z1, empty, z2) -> c8 REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2)) IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3)) IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12 IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5)) IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5)) Tuples: EQ'(s(z0), s(z1)) -> c18(EQ'(z0, z1)) UNION'(edge(z0, z1, z2), z3) -> c22(UNION'(z2, z3)) REACH'(z0, z1, edge(z2, z3, z4), z5) -> c24(IF_REACH_1'(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2)) IF_REACH_1'(true, z0, z1, edge(z2, z3, z4), z5) -> c25(IF_REACH_2'(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3)) IF_REACH_1'(false, z0, z1, edge(z2, z3, z4), z5) -> c26(REACH'(z0, z1, z4, edge(z2, z3, z5))) EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2'(false, z0, z1, edge(z2, z3, z4), z5) -> c28(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) S tuples: EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) K tuples:none Defined Rule Symbols: EQ_2, OR_2, UNION_2, REACH_4, IF_REACH_1_5, IF_REACH_2_5, eq_2, or_2, union_2, reach_4, if_reach_1_5, if_reach_2_5 Defined Pair Symbols: EQ'_2, UNION'_2, REACH'_4, IF_REACH_1'_5, EQ''_2, UNION''_2, REACH''_4, IF_REACH_1''_5, IF_REACH_2'_5, IF_REACH_2''_5 Compound Symbols: c18_1, c22_1, c24_2, c25_2, c26_1, c32_1, c36_1, c38_3, c39_3, c40_1, c28_3, c42_4, c43_6 ---------------------------------------- (9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: or(true, z0) -> true or(false, z0) -> z0 reach(z0, z1, empty, z2) -> false reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5) if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5) if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5)) if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)) EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) OR(true, z0) -> c4 OR(false, z0) -> c5 UNION(empty, z0) -> c6 UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3)) REACH(z0, z1, empty, z2) -> c8 REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2)) IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3)) IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12 IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5)) IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5)) ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) Tuples: EQ'(s(z0), s(z1)) -> c18(EQ'(z0, z1)) UNION'(edge(z0, z1, z2), z3) -> c22(UNION'(z2, z3)) REACH'(z0, z1, edge(z2, z3, z4), z5) -> c24(IF_REACH_1'(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2)) IF_REACH_1'(true, z0, z1, edge(z2, z3, z4), z5) -> c25(IF_REACH_2'(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3)) IF_REACH_1'(false, z0, z1, edge(z2, z3, z4), z5) -> c26(REACH'(z0, z1, z4, edge(z2, z3, z5))) EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2'(false, z0, z1, edge(z2, z3, z4), z5) -> c28(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) S tuples: EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) K tuples:none Defined Rule Symbols: eq_2, union_2 Defined Pair Symbols: EQ'_2, UNION'_2, REACH'_4, IF_REACH_1'_5, EQ''_2, UNION''_2, REACH''_4, IF_REACH_1''_5, IF_REACH_2'_5, IF_REACH_2''_5 Compound Symbols: c18_1, c22_1, c24_2, c25_2, c26_1, c32_1, c36_1, c38_3, c39_3, c40_1, c28_3, c42_4, c43_6 ---------------------------------------- (11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) We considered the (Usable) Rules: union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) And the Tuples: EQ'(s(z0), s(z1)) -> c18(EQ'(z0, z1)) UNION'(edge(z0, z1, z2), z3) -> c22(UNION'(z2, z3)) REACH'(z0, z1, edge(z2, z3, z4), z5) -> c24(IF_REACH_1'(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2)) IF_REACH_1'(true, z0, z1, edge(z2, z3, z4), z5) -> c25(IF_REACH_2'(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3)) IF_REACH_1'(false, z0, z1, edge(z2, z3, z4), z5) -> c26(REACH'(z0, z1, z4, edge(z2, z3, z5))) EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2'(false, z0, z1, edge(z2, z3, z4), z5) -> c28(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = [1] POL(EQ'(x_1, x_2)) = 0 POL(EQ''(x_1, x_2)) = 0 POL(IF_REACH_1'(x_1, x_2, x_3, x_4, x_5)) = 0 POL(IF_REACH_1''(x_1, x_2, x_3, x_4, x_5)) = x_3 + x_4 + x_5 POL(IF_REACH_2'(x_1, x_2, x_3, x_4, x_5)) = 0 POL(IF_REACH_2''(x_1, x_2, x_3, x_4, x_5)) = x_3 + x_4 + x_5 POL(REACH'(x_1, x_2, x_3, x_4)) = 0 POL(REACH''(x_1, x_2, x_3, x_4)) = x_2 + x_3 + x_4 POL(UNION'(x_1, x_2)) = 0 POL(UNION''(x_1, x_2)) = 0 POL(c18(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c24(x_1, x_2)) = x_1 + x_2 POL(c25(x_1, x_2)) = x_1 + x_2 POL(c26(x_1)) = x_1 POL(c28(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c32(x_1)) = x_1 POL(c36(x_1)) = x_1 POL(c38(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c39(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c40(x_1)) = x_1 POL(c42(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4 POL(c43(x_1, x_2, x_3, x_4, x_5, x_6)) = x_1 + x_2 + x_3 + x_4 + x_5 + x_6 POL(edge(x_1, x_2, x_3)) = [1] + x_3 POL(empty) = 0 POL(eq(x_1, x_2)) = x_1 + x_2 POL(false) = 0 POL(s(x_1)) = [1] + x_1 POL(true) = [1] POL(union(x_1, x_2)) = x_1 + x_2 ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) Tuples: EQ'(s(z0), s(z1)) -> c18(EQ'(z0, z1)) UNION'(edge(z0, z1, z2), z3) -> c22(UNION'(z2, z3)) REACH'(z0, z1, edge(z2, z3, z4), z5) -> c24(IF_REACH_1'(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2)) IF_REACH_1'(true, z0, z1, edge(z2, z3, z4), z5) -> c25(IF_REACH_2'(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3)) IF_REACH_1'(false, z0, z1, edge(z2, z3, z4), z5) -> c26(REACH'(z0, z1, z4, edge(z2, z3, z5))) EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2'(false, z0, z1, edge(z2, z3, z4), z5) -> c28(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) S tuples: EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) K tuples: IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) Defined Rule Symbols: eq_2, union_2 Defined Pair Symbols: EQ'_2, UNION'_2, REACH'_4, IF_REACH_1'_5, EQ''_2, UNION''_2, REACH''_4, IF_REACH_1''_5, IF_REACH_2'_5, IF_REACH_2''_5 Compound Symbols: c18_1, c22_1, c24_2, c25_2, c26_1, c32_1, c36_1, c38_3, c39_3, c40_1, c28_3, c42_4, c43_6 ---------------------------------------- (13) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) We considered the (Usable) Rules: union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) And the Tuples: EQ'(s(z0), s(z1)) -> c18(EQ'(z0, z1)) UNION'(edge(z0, z1, z2), z3) -> c22(UNION'(z2, z3)) REACH'(z0, z1, edge(z2, z3, z4), z5) -> c24(IF_REACH_1'(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2)) IF_REACH_1'(true, z0, z1, edge(z2, z3, z4), z5) -> c25(IF_REACH_2'(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3)) IF_REACH_1'(false, z0, z1, edge(z2, z3, z4), z5) -> c26(REACH'(z0, z1, z4, edge(z2, z3, z5))) EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2'(false, z0, z1, edge(z2, z3, z4), z5) -> c28(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = 0 POL(EQ'(x_1, x_2)) = 0 POL(EQ''(x_1, x_2)) = 0 POL(IF_REACH_1'(x_1, x_2, x_3, x_4, x_5)) = 0 POL(IF_REACH_1''(x_1, x_2, x_3, x_4, x_5)) = [1] + x_4 + x_5 POL(IF_REACH_2'(x_1, x_2, x_3, x_4, x_5)) = 0 POL(IF_REACH_2''(x_1, x_2, x_3, x_4, x_5)) = x_4 + x_5 POL(REACH'(x_1, x_2, x_3, x_4)) = 0 POL(REACH''(x_1, x_2, x_3, x_4)) = [1] + x_3 + x_4 POL(UNION'(x_1, x_2)) = 0 POL(UNION''(x_1, x_2)) = 0 POL(c18(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c24(x_1, x_2)) = x_1 + x_2 POL(c25(x_1, x_2)) = x_1 + x_2 POL(c26(x_1)) = x_1 POL(c28(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c32(x_1)) = x_1 POL(c36(x_1)) = x_1 POL(c38(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c39(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c40(x_1)) = x_1 POL(c42(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4 POL(c43(x_1, x_2, x_3, x_4, x_5, x_6)) = x_1 + x_2 + x_3 + x_4 + x_5 + x_6 POL(edge(x_1, x_2, x_3)) = [1] + x_3 POL(empty) = 0 POL(eq(x_1, x_2)) = 0 POL(false) = 0 POL(s(x_1)) = x_1 POL(true) = 0 POL(union(x_1, x_2)) = x_1 + x_2 ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) Tuples: EQ'(s(z0), s(z1)) -> c18(EQ'(z0, z1)) UNION'(edge(z0, z1, z2), z3) -> c22(UNION'(z2, z3)) REACH'(z0, z1, edge(z2, z3, z4), z5) -> c24(IF_REACH_1'(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2)) IF_REACH_1'(true, z0, z1, edge(z2, z3, z4), z5) -> c25(IF_REACH_2'(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3)) IF_REACH_1'(false, z0, z1, edge(z2, z3, z4), z5) -> c26(REACH'(z0, z1, z4, edge(z2, z3, z5))) EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2'(false, z0, z1, edge(z2, z3, z4), z5) -> c28(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) S tuples: EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) K tuples: IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) Defined Rule Symbols: eq_2, union_2 Defined Pair Symbols: EQ'_2, UNION'_2, REACH'_4, IF_REACH_1'_5, EQ''_2, UNION''_2, REACH''_4, IF_REACH_1''_5, IF_REACH_2'_5, IF_REACH_2''_5 Compound Symbols: c18_1, c22_1, c24_2, c25_2, c26_1, c32_1, c36_1, c38_3, c39_3, c40_1, c28_3, c42_4, c43_6 ---------------------------------------- (15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) We considered the (Usable) Rules: union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) And the Tuples: EQ'(s(z0), s(z1)) -> c18(EQ'(z0, z1)) UNION'(edge(z0, z1, z2), z3) -> c22(UNION'(z2, z3)) REACH'(z0, z1, edge(z2, z3, z4), z5) -> c24(IF_REACH_1'(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2)) IF_REACH_1'(true, z0, z1, edge(z2, z3, z4), z5) -> c25(IF_REACH_2'(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3)) IF_REACH_1'(false, z0, z1, edge(z2, z3, z4), z5) -> c26(REACH'(z0, z1, z4, edge(z2, z3, z5))) EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2'(false, z0, z1, edge(z2, z3, z4), z5) -> c28(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = [2] POL(EQ'(x_1, x_2)) = 0 POL(EQ''(x_1, x_2)) = 0 POL(IF_REACH_1'(x_1, x_2, x_3, x_4, x_5)) = 0 POL(IF_REACH_1''(x_1, x_2, x_3, x_4, x_5)) = [2]x_4 + x_5^2 + [2]x_4*x_5 + x_4^2 POL(IF_REACH_2'(x_1, x_2, x_3, x_4, x_5)) = 0 POL(IF_REACH_2''(x_1, x_2, x_3, x_4, x_5)) = x_5^2 + [2]x_4*x_5 + x_4^2 POL(REACH'(x_1, x_2, x_3, x_4)) = 0 POL(REACH''(x_1, x_2, x_3, x_4)) = [2]x_3 + x_4^2 + [2]x_3*x_4 + x_3^2 POL(UNION'(x_1, x_2)) = 0 POL(UNION''(x_1, x_2)) = x_2 POL(c18(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c24(x_1, x_2)) = x_1 + x_2 POL(c25(x_1, x_2)) = x_1 + x_2 POL(c26(x_1)) = x_1 POL(c28(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c32(x_1)) = x_1 POL(c36(x_1)) = x_1 POL(c38(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c39(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c40(x_1)) = x_1 POL(c42(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4 POL(c43(x_1, x_2, x_3, x_4, x_5, x_6)) = x_1 + x_2 + x_3 + x_4 + x_5 + x_6 POL(edge(x_1, x_2, x_3)) = [2] + x_3 POL(empty) = 0 POL(eq(x_1, x_2)) = 0 POL(false) = 0 POL(s(x_1)) = 0 POL(true) = 0 POL(union(x_1, x_2)) = x_1 + x_2 ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) Tuples: EQ'(s(z0), s(z1)) -> c18(EQ'(z0, z1)) UNION'(edge(z0, z1, z2), z3) -> c22(UNION'(z2, z3)) REACH'(z0, z1, edge(z2, z3, z4), z5) -> c24(IF_REACH_1'(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2)) IF_REACH_1'(true, z0, z1, edge(z2, z3, z4), z5) -> c25(IF_REACH_2'(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3)) IF_REACH_1'(false, z0, z1, edge(z2, z3, z4), z5) -> c26(REACH'(z0, z1, z4, edge(z2, z3, z5))) EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2'(false, z0, z1, edge(z2, z3, z4), z5) -> c28(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) S tuples: EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) K tuples: IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) Defined Rule Symbols: eq_2, union_2 Defined Pair Symbols: EQ'_2, UNION'_2, REACH'_4, IF_REACH_1'_5, EQ''_2, UNION''_2, REACH''_4, IF_REACH_1''_5, IF_REACH_2'_5, IF_REACH_2''_5 Compound Symbols: c18_1, c22_1, c24_2, c25_2, c26_1, c32_1, c36_1, c38_3, c39_3, c40_1, c28_3, c42_4, c43_6 ---------------------------------------- (17) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) Tuples: EQ'(s(z0), s(z1)) -> c18(EQ'(z0, z1)) UNION'(edge(z0, z1, z2), z3) -> c22(UNION'(z2, z3)) REACH'(z0, z1, edge(z2, z3, z4), z5) -> c24(IF_REACH_1'(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2)) IF_REACH_1'(true, z0, z1, edge(z2, z3, z4), z5) -> c25(IF_REACH_2'(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3)) IF_REACH_1'(false, z0, z1, edge(z2, z3, z4), z5) -> c26(REACH'(z0, z1, z4, edge(z2, z3, z5))) EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2'(false, z0, z1, edge(z2, z3, z4), z5) -> c28(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) S tuples: EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) K tuples: IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) Defined Rule Symbols: eq_2, union_2 Defined Pair Symbols: EQ'_2, UNION'_2, REACH'_4, IF_REACH_1'_5, EQ''_2, UNION''_2, REACH''_4, IF_REACH_1''_5, IF_REACH_2'_5, IF_REACH_2''_5 Compound Symbols: c18_1, c22_1, c24_2, c25_2, c26_1, c32_1, c36_1, c38_3, c39_3, c40_1, c28_3, c42_4, c43_6 ---------------------------------------- (19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) We considered the (Usable) Rules: union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) And the Tuples: EQ'(s(z0), s(z1)) -> c18(EQ'(z0, z1)) UNION'(edge(z0, z1, z2), z3) -> c22(UNION'(z2, z3)) REACH'(z0, z1, edge(z2, z3, z4), z5) -> c24(IF_REACH_1'(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2)) IF_REACH_1'(true, z0, z1, edge(z2, z3, z4), z5) -> c25(IF_REACH_2'(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3)) IF_REACH_1'(false, z0, z1, edge(z2, z3, z4), z5) -> c26(REACH'(z0, z1, z4, edge(z2, z3, z5))) EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2'(false, z0, z1, edge(z2, z3, z4), z5) -> c28(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = [2] POL(EQ'(x_1, x_2)) = 0 POL(EQ''(x_1, x_2)) = 0 POL(IF_REACH_1'(x_1, x_2, x_3, x_4, x_5)) = 0 POL(IF_REACH_1''(x_1, x_2, x_3, x_4, x_5)) = x_5^2 + [2]x_4*x_5 + x_4^2 POL(IF_REACH_2'(x_1, x_2, x_3, x_4, x_5)) = 0 POL(IF_REACH_2''(x_1, x_2, x_3, x_4, x_5)) = x_5^2 + [2]x_4*x_5 + x_4^2 POL(REACH'(x_1, x_2, x_3, x_4)) = 0 POL(REACH''(x_1, x_2, x_3, x_4)) = x_4^2 + [2]x_3*x_4 + x_3^2 POL(UNION'(x_1, x_2)) = 0 POL(UNION''(x_1, x_2)) = [2] + [2]x_1 POL(c18(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c24(x_1, x_2)) = x_1 + x_2 POL(c25(x_1, x_2)) = x_1 + x_2 POL(c26(x_1)) = x_1 POL(c28(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c32(x_1)) = x_1 POL(c36(x_1)) = x_1 POL(c38(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c39(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c40(x_1)) = x_1 POL(c42(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4 POL(c43(x_1, x_2, x_3, x_4, x_5, x_6)) = x_1 + x_2 + x_3 + x_4 + x_5 + x_6 POL(edge(x_1, x_2, x_3)) = [2] + x_3 POL(empty) = 0 POL(eq(x_1, x_2)) = 0 POL(false) = 0 POL(s(x_1)) = 0 POL(true) = 0 POL(union(x_1, x_2)) = x_1 + x_2 ---------------------------------------- (20) Obligation: Complexity Dependency Tuples Problem Rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) Tuples: EQ'(s(z0), s(z1)) -> c18(EQ'(z0, z1)) UNION'(edge(z0, z1, z2), z3) -> c22(UNION'(z2, z3)) REACH'(z0, z1, edge(z2, z3, z4), z5) -> c24(IF_REACH_1'(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2)) IF_REACH_1'(true, z0, z1, edge(z2, z3, z4), z5) -> c25(IF_REACH_2'(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3)) IF_REACH_1'(false, z0, z1, edge(z2, z3, z4), z5) -> c26(REACH'(z0, z1, z4, edge(z2, z3, z5))) EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2'(false, z0, z1, edge(z2, z3, z4), z5) -> c28(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) S tuples: EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) K tuples: IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) Defined Rule Symbols: eq_2, union_2 Defined Pair Symbols: EQ'_2, UNION'_2, REACH'_4, IF_REACH_1'_5, EQ''_2, UNION''_2, REACH''_4, IF_REACH_1''_5, IF_REACH_2'_5, IF_REACH_2''_5 Compound Symbols: c18_1, c22_1, c24_2, c25_2, c26_1, c32_1, c36_1, c38_3, c39_3, c40_1, c28_3, c42_4, c43_6 ---------------------------------------- (21) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) We considered the (Usable) Rules: union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) And the Tuples: EQ'(s(z0), s(z1)) -> c18(EQ'(z0, z1)) UNION'(edge(z0, z1, z2), z3) -> c22(UNION'(z2, z3)) REACH'(z0, z1, edge(z2, z3, z4), z5) -> c24(IF_REACH_1'(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2)) IF_REACH_1'(true, z0, z1, edge(z2, z3, z4), z5) -> c25(IF_REACH_2'(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3)) IF_REACH_1'(false, z0, z1, edge(z2, z3, z4), z5) -> c26(REACH'(z0, z1, z4, edge(z2, z3, z5))) EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2'(false, z0, z1, edge(z2, z3, z4), z5) -> c28(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) The order we found is given by the following interpretation: Polynomial interpretation : POL(0) = [2] POL(EQ'(x_1, x_2)) = 0 POL(EQ''(x_1, x_2)) = x_1 POL(IF_REACH_1'(x_1, x_2, x_3, x_4, x_5)) = 0 POL(IF_REACH_1''(x_1, x_2, x_3, x_4, x_5)) = x_3 + x_5^2 + [2]x_4*x_5 + [2]x_3*x_5 + x_4^2 + [2]x_3*x_4 + x_2*x_4 POL(IF_REACH_2'(x_1, x_2, x_3, x_4, x_5)) = 0 POL(IF_REACH_2''(x_1, x_2, x_3, x_4, x_5)) = x_5^2 + [2]x_4*x_5 + [2]x_3*x_5 + x_4^2 + [2]x_3*x_4 + x_2*x_4 POL(REACH'(x_1, x_2, x_3, x_4)) = 0 POL(REACH''(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_4^2 + [2]x_3*x_4 + [2]x_2*x_4 + x_1*x_3 + x_3^2 + [2]x_2*x_3 POL(UNION'(x_1, x_2)) = 0 POL(UNION''(x_1, x_2)) = 0 POL(c18(x_1)) = x_1 POL(c22(x_1)) = x_1 POL(c24(x_1, x_2)) = x_1 + x_2 POL(c25(x_1, x_2)) = x_1 + x_2 POL(c26(x_1)) = x_1 POL(c28(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c32(x_1)) = x_1 POL(c36(x_1)) = x_1 POL(c38(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c39(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c40(x_1)) = x_1 POL(c42(x_1, x_2, x_3, x_4)) = x_1 + x_2 + x_3 + x_4 POL(c43(x_1, x_2, x_3, x_4, x_5, x_6)) = x_1 + x_2 + x_3 + x_4 + x_5 + x_6 POL(edge(x_1, x_2, x_3)) = [1] + x_2 + x_3 POL(empty) = 0 POL(eq(x_1, x_2)) = 0 POL(false) = 0 POL(s(x_1)) = [1] + x_1 POL(true) = 0 POL(union(x_1, x_2)) = x_1 + x_2 ---------------------------------------- (22) Obligation: Complexity Dependency Tuples Problem Rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) Tuples: EQ'(s(z0), s(z1)) -> c18(EQ'(z0, z1)) UNION'(edge(z0, z1, z2), z3) -> c22(UNION'(z2, z3)) REACH'(z0, z1, edge(z2, z3, z4), z5) -> c24(IF_REACH_1'(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2)) IF_REACH_1'(true, z0, z1, edge(z2, z3, z4), z5) -> c25(IF_REACH_2'(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3)) IF_REACH_1'(false, z0, z1, edge(z2, z3, z4), z5) -> c26(REACH'(z0, z1, z4, edge(z2, z3, z5))) EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2'(false, z0, z1, edge(z2, z3, z4), z5) -> c28(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) S tuples:none K tuples: IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c42(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z0, z1, z4, z5)) IF_REACH_2''(false, z0, z1, edge(z2, z3, z4), z5) -> c43(REACH'(z0, z1, z4, z5), REACH'(z3, z1, union(z4, z5), empty), UNION'(z4, z5), REACH''(z3, z1, union(z4, z5), empty), UNION'(z4, z5), UNION''(z4, z5)) IF_REACH_1''(true, z0, z1, edge(z2, z3, z4), z5) -> c39(IF_REACH_2''(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ'(z1, z3), EQ''(z1, z3)) IF_REACH_1''(false, z0, z1, edge(z2, z3, z4), z5) -> c40(REACH''(z0, z1, z4, edge(z2, z3, z5))) REACH''(z0, z1, edge(z2, z3, z4), z5) -> c38(IF_REACH_1''(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ'(z0, z2), EQ''(z0, z2)) UNION''(edge(z0, z1, z2), z3) -> c36(UNION''(z2, z3)) EQ''(s(z0), s(z1)) -> c32(EQ''(z0, z1)) Defined Rule Symbols: eq_2, union_2 Defined Pair Symbols: EQ'_2, UNION'_2, REACH'_4, IF_REACH_1'_5, EQ''_2, UNION''_2, REACH''_4, IF_REACH_1''_5, IF_REACH_2'_5, IF_REACH_2''_5 Compound Symbols: c18_1, c22_1, c24_2, c25_2, c26_1, c32_1, c36_1, c38_3, c39_3, c40_1, c28_3, c42_4, c43_6 ---------------------------------------- (23) SIsEmptyProof (BOTH BOUNDS(ID, ID)) The set S is empty ---------------------------------------- (24) BOUNDS(1, 1) ---------------------------------------- (25) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (26) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) OR(true, z0) -> c4 OR(false, z0) -> c5 UNION(empty, z0) -> c6 UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3)) REACH(z0, z1, empty, z2) -> c8 REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2)) IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3)) IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12 IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5)) IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5)) The (relative) TRS S consists of the following rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) or(true, z0) -> true or(false, z0) -> z0 union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) reach(z0, z1, empty, z2) -> false reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5) if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5) if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5)) if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)) Rewrite Strategy: INNERMOST ---------------------------------------- (27) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence EQ(s(z0), s(z1)) ->^+ c3(EQ(z0, z1)) gives rise to a decreasing loop by considering the right hand sides subterm at position [0]. The pumping substitution is [z0 / s(z0), z1 / s(z1)]. The result substitution is [ ]. ---------------------------------------- (28) Complex Obligation (BEST) ---------------------------------------- (29) Obligation: Proved the lower bound n^1 for the following obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) OR(true, z0) -> c4 OR(false, z0) -> c5 UNION(empty, z0) -> c6 UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3)) REACH(z0, z1, empty, z2) -> c8 REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2)) IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3)) IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12 IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5)) IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5)) The (relative) TRS S consists of the following rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) or(true, z0) -> true or(false, z0) -> z0 union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) reach(z0, z1, empty, z2) -> false reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5) if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5) if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5)) if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)) Rewrite Strategy: INNERMOST ---------------------------------------- (30) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (31) BOUNDS(n^1, INF) ---------------------------------------- (32) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^2). The TRS R consists of the following rules: EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) OR(true, z0) -> c4 OR(false, z0) -> c5 UNION(empty, z0) -> c6 UNION(edge(z0, z1, z2), z3) -> c7(UNION(z2, z3)) REACH(z0, z1, empty, z2) -> c8 REACH(z0, z1, edge(z2, z3, z4), z5) -> c9(IF_REACH_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5), EQ(z0, z2)) IF_REACH_1(true, z0, z1, edge(z2, z3, z4), z5) -> c10(IF_REACH_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5), EQ(z1, z3)) IF_REACH_1(false, z0, z1, edge(z2, z3, z4), z5) -> c11(REACH(z0, z1, z4, edge(z2, z3, z5))) IF_REACH_2(true, z0, z1, edge(z2, z3, z4), z5) -> c12 IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c13(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z0, z1, z4, z5)) IF_REACH_2(false, z0, z1, edge(z2, z3, z4), z5) -> c14(OR(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)), REACH(z3, z1, union(z4, z5), empty), UNION(z4, z5)) The (relative) TRS S consists of the following rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) or(true, z0) -> true or(false, z0) -> z0 union(empty, z0) -> z0 union(edge(z0, z1, z2), z3) -> edge(z0, z1, union(z2, z3)) reach(z0, z1, empty, z2) -> false reach(z0, z1, edge(z2, z3, z4), z5) -> if_reach_1(eq(z0, z2), z0, z1, edge(z2, z3, z4), z5) if_reach_1(true, z0, z1, edge(z2, z3, z4), z5) -> if_reach_2(eq(z1, z3), z0, z1, edge(z2, z3, z4), z5) if_reach_1(false, z0, z1, edge(z2, z3, z4), z5) -> reach(z0, z1, z4, edge(z2, z3, z5)) if_reach_2(true, z0, z1, edge(z2, z3, z4), z5) -> true if_reach_2(false, z0, z1, edge(z2, z3, z4), z5) -> or(reach(z0, z1, z4, z5), reach(z3, z1, union(z4, z5), empty)) Rewrite Strategy: INNERMOST