WORST_CASE(Omega(n^1),O(n^2)) proof of /export/starexec/sandbox/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), 1093 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) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 4 ms] (12) CdtProblem (13) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 190 ms] (14) CdtProblem (15) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CdtProblem (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 886 ms] (18) CdtProblem (19) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 656 ms] (20) CdtProblem (21) CdtKnowledgeProof [BOTH BOUNDS(ID, ID), 0 ms] (22) CdtProblem (23) CdtRuleRemovalProof [UPPER BOUND(ADD(n^2)), 650 ms] (24) CdtProblem (25) CdtKnowledgeProof [FINISHED, 0 ms] (26) BOUNDS(1, 1) (27) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 4 ms] (28) TRS for Loop Detection (29) DecreasingLoopProof [LOWER BOUND(ID), 203 ms] (30) BEST (31) proven lower bound (32) LowerBoundPropagationProof [FINISHED, 0 ms] (33) BOUNDS(n^1, INF) (34) 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: #EQUAL(z0, z1) -> c21(#EQ(z0, z1)) AND(z0, z1) -> c22(#AND(z0, z1)) EQ(z0, z1) -> c23(EQ#1(z0, z1)) EQ#1(::(z0, z1), z2) -> c24(EQ#3(z2, z0, z1)) EQ#1(nil, z0) -> c25(EQ#2(z0)) EQ#2(::(z0, z1)) -> c26 EQ#2(nil) -> c27 EQ#3(::(z0, z1), z2, z3) -> c28(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0)) EQ#3(::(z0, z1), z2, z3) -> c29(AND(#equal(z2, z0), eq(z3, z1)), EQ(z3, z1)) EQ#3(nil, z0, z1) -> c30 NUB(z0) -> c31(NUB#1(z0)) NUB#1(::(z0, z1)) -> c32(NUB(remove(z0, z1)), REMOVE(z0, z1)) NUB#1(nil) -> c33 REMOVE(z0, z1) -> c34(REMOVE#1(z1, z0)) REMOVE#1(::(z0, z1), z2) -> c35(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) REMOVE#1(nil, z0) -> c36 REMOVE#2(#false, z0, z1, z2) -> c37(REMOVE(z0, z2)) REMOVE#2(#true, z0, z1, z2) -> c38(REMOVE(z0, z2)) The (relative) TRS S consists of the following rules: #AND(#false, #false) -> c #AND(#false, #true) -> c1 #AND(#true, #false) -> c2 #AND(#true, #true) -> c3 #EQ(#0, #0) -> c4 #EQ(#0, #neg(z0)) -> c5 #EQ(#0, #pos(z0)) -> c6 #EQ(#0, #s(z0)) -> c7 #EQ(#neg(z0), #0) -> c8 #EQ(#neg(z0), #neg(z1)) -> c9(#EQ(z0, z1)) #EQ(#neg(z0), #pos(z1)) -> c10 #EQ(#pos(z0), #0) -> c11 #EQ(#pos(z0), #neg(z1)) -> c12 #EQ(#pos(z0), #pos(z1)) -> c13(#EQ(z0, z1)) #EQ(#s(z0), #0) -> c14 #EQ(#s(z0), #s(z1)) -> c15(#EQ(z0, z1)) #EQ(::(z0, z1), ::(z2, z3)) -> c16(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z0, z2)) #EQ(::(z0, z1), ::(z2, z3)) -> c17(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z1, z3)) #EQ(::(z0, z1), nil) -> c18 #EQ(nil, ::(z0, z1)) -> c19 #EQ(nil, nil) -> c20 #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #equal(z0, z1) -> #eq(z0, z1) and(z0, z1) -> #and(z0, z1) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false nub(z0) -> nub#1(z0) nub#1(::(z0, z1)) -> ::(z0, nub(remove(z0, z1))) nub#1(nil) -> nil remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) 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: #EQUAL(z0, z1) -> c21(#EQ(z0, z1)) AND(z0, z1) -> c22(#AND(z0, z1)) EQ(z0, z1) -> c23(EQ#1(z0, z1)) EQ#1(::(z0, z1), z2) -> c24(EQ#3(z2, z0, z1)) EQ#1(nil, z0) -> c25(EQ#2(z0)) EQ#2(::(z0, z1)) -> c26 EQ#2(nil) -> c27 EQ#3(::(z0, z1), z2, z3) -> c28(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0)) EQ#3(::(z0, z1), z2, z3) -> c29(AND(#equal(z2, z0), eq(z3, z1)), EQ(z3, z1)) EQ#3(nil, z0, z1) -> c30 NUB(z0) -> c31(NUB#1(z0)) NUB#1(::(z0, z1)) -> c32(NUB(remove(z0, z1)), REMOVE(z0, z1)) NUB#1(nil) -> c33 REMOVE(z0, z1) -> c34(REMOVE#1(z1, z0)) REMOVE#1(::(z0, z1), z2) -> c35(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) REMOVE#1(nil, z0) -> c36 REMOVE#2(#false, z0, z1, z2) -> c37(REMOVE(z0, z2)) REMOVE#2(#true, z0, z1, z2) -> c38(REMOVE(z0, z2)) The (relative) TRS S consists of the following rules: #AND(#false, #false) -> c #AND(#false, #true) -> c1 #AND(#true, #false) -> c2 #AND(#true, #true) -> c3 #EQ(#0, #0) -> c4 #EQ(#0, #neg(z0)) -> c5 #EQ(#0, #pos(z0)) -> c6 #EQ(#0, #s(z0)) -> c7 #EQ(#neg(z0), #0) -> c8 #EQ(#neg(z0), #neg(z1)) -> c9(#EQ(z0, z1)) #EQ(#neg(z0), #pos(z1)) -> c10 #EQ(#pos(z0), #0) -> c11 #EQ(#pos(z0), #neg(z1)) -> c12 #EQ(#pos(z0), #pos(z1)) -> c13(#EQ(z0, z1)) #EQ(#s(z0), #0) -> c14 #EQ(#s(z0), #s(z1)) -> c15(#EQ(z0, z1)) #EQ(::(z0, z1), ::(z2, z3)) -> c16(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z0, z2)) #EQ(::(z0, z1), ::(z2, z3)) -> c17(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z1, z3)) #EQ(::(z0, z1), nil) -> c18 #EQ(nil, ::(z0, z1)) -> c19 #EQ(nil, nil) -> c20 #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #equal(z0, z1) -> #eq(z0, z1) and(z0, z1) -> #and(z0, z1) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false nub(z0) -> nub#1(z0) nub#1(::(z0, z1)) -> ::(z0, nub(remove(z0, z1))) nub#1(nil) -> nil remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) Rewrite Strategy: INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: #AND(#false, #false) -> c #AND(#false, #true) -> c1 #AND(#true, #false) -> c2 #AND(#true, #true) -> c3 #EQ(#0, #0) -> c4 #EQ(#0, #neg(z0)) -> c5 #EQ(#0, #pos(z0)) -> c6 #EQ(#0, #s(z0)) -> c7 #EQ(#neg(z0), #0) -> c8 #EQ(#neg(z0), #neg(z1)) -> c9(#EQ(z0, z1)) #EQ(#neg(z0), #pos(z1)) -> c10 #EQ(#pos(z0), #0) -> c11 #EQ(#pos(z0), #neg(z1)) -> c12 #EQ(#pos(z0), #pos(z1)) -> c13(#EQ(z0, z1)) #EQ(#s(z0), #0) -> c14 #EQ(#s(z0), #s(z1)) -> c15(#EQ(z0, z1)) #EQ(::(z0, z1), ::(z2, z3)) -> c16(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z0, z2)) #EQ(::(z0, z1), ::(z2, z3)) -> c17(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z1, z3)) #EQ(::(z0, z1), nil) -> c18 #EQ(nil, ::(z0, z1)) -> c19 #EQ(nil, nil) -> c20 #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #equal(z0, z1) -> #eq(z0, z1) and(z0, z1) -> #and(z0, z1) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false nub(z0) -> nub#1(z0) nub#1(::(z0, z1)) -> ::(z0, nub(remove(z0, z1))) nub#1(nil) -> nil remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) #EQUAL(z0, z1) -> c21(#EQ(z0, z1)) AND(z0, z1) -> c22(#AND(z0, z1)) EQ(z0, z1) -> c23(EQ#1(z0, z1)) EQ#1(::(z0, z1), z2) -> c24(EQ#3(z2, z0, z1)) EQ#1(nil, z0) -> c25(EQ#2(z0)) EQ#2(::(z0, z1)) -> c26 EQ#2(nil) -> c27 EQ#3(::(z0, z1), z2, z3) -> c28(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0)) EQ#3(::(z0, z1), z2, z3) -> c29(AND(#equal(z2, z0), eq(z3, z1)), EQ(z3, z1)) EQ#3(nil, z0, z1) -> c30 NUB(z0) -> c31(NUB#1(z0)) NUB#1(::(z0, z1)) -> c32(NUB(remove(z0, z1)), REMOVE(z0, z1)) NUB#1(nil) -> c33 REMOVE(z0, z1) -> c34(REMOVE#1(z1, z0)) REMOVE#1(::(z0, z1), z2) -> c35(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) REMOVE#1(nil, z0) -> c36 REMOVE#2(#false, z0, z1, z2) -> c37(REMOVE(z0, z2)) REMOVE#2(#true, z0, z1, z2) -> c38(REMOVE(z0, z2)) Tuples: #AND'(#false, #false) -> c39 #AND'(#false, #true) -> c40 #AND'(#true, #false) -> c41 #AND'(#true, #true) -> c42 #EQ'(#0, #0) -> c43 #EQ'(#0, #neg(z0)) -> c44 #EQ'(#0, #pos(z0)) -> c45 #EQ'(#0, #s(z0)) -> c46 #EQ'(#neg(z0), #0) -> c47 #EQ'(#neg(z0), #neg(z1)) -> c48(#EQ'(z0, z1)) #EQ'(#neg(z0), #pos(z1)) -> c49 #EQ'(#pos(z0), #0) -> c50 #EQ'(#pos(z0), #neg(z1)) -> c51 #EQ'(#pos(z0), #pos(z1)) -> c52(#EQ'(z0, z1)) #EQ'(#s(z0), #0) -> c53 #EQ'(#s(z0), #s(z1)) -> c54(#EQ'(z0, z1)) #EQ'(::(z0, z1), ::(z2, z3)) -> c55(#AND'(#eq(z0, z2), #eq(z1, z3)), #EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c56(#AND'(#eq(z0, z2), #eq(z1, z3)), #EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z1, z3)) #EQ'(::(z0, z1), nil) -> c57 #EQ'(nil, ::(z0, z1)) -> c58 #EQ'(nil, nil) -> c59 #AND''(#false, #false) -> c60 #AND''(#false, #true) -> c61 #AND''(#true, #false) -> c62 #AND''(#true, #true) -> c63 #EQ''(#0, #0) -> c64 #EQ''(#0, #neg(z0)) -> c65 #EQ''(#0, #pos(z0)) -> c66 #EQ''(#0, #s(z0)) -> c67 #EQ''(#neg(z0), #0) -> c68 #EQ''(#neg(z0), #neg(z1)) -> c69(#EQ''(z0, z1)) #EQ''(#neg(z0), #pos(z1)) -> c70 #EQ''(#pos(z0), #0) -> c71 #EQ''(#pos(z0), #neg(z1)) -> c72 #EQ''(#pos(z0), #pos(z1)) -> c73(#EQ''(z0, z1)) #EQ''(#s(z0), #0) -> c74 #EQ''(#s(z0), #s(z1)) -> c75(#EQ''(z0, z1)) #EQ''(::(z0, z1), ::(z2, z3)) -> c76(#AND''(#eq(z0, z2), #eq(z1, z3)), #EQ''(z0, z2), #EQ''(z1, z3)) #EQ''(::(z0, z1), nil) -> c77 #EQ''(nil, ::(z0, z1)) -> c78 #EQ''(nil, nil) -> c79 #EQUAL'(z0, z1) -> c80(#EQ''(z0, z1)) AND'(z0, z1) -> c81(#AND''(z0, z1)) EQ'(z0, z1) -> c82(EQ#1'(z0, z1)) EQ#1'(::(z0, z1), z2) -> c83(EQ#3'(z2, z0, z1)) EQ#1'(nil, z0) -> c84(EQ#2'(z0)) EQ#2'(::(z0, z1)) -> c85 EQ#2'(nil) -> c86 EQ#3'(::(z0, z1), z2, z3) -> c87(AND'(#equal(z2, z0), eq(z3, z1)), #EQUAL'(z2, z0), EQ'(z3, z1)) EQ#3'(nil, z0, z1) -> c88 NUB'(z0) -> c89(NUB#1'(z0)) NUB#1'(::(z0, z1)) -> c90(NUB'(remove(z0, z1)), REMOVE'(z0, z1)) NUB#1'(nil) -> c91 REMOVE'(z0, z1) -> c92(REMOVE#1'(z1, z0)) REMOVE#1'(::(z0, z1), z2) -> c93(REMOVE#2'(eq(z2, z0), z2, z0, z1), EQ'(z2, z0)) REMOVE#1'(nil, z0) -> c94 REMOVE#2'(#false, z0, z1, z2) -> c95(REMOVE'(z0, z2)) REMOVE#2'(#true, z0, z1, z2) -> c96(REMOVE'(z0, z2)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) AND''(z0, z1) -> c98(#AND'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) EQ#1''(nil, z0) -> c101(EQ#2''(z0)) EQ#2''(::(z0, z1)) -> c102 EQ#2''(nil) -> c103 EQ#3''(::(z0, z1), z2, z3) -> c104(AND''(#equal(z2, z0), eq(z3, z1)), #EQUAL'(z2, z0), EQ'(z3, z1), #EQUAL''(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c105(AND''(#equal(z2, z0), eq(z3, z1)), #EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(nil, z0, z1) -> c106 NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) NUB#1''(nil) -> c109 REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#1''(nil, z0) -> c112 REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) S tuples: #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) AND''(z0, z1) -> c98(#AND'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) EQ#1''(nil, z0) -> c101(EQ#2''(z0)) EQ#2''(::(z0, z1)) -> c102 EQ#2''(nil) -> c103 EQ#3''(::(z0, z1), z2, z3) -> c104(AND''(#equal(z2, z0), eq(z3, z1)), #EQUAL'(z2, z0), EQ'(z3, z1), #EQUAL''(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c105(AND''(#equal(z2, z0), eq(z3, z1)), #EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(nil, z0, z1) -> c106 NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) NUB#1''(nil) -> c109 REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#1''(nil, z0) -> c112 REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) K tuples:none Defined Rule Symbols: #EQUAL_2, AND_2, EQ_2, EQ#1_2, EQ#2_1, EQ#3_3, NUB_1, NUB#1_1, REMOVE_2, REMOVE#1_2, REMOVE#2_4, #AND_2, #EQ_2, #and_2, #eq_2, #equal_2, and_2, eq_2, eq#1_2, eq#2_1, eq#3_3, nub_1, nub#1_1, remove_2, remove#1_2, remove#2_4 Defined Pair Symbols: #AND'_2, #EQ'_2, #AND''_2, #EQ''_2, #EQUAL'_2, AND'_2, EQ'_2, EQ#1'_2, EQ#2'_1, EQ#3'_3, NUB'_1, NUB#1'_1, REMOVE'_2, REMOVE#1'_2, REMOVE#2'_4, #EQUAL''_2, AND''_2, EQ''_2, EQ#1''_2, EQ#2''_1, EQ#3''_3, NUB''_1, NUB#1''_1, REMOVE''_2, REMOVE#1''_2, REMOVE#2''_4 Compound Symbols: c39, c40, c41, c42, c43, c44, c45, c46, c47, c48_1, c49, c50, c51, c52_1, c53, c54_1, c55_4, c56_4, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c67, c68, c69_1, c70, c71, c72, c73_1, c74, c75_1, c76_3, c77, c78, c79, c80_1, c81_1, c82_1, c83_1, c84_1, c85, c86, c87_3, c88, c89_1, c90_2, c91, c92_1, c93_2, c94, c95_1, c96_1, c97_1, c98_1, c99_1, c100_1, c101_1, c102, c103, c104_4, c105_4, c106, c107_1, c108_3, c109, c110_1, c111_3, c112, c113_1, c114_1 ---------------------------------------- (5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 46 trailing nodes: #EQ''(#0, #0) -> c64 #EQ''(nil, ::(z0, z1)) -> c78 EQ#2''(nil) -> c103 #EQ'(#neg(z0), #pos(z1)) -> c49 AND'(z0, z1) -> c81(#AND''(z0, z1)) #EQ'(::(z0, z1), nil) -> c57 #EQ'(nil, ::(z0, z1)) -> c58 EQ#3''(nil, z0, z1) -> c106 #AND''(#true, #true) -> c63 #EQ'(#0, #pos(z0)) -> c45 EQ#3'(nil, z0, z1) -> c88 #EQ''(#s(z0), #0) -> c74 #EQ''(#neg(z0), #0) -> c68 #EQ''(::(z0, z1), nil) -> c77 #EQ''(#pos(z0), #0) -> c71 #AND''(#false, #true) -> c61 #EQ'(#pos(z0), #0) -> c50 #EQ'(nil, nil) -> c59 #EQ'(#0, #neg(z0)) -> c44 EQ#1''(nil, z0) -> c101(EQ#2''(z0)) #EQ''(#pos(z0), #neg(z1)) -> c72 #EQ''(#neg(z0), #pos(z1)) -> c70 #EQ''(#0, #pos(z0)) -> c66 REMOVE#1''(nil, z0) -> c112 #EQ'(#neg(z0), #0) -> c47 #EQ'(#0, #0) -> c43 #EQ''(#0, #neg(z0)) -> c65 #EQ'(#s(z0), #0) -> c53 #EQ'(#0, #s(z0)) -> c46 REMOVE#1'(nil, z0) -> c94 EQ#2'(nil) -> c86 EQ#1'(nil, z0) -> c84(EQ#2'(z0)) #AND'(#false, #false) -> c39 #AND'(#true, #true) -> c42 #AND'(#true, #false) -> c41 EQ#2'(::(z0, z1)) -> c85 NUB#1''(nil) -> c109 EQ#2''(::(z0, z1)) -> c102 #EQ''(#0, #s(z0)) -> c67 #AND'(#false, #true) -> c40 #EQ''(nil, nil) -> c79 #AND''(#true, #false) -> c62 #AND''(#false, #false) -> c60 #EQ'(#pos(z0), #neg(z1)) -> c51 NUB#1'(nil) -> c91 AND''(z0, z1) -> c98(#AND'(z0, z1)) ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: #AND(#false, #false) -> c #AND(#false, #true) -> c1 #AND(#true, #false) -> c2 #AND(#true, #true) -> c3 #EQ(#0, #0) -> c4 #EQ(#0, #neg(z0)) -> c5 #EQ(#0, #pos(z0)) -> c6 #EQ(#0, #s(z0)) -> c7 #EQ(#neg(z0), #0) -> c8 #EQ(#neg(z0), #neg(z1)) -> c9(#EQ(z0, z1)) #EQ(#neg(z0), #pos(z1)) -> c10 #EQ(#pos(z0), #0) -> c11 #EQ(#pos(z0), #neg(z1)) -> c12 #EQ(#pos(z0), #pos(z1)) -> c13(#EQ(z0, z1)) #EQ(#s(z0), #0) -> c14 #EQ(#s(z0), #s(z1)) -> c15(#EQ(z0, z1)) #EQ(::(z0, z1), ::(z2, z3)) -> c16(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z0, z2)) #EQ(::(z0, z1), ::(z2, z3)) -> c17(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z1, z3)) #EQ(::(z0, z1), nil) -> c18 #EQ(nil, ::(z0, z1)) -> c19 #EQ(nil, nil) -> c20 #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #equal(z0, z1) -> #eq(z0, z1) and(z0, z1) -> #and(z0, z1) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false nub(z0) -> nub#1(z0) nub#1(::(z0, z1)) -> ::(z0, nub(remove(z0, z1))) nub#1(nil) -> nil remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) #EQUAL(z0, z1) -> c21(#EQ(z0, z1)) AND(z0, z1) -> c22(#AND(z0, z1)) EQ(z0, z1) -> c23(EQ#1(z0, z1)) EQ#1(::(z0, z1), z2) -> c24(EQ#3(z2, z0, z1)) EQ#1(nil, z0) -> c25(EQ#2(z0)) EQ#2(::(z0, z1)) -> c26 EQ#2(nil) -> c27 EQ#3(::(z0, z1), z2, z3) -> c28(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0)) EQ#3(::(z0, z1), z2, z3) -> c29(AND(#equal(z2, z0), eq(z3, z1)), EQ(z3, z1)) EQ#3(nil, z0, z1) -> c30 NUB(z0) -> c31(NUB#1(z0)) NUB#1(::(z0, z1)) -> c32(NUB(remove(z0, z1)), REMOVE(z0, z1)) NUB#1(nil) -> c33 REMOVE(z0, z1) -> c34(REMOVE#1(z1, z0)) REMOVE#1(::(z0, z1), z2) -> c35(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) REMOVE#1(nil, z0) -> c36 REMOVE#2(#false, z0, z1, z2) -> c37(REMOVE(z0, z2)) REMOVE#2(#true, z0, z1, z2) -> c38(REMOVE(z0, z2)) Tuples: #EQ'(#neg(z0), #neg(z1)) -> c48(#EQ'(z0, z1)) #EQ'(#pos(z0), #pos(z1)) -> c52(#EQ'(z0, z1)) #EQ'(#s(z0), #s(z1)) -> c54(#EQ'(z0, z1)) #EQ'(::(z0, z1), ::(z2, z3)) -> c55(#AND'(#eq(z0, z2), #eq(z1, z3)), #EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c56(#AND'(#eq(z0, z2), #eq(z1, z3)), #EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z1, z3)) #EQ''(#neg(z0), #neg(z1)) -> c69(#EQ''(z0, z1)) #EQ''(#pos(z0), #pos(z1)) -> c73(#EQ''(z0, z1)) #EQ''(#s(z0), #s(z1)) -> c75(#EQ''(z0, z1)) #EQ''(::(z0, z1), ::(z2, z3)) -> c76(#AND''(#eq(z0, z2), #eq(z1, z3)), #EQ''(z0, z2), #EQ''(z1, z3)) #EQUAL'(z0, z1) -> c80(#EQ''(z0, z1)) EQ'(z0, z1) -> c82(EQ#1'(z0, z1)) EQ#1'(::(z0, z1), z2) -> c83(EQ#3'(z2, z0, z1)) EQ#3'(::(z0, z1), z2, z3) -> c87(AND'(#equal(z2, z0), eq(z3, z1)), #EQUAL'(z2, z0), EQ'(z3, z1)) NUB'(z0) -> c89(NUB#1'(z0)) NUB#1'(::(z0, z1)) -> c90(NUB'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, z1) -> c92(REMOVE#1'(z1, z0)) REMOVE#1'(::(z0, z1), z2) -> c93(REMOVE#2'(eq(z2, z0), z2, z0, z1), EQ'(z2, z0)) REMOVE#2'(#false, z0, z1, z2) -> c95(REMOVE'(z0, z2)) REMOVE#2'(#true, z0, z1, z2) -> c96(REMOVE'(z0, z2)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) EQ#3''(::(z0, z1), z2, z3) -> c104(AND''(#equal(z2, z0), eq(z3, z1)), #EQUAL'(z2, z0), EQ'(z3, z1), #EQUAL''(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c105(AND''(#equal(z2, z0), eq(z3, z1)), #EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) S tuples: #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) EQ#3''(::(z0, z1), z2, z3) -> c104(AND''(#equal(z2, z0), eq(z3, z1)), #EQUAL'(z2, z0), EQ'(z3, z1), #EQUAL''(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c105(AND''(#equal(z2, z0), eq(z3, z1)), #EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) K tuples:none Defined Rule Symbols: #EQUAL_2, AND_2, EQ_2, EQ#1_2, EQ#2_1, EQ#3_3, NUB_1, NUB#1_1, REMOVE_2, REMOVE#1_2, REMOVE#2_4, #AND_2, #EQ_2, #and_2, #eq_2, #equal_2, and_2, eq_2, eq#1_2, eq#2_1, eq#3_3, nub_1, nub#1_1, remove_2, remove#1_2, remove#2_4 Defined Pair Symbols: #EQ'_2, #EQ''_2, #EQUAL'_2, EQ'_2, EQ#1'_2, EQ#3'_3, NUB'_1, NUB#1'_1, REMOVE'_2, REMOVE#1'_2, REMOVE#2'_4, #EQUAL''_2, EQ''_2, EQ#1''_2, EQ#3''_3, NUB''_1, NUB#1''_1, REMOVE''_2, REMOVE#1''_2, REMOVE#2''_4 Compound Symbols: c48_1, c52_1, c54_1, c55_4, c56_4, c69_1, c73_1, c75_1, c76_3, c80_1, c82_1, c83_1, c87_3, c89_1, c90_2, c92_1, c93_2, c95_1, c96_1, c97_1, c99_1, c100_1, c104_4, c105_4, c107_1, c108_3, c110_1, c111_3, c113_1, c114_1 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 6 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: #AND(#false, #false) -> c #AND(#false, #true) -> c1 #AND(#true, #false) -> c2 #AND(#true, #true) -> c3 #EQ(#0, #0) -> c4 #EQ(#0, #neg(z0)) -> c5 #EQ(#0, #pos(z0)) -> c6 #EQ(#0, #s(z0)) -> c7 #EQ(#neg(z0), #0) -> c8 #EQ(#neg(z0), #neg(z1)) -> c9(#EQ(z0, z1)) #EQ(#neg(z0), #pos(z1)) -> c10 #EQ(#pos(z0), #0) -> c11 #EQ(#pos(z0), #neg(z1)) -> c12 #EQ(#pos(z0), #pos(z1)) -> c13(#EQ(z0, z1)) #EQ(#s(z0), #0) -> c14 #EQ(#s(z0), #s(z1)) -> c15(#EQ(z0, z1)) #EQ(::(z0, z1), ::(z2, z3)) -> c16(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z0, z2)) #EQ(::(z0, z1), ::(z2, z3)) -> c17(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z1, z3)) #EQ(::(z0, z1), nil) -> c18 #EQ(nil, ::(z0, z1)) -> c19 #EQ(nil, nil) -> c20 #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #equal(z0, z1) -> #eq(z0, z1) and(z0, z1) -> #and(z0, z1) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false nub(z0) -> nub#1(z0) nub#1(::(z0, z1)) -> ::(z0, nub(remove(z0, z1))) nub#1(nil) -> nil remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) #EQUAL(z0, z1) -> c21(#EQ(z0, z1)) AND(z0, z1) -> c22(#AND(z0, z1)) EQ(z0, z1) -> c23(EQ#1(z0, z1)) EQ#1(::(z0, z1), z2) -> c24(EQ#3(z2, z0, z1)) EQ#1(nil, z0) -> c25(EQ#2(z0)) EQ#2(::(z0, z1)) -> c26 EQ#2(nil) -> c27 EQ#3(::(z0, z1), z2, z3) -> c28(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0)) EQ#3(::(z0, z1), z2, z3) -> c29(AND(#equal(z2, z0), eq(z3, z1)), EQ(z3, z1)) EQ#3(nil, z0, z1) -> c30 NUB(z0) -> c31(NUB#1(z0)) NUB#1(::(z0, z1)) -> c32(NUB(remove(z0, z1)), REMOVE(z0, z1)) NUB#1(nil) -> c33 REMOVE(z0, z1) -> c34(REMOVE#1(z1, z0)) REMOVE#1(::(z0, z1), z2) -> c35(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) REMOVE#1(nil, z0) -> c36 REMOVE#2(#false, z0, z1, z2) -> c37(REMOVE(z0, z2)) REMOVE#2(#true, z0, z1, z2) -> c38(REMOVE(z0, z2)) Tuples: #EQ'(#neg(z0), #neg(z1)) -> c48(#EQ'(z0, z1)) #EQ'(#pos(z0), #pos(z1)) -> c52(#EQ'(z0, z1)) #EQ'(#s(z0), #s(z1)) -> c54(#EQ'(z0, z1)) #EQ''(#neg(z0), #neg(z1)) -> c69(#EQ''(z0, z1)) #EQ''(#pos(z0), #pos(z1)) -> c73(#EQ''(z0, z1)) #EQ''(#s(z0), #s(z1)) -> c75(#EQ''(z0, z1)) #EQUAL'(z0, z1) -> c80(#EQ''(z0, z1)) EQ'(z0, z1) -> c82(EQ#1'(z0, z1)) EQ#1'(::(z0, z1), z2) -> c83(EQ#3'(z2, z0, z1)) NUB'(z0) -> c89(NUB#1'(z0)) NUB#1'(::(z0, z1)) -> c90(NUB'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, z1) -> c92(REMOVE#1'(z1, z0)) REMOVE#1'(::(z0, z1), z2) -> c93(REMOVE#2'(eq(z2, z0), z2, z0, z1), EQ'(z2, z0)) REMOVE#2'(#false, z0, z1, z2) -> c95(REMOVE'(z0, z2)) REMOVE#2'(#true, z0, z1, z2) -> c96(REMOVE'(z0, z2)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c55(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c56(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z1, z3)) #EQ''(::(z0, z1), ::(z2, z3)) -> c76(#EQ''(z0, z2), #EQ''(z1, z3)) EQ#3'(::(z0, z1), z2, z3) -> c87(#EQUAL'(z2, z0), EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c104(#EQUAL'(z2, z0), EQ'(z3, z1), #EQUAL''(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) S tuples: #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) EQ#3''(::(z0, z1), z2, z3) -> c104(#EQUAL'(z2, z0), EQ'(z3, z1), #EQUAL''(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) K tuples:none Defined Rule Symbols: #EQUAL_2, AND_2, EQ_2, EQ#1_2, EQ#2_1, EQ#3_3, NUB_1, NUB#1_1, REMOVE_2, REMOVE#1_2, REMOVE#2_4, #AND_2, #EQ_2, #and_2, #eq_2, #equal_2, and_2, eq_2, eq#1_2, eq#2_1, eq#3_3, nub_1, nub#1_1, remove_2, remove#1_2, remove#2_4 Defined Pair Symbols: #EQ'_2, #EQ''_2, #EQUAL'_2, EQ'_2, EQ#1'_2, NUB'_1, NUB#1'_1, REMOVE'_2, REMOVE#1'_2, REMOVE#2'_4, #EQUAL''_2, EQ''_2, EQ#1''_2, NUB''_1, NUB#1''_1, REMOVE''_2, REMOVE#1''_2, REMOVE#2''_4, EQ#3'_3, EQ#3''_3 Compound Symbols: c48_1, c52_1, c54_1, c69_1, c73_1, c75_1, c80_1, c82_1, c83_1, c89_1, c90_2, c92_1, c93_2, c95_1, c96_1, c97_1, c99_1, c100_1, c107_1, c108_3, c110_1, c111_3, c113_1, c114_1, c55_3, c56_3, c76_2, c87_2, c104_3, c105_3 ---------------------------------------- (9) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID)) Split RHS of tuples not part of any SCC ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: #AND(#false, #false) -> c #AND(#false, #true) -> c1 #AND(#true, #false) -> c2 #AND(#true, #true) -> c3 #EQ(#0, #0) -> c4 #EQ(#0, #neg(z0)) -> c5 #EQ(#0, #pos(z0)) -> c6 #EQ(#0, #s(z0)) -> c7 #EQ(#neg(z0), #0) -> c8 #EQ(#neg(z0), #neg(z1)) -> c9(#EQ(z0, z1)) #EQ(#neg(z0), #pos(z1)) -> c10 #EQ(#pos(z0), #0) -> c11 #EQ(#pos(z0), #neg(z1)) -> c12 #EQ(#pos(z0), #pos(z1)) -> c13(#EQ(z0, z1)) #EQ(#s(z0), #0) -> c14 #EQ(#s(z0), #s(z1)) -> c15(#EQ(z0, z1)) #EQ(::(z0, z1), ::(z2, z3)) -> c16(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z0, z2)) #EQ(::(z0, z1), ::(z2, z3)) -> c17(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z1, z3)) #EQ(::(z0, z1), nil) -> c18 #EQ(nil, ::(z0, z1)) -> c19 #EQ(nil, nil) -> c20 #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #equal(z0, z1) -> #eq(z0, z1) and(z0, z1) -> #and(z0, z1) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false nub(z0) -> nub#1(z0) nub#1(::(z0, z1)) -> ::(z0, nub(remove(z0, z1))) nub#1(nil) -> nil remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) #EQUAL(z0, z1) -> c21(#EQ(z0, z1)) AND(z0, z1) -> c22(#AND(z0, z1)) EQ(z0, z1) -> c23(EQ#1(z0, z1)) EQ#1(::(z0, z1), z2) -> c24(EQ#3(z2, z0, z1)) EQ#1(nil, z0) -> c25(EQ#2(z0)) EQ#2(::(z0, z1)) -> c26 EQ#2(nil) -> c27 EQ#3(::(z0, z1), z2, z3) -> c28(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0)) EQ#3(::(z0, z1), z2, z3) -> c29(AND(#equal(z2, z0), eq(z3, z1)), EQ(z3, z1)) EQ#3(nil, z0, z1) -> c30 NUB(z0) -> c31(NUB#1(z0)) NUB#1(::(z0, z1)) -> c32(NUB(remove(z0, z1)), REMOVE(z0, z1)) NUB#1(nil) -> c33 REMOVE(z0, z1) -> c34(REMOVE#1(z1, z0)) REMOVE#1(::(z0, z1), z2) -> c35(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) REMOVE#1(nil, z0) -> c36 REMOVE#2(#false, z0, z1, z2) -> c37(REMOVE(z0, z2)) REMOVE#2(#true, z0, z1, z2) -> c38(REMOVE(z0, z2)) Tuples: #EQ'(#neg(z0), #neg(z1)) -> c48(#EQ'(z0, z1)) #EQ'(#pos(z0), #pos(z1)) -> c52(#EQ'(z0, z1)) #EQ'(#s(z0), #s(z1)) -> c54(#EQ'(z0, z1)) #EQ''(#neg(z0), #neg(z1)) -> c69(#EQ''(z0, z1)) #EQ''(#pos(z0), #pos(z1)) -> c73(#EQ''(z0, z1)) #EQ''(#s(z0), #s(z1)) -> c75(#EQ''(z0, z1)) #EQUAL'(z0, z1) -> c80(#EQ''(z0, z1)) EQ'(z0, z1) -> c82(EQ#1'(z0, z1)) EQ#1'(::(z0, z1), z2) -> c83(EQ#3'(z2, z0, z1)) NUB'(z0) -> c89(NUB#1'(z0)) NUB#1'(::(z0, z1)) -> c90(NUB'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, z1) -> c92(REMOVE#1'(z1, z0)) REMOVE#1'(::(z0, z1), z2) -> c93(REMOVE#2'(eq(z2, z0), z2, z0, z1), EQ'(z2, z0)) REMOVE#2'(#false, z0, z1, z2) -> c95(REMOVE'(z0, z2)) REMOVE#2'(#true, z0, z1, z2) -> c96(REMOVE'(z0, z2)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c55(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c56(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z1, z3)) #EQ''(::(z0, z1), ::(z2, z3)) -> c76(#EQ''(z0, z2), #EQ''(z1, z3)) EQ#3'(::(z0, z1), z2, z3) -> c87(#EQUAL'(z2, z0), EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) S tuples: #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) K tuples:none Defined Rule Symbols: #EQUAL_2, AND_2, EQ_2, EQ#1_2, EQ#2_1, EQ#3_3, NUB_1, NUB#1_1, REMOVE_2, REMOVE#1_2, REMOVE#2_4, #AND_2, #EQ_2, #and_2, #eq_2, #equal_2, and_2, eq_2, eq#1_2, eq#2_1, eq#3_3, nub_1, nub#1_1, remove_2, remove#1_2, remove#2_4 Defined Pair Symbols: #EQ'_2, #EQ''_2, #EQUAL'_2, EQ'_2, EQ#1'_2, NUB'_1, NUB#1'_1, REMOVE'_2, REMOVE#1'_2, REMOVE#2'_4, #EQUAL''_2, EQ''_2, EQ#1''_2, NUB''_1, NUB#1''_1, REMOVE''_2, REMOVE#1''_2, REMOVE#2''_4, EQ#3'_3, EQ#3''_3 Compound Symbols: c48_1, c52_1, c54_1, c69_1, c73_1, c75_1, c80_1, c82_1, c83_1, c89_1, c90_2, c92_1, c93_2, c95_1, c96_1, c97_1, c99_1, c100_1, c107_1, c108_3, c110_1, c111_3, c113_1, c114_1, c55_3, c56_3, c76_2, c87_2, c105_3, c39_1 ---------------------------------------- (11) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: #AND(#false, #false) -> c #AND(#false, #true) -> c1 #AND(#true, #false) -> c2 #AND(#true, #true) -> c3 #EQ(#0, #0) -> c4 #EQ(#0, #neg(z0)) -> c5 #EQ(#0, #pos(z0)) -> c6 #EQ(#0, #s(z0)) -> c7 #EQ(#neg(z0), #0) -> c8 #EQ(#neg(z0), #neg(z1)) -> c9(#EQ(z0, z1)) #EQ(#neg(z0), #pos(z1)) -> c10 #EQ(#pos(z0), #0) -> c11 #EQ(#pos(z0), #neg(z1)) -> c12 #EQ(#pos(z0), #pos(z1)) -> c13(#EQ(z0, z1)) #EQ(#s(z0), #0) -> c14 #EQ(#s(z0), #s(z1)) -> c15(#EQ(z0, z1)) #EQ(::(z0, z1), ::(z2, z3)) -> c16(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z0, z2)) #EQ(::(z0, z1), ::(z2, z3)) -> c17(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z1, z3)) #EQ(::(z0, z1), nil) -> c18 #EQ(nil, ::(z0, z1)) -> c19 #EQ(nil, nil) -> c20 nub(z0) -> nub#1(z0) nub#1(::(z0, z1)) -> ::(z0, nub(remove(z0, z1))) nub#1(nil) -> nil #EQUAL(z0, z1) -> c21(#EQ(z0, z1)) AND(z0, z1) -> c22(#AND(z0, z1)) EQ(z0, z1) -> c23(EQ#1(z0, z1)) EQ#1(::(z0, z1), z2) -> c24(EQ#3(z2, z0, z1)) EQ#1(nil, z0) -> c25(EQ#2(z0)) EQ#2(::(z0, z1)) -> c26 EQ#2(nil) -> c27 EQ#3(::(z0, z1), z2, z3) -> c28(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0)) EQ#3(::(z0, z1), z2, z3) -> c29(AND(#equal(z2, z0), eq(z3, z1)), EQ(z3, z1)) EQ#3(nil, z0, z1) -> c30 NUB(z0) -> c31(NUB#1(z0)) NUB#1(::(z0, z1)) -> c32(NUB(remove(z0, z1)), REMOVE(z0, z1)) NUB#1(nil) -> c33 REMOVE(z0, z1) -> c34(REMOVE#1(z1, z0)) REMOVE#1(::(z0, z1), z2) -> c35(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) REMOVE#1(nil, z0) -> c36 REMOVE#2(#false, z0, z1, z2) -> c37(REMOVE(z0, z2)) REMOVE#2(#true, z0, z1, z2) -> c38(REMOVE(z0, z2)) ---------------------------------------- (12) Obligation: Complexity Dependency Tuples Problem Rules: remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false and(z0, z1) -> #and(z0, z1) #equal(z0, z1) -> #eq(z0, z1) #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true Tuples: #EQ'(#neg(z0), #neg(z1)) -> c48(#EQ'(z0, z1)) #EQ'(#pos(z0), #pos(z1)) -> c52(#EQ'(z0, z1)) #EQ'(#s(z0), #s(z1)) -> c54(#EQ'(z0, z1)) #EQ''(#neg(z0), #neg(z1)) -> c69(#EQ''(z0, z1)) #EQ''(#pos(z0), #pos(z1)) -> c73(#EQ''(z0, z1)) #EQ''(#s(z0), #s(z1)) -> c75(#EQ''(z0, z1)) #EQUAL'(z0, z1) -> c80(#EQ''(z0, z1)) EQ'(z0, z1) -> c82(EQ#1'(z0, z1)) EQ#1'(::(z0, z1), z2) -> c83(EQ#3'(z2, z0, z1)) NUB'(z0) -> c89(NUB#1'(z0)) NUB#1'(::(z0, z1)) -> c90(NUB'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, z1) -> c92(REMOVE#1'(z1, z0)) REMOVE#1'(::(z0, z1), z2) -> c93(REMOVE#2'(eq(z2, z0), z2, z0, z1), EQ'(z2, z0)) REMOVE#2'(#false, z0, z1, z2) -> c95(REMOVE'(z0, z2)) REMOVE#2'(#true, z0, z1, z2) -> c96(REMOVE'(z0, z2)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c55(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c56(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z1, z3)) #EQ''(::(z0, z1), ::(z2, z3)) -> c76(#EQ''(z0, z2), #EQ''(z1, z3)) EQ#3'(::(z0, z1), z2, z3) -> c87(#EQUAL'(z2, z0), EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) S tuples: #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) K tuples:none Defined Rule Symbols: remove_2, remove#1_2, remove#2_4, eq_2, eq#1_2, eq#3_3, and_2, #equal_2, #eq_2, #and_2, eq#2_1 Defined Pair Symbols: #EQ'_2, #EQ''_2, #EQUAL'_2, EQ'_2, EQ#1'_2, NUB'_1, NUB#1'_1, REMOVE'_2, REMOVE#1'_2, REMOVE#2'_4, #EQUAL''_2, EQ''_2, EQ#1''_2, NUB''_1, NUB#1''_1, REMOVE''_2, REMOVE#1''_2, REMOVE#2''_4, EQ#3'_3, EQ#3''_3 Compound Symbols: c48_1, c52_1, c54_1, c69_1, c73_1, c75_1, c80_1, c82_1, c83_1, c89_1, c90_2, c92_1, c93_2, c95_1, c96_1, c97_1, c99_1, c100_1, c107_1, c108_3, c110_1, c111_3, c113_1, c114_1, c55_3, c56_3, c76_2, c87_2, c105_3, c39_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. NUB''(z0) -> c107(NUB#1''(z0)) We considered the (Usable) Rules: remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove(z0, z1) -> remove#1(z1, z0) remove#1(nil, z0) -> nil And the Tuples: #EQ'(#neg(z0), #neg(z1)) -> c48(#EQ'(z0, z1)) #EQ'(#pos(z0), #pos(z1)) -> c52(#EQ'(z0, z1)) #EQ'(#s(z0), #s(z1)) -> c54(#EQ'(z0, z1)) #EQ''(#neg(z0), #neg(z1)) -> c69(#EQ''(z0, z1)) #EQ''(#pos(z0), #pos(z1)) -> c73(#EQ''(z0, z1)) #EQ''(#s(z0), #s(z1)) -> c75(#EQ''(z0, z1)) #EQUAL'(z0, z1) -> c80(#EQ''(z0, z1)) EQ'(z0, z1) -> c82(EQ#1'(z0, z1)) EQ#1'(::(z0, z1), z2) -> c83(EQ#3'(z2, z0, z1)) NUB'(z0) -> c89(NUB#1'(z0)) NUB#1'(::(z0, z1)) -> c90(NUB'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, z1) -> c92(REMOVE#1'(z1, z0)) REMOVE#1'(::(z0, z1), z2) -> c93(REMOVE#2'(eq(z2, z0), z2, z0, z1), EQ'(z2, z0)) REMOVE#2'(#false, z0, z1, z2) -> c95(REMOVE'(z0, z2)) REMOVE#2'(#true, z0, z1, z2) -> c96(REMOVE'(z0, z2)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c55(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c56(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z1, z3)) #EQ''(::(z0, z1), ::(z2, z3)) -> c76(#EQ''(z0, z2), #EQ''(z1, z3)) EQ#3'(::(z0, z1), z2, z3) -> c87(#EQUAL'(z2, z0), EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) 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(#EQUAL'(x_1, x_2)) = 0 POL(#EQUAL''(x_1, x_2)) = 0 POL(#and(x_1, x_2)) = [1] POL(#eq(x_1, x_2)) = [1] + x_1 + x_2 POL(#equal(x_1, x_2)) = [1] + x_1 + x_2 POL(#false) = 0 POL(#neg(x_1)) = [1] + x_1 POL(#pos(x_1)) = [1] + x_1 POL(#s(x_1)) = [1] + x_1 POL(#true) = 0 POL(::(x_1, x_2)) = [1] + x_1 + x_2 POL(EQ#1'(x_1, x_2)) = 0 POL(EQ#1''(x_1, x_2)) = 0 POL(EQ#3'(x_1, x_2, x_3)) = 0 POL(EQ#3''(x_1, x_2, x_3)) = 0 POL(EQ'(x_1, x_2)) = 0 POL(EQ''(x_1, x_2)) = 0 POL(NUB#1'(x_1)) = [1] POL(NUB#1''(x_1)) = x_1 POL(NUB'(x_1)) = [1] POL(NUB''(x_1)) = [1] + x_1 POL(REMOVE#1'(x_1, x_2)) = 0 POL(REMOVE#1''(x_1, x_2)) = 0 POL(REMOVE#2'(x_1, x_2, x_3, x_4)) = 0 POL(REMOVE#2''(x_1, x_2, x_3, x_4)) = 0 POL(REMOVE'(x_1, x_2)) = 0 POL(REMOVE''(x_1, x_2)) = 0 POL(and(x_1, x_2)) = [1] + x_1 POL(c100(x_1)) = x_1 POL(c105(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c107(x_1)) = x_1 POL(c108(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c110(x_1)) = x_1 POL(c111(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c113(x_1)) = x_1 POL(c114(x_1)) = x_1 POL(c39(x_1)) = x_1 POL(c48(x_1)) = x_1 POL(c52(x_1)) = x_1 POL(c54(x_1)) = x_1 POL(c55(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c56(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c69(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1, x_2)) = x_1 + x_2 POL(c80(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(c83(x_1)) = x_1 POL(c87(x_1, x_2)) = x_1 + x_2 POL(c89(x_1)) = x_1 POL(c90(x_1, x_2)) = x_1 + x_2 POL(c92(x_1)) = x_1 POL(c93(x_1, x_2)) = x_1 + x_2 POL(c95(x_1)) = x_1 POL(c96(x_1)) = x_1 POL(c97(x_1)) = x_1 POL(c99(x_1)) = x_1 POL(eq(x_1, x_2)) = x_1 + x_2 POL(eq#1(x_1, x_2)) = [1] + x_1 + x_2 POL(eq#2(x_1)) = [1] + x_1 POL(eq#3(x_1, x_2, x_3)) = [1] + x_1 + x_2 + x_3 POL(nil) = [1] POL(remove(x_1, x_2)) = x_1 + x_2 POL(remove#1(x_1, x_2)) = x_1 + x_2 POL(remove#2(x_1, x_2, x_3, x_4)) = [1] + x_2 + x_3 + x_4 ---------------------------------------- (14) Obligation: Complexity Dependency Tuples Problem Rules: remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false and(z0, z1) -> #and(z0, z1) #equal(z0, z1) -> #eq(z0, z1) #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true Tuples: #EQ'(#neg(z0), #neg(z1)) -> c48(#EQ'(z0, z1)) #EQ'(#pos(z0), #pos(z1)) -> c52(#EQ'(z0, z1)) #EQ'(#s(z0), #s(z1)) -> c54(#EQ'(z0, z1)) #EQ''(#neg(z0), #neg(z1)) -> c69(#EQ''(z0, z1)) #EQ''(#pos(z0), #pos(z1)) -> c73(#EQ''(z0, z1)) #EQ''(#s(z0), #s(z1)) -> c75(#EQ''(z0, z1)) #EQUAL'(z0, z1) -> c80(#EQ''(z0, z1)) EQ'(z0, z1) -> c82(EQ#1'(z0, z1)) EQ#1'(::(z0, z1), z2) -> c83(EQ#3'(z2, z0, z1)) NUB'(z0) -> c89(NUB#1'(z0)) NUB#1'(::(z0, z1)) -> c90(NUB'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, z1) -> c92(REMOVE#1'(z1, z0)) REMOVE#1'(::(z0, z1), z2) -> c93(REMOVE#2'(eq(z2, z0), z2, z0, z1), EQ'(z2, z0)) REMOVE#2'(#false, z0, z1, z2) -> c95(REMOVE'(z0, z2)) REMOVE#2'(#true, z0, z1, z2) -> c96(REMOVE'(z0, z2)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c55(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c56(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z1, z3)) #EQ''(::(z0, z1), ::(z2, z3)) -> c76(#EQ''(z0, z2), #EQ''(z1, z3)) EQ#3'(::(z0, z1), z2, z3) -> c87(#EQUAL'(z2, z0), EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) S tuples: #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) K tuples: NUB''(z0) -> c107(NUB#1''(z0)) Defined Rule Symbols: remove_2, remove#1_2, remove#2_4, eq_2, eq#1_2, eq#3_3, and_2, #equal_2, #eq_2, #and_2, eq#2_1 Defined Pair Symbols: #EQ'_2, #EQ''_2, #EQUAL'_2, EQ'_2, EQ#1'_2, NUB'_1, NUB#1'_1, REMOVE'_2, REMOVE#1'_2, REMOVE#2'_4, #EQUAL''_2, EQ''_2, EQ#1''_2, NUB''_1, NUB#1''_1, REMOVE''_2, REMOVE#1''_2, REMOVE#2''_4, EQ#3'_3, EQ#3''_3 Compound Symbols: c48_1, c52_1, c54_1, c69_1, c73_1, c75_1, c80_1, c82_1, c83_1, c89_1, c90_2, c92_1, c93_2, c95_1, c96_1, c97_1, c99_1, c100_1, c107_1, c108_3, c110_1, c111_3, c113_1, c114_1, c55_3, c56_3, c76_2, c87_2, c105_3, c39_1 ---------------------------------------- (15) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) ---------------------------------------- (16) Obligation: Complexity Dependency Tuples Problem Rules: remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false and(z0, z1) -> #and(z0, z1) #equal(z0, z1) -> #eq(z0, z1) #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true Tuples: #EQ'(#neg(z0), #neg(z1)) -> c48(#EQ'(z0, z1)) #EQ'(#pos(z0), #pos(z1)) -> c52(#EQ'(z0, z1)) #EQ'(#s(z0), #s(z1)) -> c54(#EQ'(z0, z1)) #EQ''(#neg(z0), #neg(z1)) -> c69(#EQ''(z0, z1)) #EQ''(#pos(z0), #pos(z1)) -> c73(#EQ''(z0, z1)) #EQ''(#s(z0), #s(z1)) -> c75(#EQ''(z0, z1)) #EQUAL'(z0, z1) -> c80(#EQ''(z0, z1)) EQ'(z0, z1) -> c82(EQ#1'(z0, z1)) EQ#1'(::(z0, z1), z2) -> c83(EQ#3'(z2, z0, z1)) NUB'(z0) -> c89(NUB#1'(z0)) NUB#1'(::(z0, z1)) -> c90(NUB'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, z1) -> c92(REMOVE#1'(z1, z0)) REMOVE#1'(::(z0, z1), z2) -> c93(REMOVE#2'(eq(z2, z0), z2, z0, z1), EQ'(z2, z0)) REMOVE#2'(#false, z0, z1, z2) -> c95(REMOVE'(z0, z2)) REMOVE#2'(#true, z0, z1, z2) -> c96(REMOVE'(z0, z2)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c55(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c56(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z1, z3)) #EQ''(::(z0, z1), ::(z2, z3)) -> c76(#EQ''(z0, z2), #EQ''(z1, z3)) EQ#3'(::(z0, z1), z2, z3) -> c87(#EQUAL'(z2, z0), EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) S tuples: #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) K tuples: NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) Defined Rule Symbols: remove_2, remove#1_2, remove#2_4, eq_2, eq#1_2, eq#3_3, and_2, #equal_2, #eq_2, #and_2, eq#2_1 Defined Pair Symbols: #EQ'_2, #EQ''_2, #EQUAL'_2, EQ'_2, EQ#1'_2, NUB'_1, NUB#1'_1, REMOVE'_2, REMOVE#1'_2, REMOVE#2'_4, #EQUAL''_2, EQ''_2, EQ#1''_2, NUB''_1, NUB#1''_1, REMOVE''_2, REMOVE#1''_2, REMOVE#2''_4, EQ#3'_3, EQ#3''_3 Compound Symbols: c48_1, c52_1, c54_1, c69_1, c73_1, c75_1, c80_1, c82_1, c83_1, c89_1, c90_2, c92_1, c93_2, c95_1, c96_1, c97_1, c99_1, c100_1, c107_1, c108_3, c110_1, c111_3, c113_1, c114_1, c55_3, c56_3, c76_2, c87_2, c105_3, c39_1 ---------------------------------------- (17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) We considered the (Usable) Rules: #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(#0, #neg(z0)) -> #false #eq(#neg(z0), #0) -> #false remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) #eq(#0, #pos(z0)) -> #false #eq(#pos(z0), #0) -> #false remove#2(#true, z0, z1, z2) -> remove(z0, z2) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #neg(z1)) -> #false #and(#true, #true) -> #true remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) #eq(#0, #s(z0)) -> #false #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) eq(z0, z1) -> eq#1(z0, z1) remove(z0, z1) -> remove#1(z1, z0) #eq(nil, nil) -> #true eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) and(z0, z1) -> #and(z0, z1) #eq(#0, #0) -> #true #and(#false, #true) -> #false #and(#true, #false) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) remove#1(nil, z0) -> nil eq#1(nil, z0) -> eq#2(z0) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false eq#3(nil, z0, z1) -> #false #equal(z0, z1) -> #eq(z0, z1) eq#2(nil) -> #true eq#2(::(z0, z1)) -> #false #and(#false, #false) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) And the Tuples: #EQ'(#neg(z0), #neg(z1)) -> c48(#EQ'(z0, z1)) #EQ'(#pos(z0), #pos(z1)) -> c52(#EQ'(z0, z1)) #EQ'(#s(z0), #s(z1)) -> c54(#EQ'(z0, z1)) #EQ''(#neg(z0), #neg(z1)) -> c69(#EQ''(z0, z1)) #EQ''(#pos(z0), #pos(z1)) -> c73(#EQ''(z0, z1)) #EQ''(#s(z0), #s(z1)) -> c75(#EQ''(z0, z1)) #EQUAL'(z0, z1) -> c80(#EQ''(z0, z1)) EQ'(z0, z1) -> c82(EQ#1'(z0, z1)) EQ#1'(::(z0, z1), z2) -> c83(EQ#3'(z2, z0, z1)) NUB'(z0) -> c89(NUB#1'(z0)) NUB#1'(::(z0, z1)) -> c90(NUB'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, z1) -> c92(REMOVE#1'(z1, z0)) REMOVE#1'(::(z0, z1), z2) -> c93(REMOVE#2'(eq(z2, z0), z2, z0, z1), EQ'(z2, z0)) REMOVE#2'(#false, z0, z1, z2) -> c95(REMOVE'(z0, z2)) REMOVE#2'(#true, z0, z1, z2) -> c96(REMOVE'(z0, z2)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c55(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c56(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z1, z3)) #EQ''(::(z0, z1), ::(z2, z3)) -> c76(#EQ''(z0, z2), #EQ''(z1, z3)) EQ#3'(::(z0, z1), z2, z3) -> c87(#EQUAL'(z2, z0), EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) 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(#EQUAL'(x_1, x_2)) = 0 POL(#EQUAL''(x_1, x_2)) = 0 POL(#and(x_1, x_2)) = x_1 POL(#eq(x_1, x_2)) = x_1*x_2 POL(#equal(x_1, x_2)) = x_1*x_2 POL(#false) = 0 POL(#neg(x_1)) = x_1 POL(#pos(x_1)) = x_1 POL(#s(x_1)) = x_1 POL(#true) = [2] POL(::(x_1, x_2)) = x_1 + x_2 POL(EQ#1'(x_1, x_2)) = 0 POL(EQ#1''(x_1, x_2)) = 0 POL(EQ#3'(x_1, x_2, x_3)) = 0 POL(EQ#3''(x_1, x_2, x_3)) = 0 POL(EQ'(x_1, x_2)) = 0 POL(EQ''(x_1, x_2)) = 0 POL(NUB#1'(x_1)) = 0 POL(NUB#1''(x_1)) = x_1^2 POL(NUB'(x_1)) = 0 POL(NUB''(x_1)) = x_1^2 POL(REMOVE#1'(x_1, x_2)) = 0 POL(REMOVE#1''(x_1, x_2)) = x_1*x_2 POL(REMOVE#2'(x_1, x_2, x_3, x_4)) = 0 POL(REMOVE#2''(x_1, x_2, x_3, x_4)) = x_1 + x_2*x_4 POL(REMOVE'(x_1, x_2)) = 0 POL(REMOVE''(x_1, x_2)) = x_1*x_2 POL(and(x_1, x_2)) = x_1 POL(c100(x_1)) = x_1 POL(c105(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c107(x_1)) = x_1 POL(c108(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c110(x_1)) = x_1 POL(c111(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c113(x_1)) = x_1 POL(c114(x_1)) = x_1 POL(c39(x_1)) = x_1 POL(c48(x_1)) = x_1 POL(c52(x_1)) = x_1 POL(c54(x_1)) = x_1 POL(c55(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c56(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c69(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1, x_2)) = x_1 + x_2 POL(c80(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(c83(x_1)) = x_1 POL(c87(x_1, x_2)) = x_1 + x_2 POL(c89(x_1)) = x_1 POL(c90(x_1, x_2)) = x_1 + x_2 POL(c92(x_1)) = x_1 POL(c93(x_1, x_2)) = x_1 + x_2 POL(c95(x_1)) = x_1 POL(c96(x_1)) = x_1 POL(c97(x_1)) = x_1 POL(c99(x_1)) = x_1 POL(eq(x_1, x_2)) = x_1*x_2 POL(eq#1(x_1, x_2)) = x_1*x_2 POL(eq#2(x_1)) = [2]x_1 POL(eq#3(x_1, x_2, x_3)) = x_1*x_2 POL(nil) = [2] POL(remove(x_1, x_2)) = x_2 POL(remove#1(x_1, x_2)) = x_1 POL(remove#2(x_1, x_2, x_3, x_4)) = x_3 + x_4 ---------------------------------------- (18) Obligation: Complexity Dependency Tuples Problem Rules: remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false and(z0, z1) -> #and(z0, z1) #equal(z0, z1) -> #eq(z0, z1) #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true Tuples: #EQ'(#neg(z0), #neg(z1)) -> c48(#EQ'(z0, z1)) #EQ'(#pos(z0), #pos(z1)) -> c52(#EQ'(z0, z1)) #EQ'(#s(z0), #s(z1)) -> c54(#EQ'(z0, z1)) #EQ''(#neg(z0), #neg(z1)) -> c69(#EQ''(z0, z1)) #EQ''(#pos(z0), #pos(z1)) -> c73(#EQ''(z0, z1)) #EQ''(#s(z0), #s(z1)) -> c75(#EQ''(z0, z1)) #EQUAL'(z0, z1) -> c80(#EQ''(z0, z1)) EQ'(z0, z1) -> c82(EQ#1'(z0, z1)) EQ#1'(::(z0, z1), z2) -> c83(EQ#3'(z2, z0, z1)) NUB'(z0) -> c89(NUB#1'(z0)) NUB#1'(::(z0, z1)) -> c90(NUB'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, z1) -> c92(REMOVE#1'(z1, z0)) REMOVE#1'(::(z0, z1), z2) -> c93(REMOVE#2'(eq(z2, z0), z2, z0, z1), EQ'(z2, z0)) REMOVE#2'(#false, z0, z1, z2) -> c95(REMOVE'(z0, z2)) REMOVE#2'(#true, z0, z1, z2) -> c96(REMOVE'(z0, z2)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c55(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c56(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z1, z3)) #EQ''(::(z0, z1), ::(z2, z3)) -> c76(#EQ''(z0, z2), #EQ''(z1, z3)) EQ#3'(::(z0, z1), z2, z3) -> c87(#EQUAL'(z2, z0), EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) S tuples: #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) K tuples: NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) Defined Rule Symbols: remove_2, remove#1_2, remove#2_4, eq_2, eq#1_2, eq#3_3, and_2, #equal_2, #eq_2, #and_2, eq#2_1 Defined Pair Symbols: #EQ'_2, #EQ''_2, #EQUAL'_2, EQ'_2, EQ#1'_2, NUB'_1, NUB#1'_1, REMOVE'_2, REMOVE#1'_2, REMOVE#2'_4, #EQUAL''_2, EQ''_2, EQ#1''_2, NUB''_1, NUB#1''_1, REMOVE''_2, REMOVE#1''_2, REMOVE#2''_4, EQ#3'_3, EQ#3''_3 Compound Symbols: c48_1, c52_1, c54_1, c69_1, c73_1, c75_1, c80_1, c82_1, c83_1, c89_1, c90_2, c92_1, c93_2, c95_1, c96_1, c97_1, c99_1, c100_1, c107_1, c108_3, c110_1, c111_3, c113_1, c114_1, c55_3, c56_3, c76_2, c87_2, c105_3, c39_1 ---------------------------------------- (19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) We considered the (Usable) Rules: remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove(z0, z1) -> remove#1(z1, z0) remove#1(nil, z0) -> nil And the Tuples: #EQ'(#neg(z0), #neg(z1)) -> c48(#EQ'(z0, z1)) #EQ'(#pos(z0), #pos(z1)) -> c52(#EQ'(z0, z1)) #EQ'(#s(z0), #s(z1)) -> c54(#EQ'(z0, z1)) #EQ''(#neg(z0), #neg(z1)) -> c69(#EQ''(z0, z1)) #EQ''(#pos(z0), #pos(z1)) -> c73(#EQ''(z0, z1)) #EQ''(#s(z0), #s(z1)) -> c75(#EQ''(z0, z1)) #EQUAL'(z0, z1) -> c80(#EQ''(z0, z1)) EQ'(z0, z1) -> c82(EQ#1'(z0, z1)) EQ#1'(::(z0, z1), z2) -> c83(EQ#3'(z2, z0, z1)) NUB'(z0) -> c89(NUB#1'(z0)) NUB#1'(::(z0, z1)) -> c90(NUB'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, z1) -> c92(REMOVE#1'(z1, z0)) REMOVE#1'(::(z0, z1), z2) -> c93(REMOVE#2'(eq(z2, z0), z2, z0, z1), EQ'(z2, z0)) REMOVE#2'(#false, z0, z1, z2) -> c95(REMOVE'(z0, z2)) REMOVE#2'(#true, z0, z1, z2) -> c96(REMOVE'(z0, z2)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c55(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c56(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z1, z3)) #EQ''(::(z0, z1), ::(z2, z3)) -> c76(#EQ''(z0, z2), #EQ''(z1, z3)) EQ#3'(::(z0, z1), z2, z3) -> c87(#EQUAL'(z2, z0), EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) 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(#EQUAL'(x_1, x_2)) = 0 POL(#EQUAL''(x_1, x_2)) = 0 POL(#and(x_1, x_2)) = [1] POL(#eq(x_1, x_2)) = [2] POL(#equal(x_1, x_2)) = 0 POL(#false) = 0 POL(#neg(x_1)) = 0 POL(#pos(x_1)) = 0 POL(#s(x_1)) = 0 POL(#true) = 0 POL(::(x_1, x_2)) = [1] + x_1 + x_2 POL(EQ#1'(x_1, x_2)) = 0 POL(EQ#1''(x_1, x_2)) = 0 POL(EQ#3'(x_1, x_2, x_3)) = 0 POL(EQ#3''(x_1, x_2, x_3)) = 0 POL(EQ'(x_1, x_2)) = 0 POL(EQ''(x_1, x_2)) = 0 POL(NUB#1'(x_1)) = 0 POL(NUB#1''(x_1)) = x_1^2 POL(NUB'(x_1)) = 0 POL(NUB''(x_1)) = x_1^2 POL(REMOVE#1'(x_1, x_2)) = 0 POL(REMOVE#1''(x_1, x_2)) = [2]x_1 POL(REMOVE#2'(x_1, x_2, x_3, x_4)) = 0 POL(REMOVE#2''(x_1, x_2, x_3, x_4)) = [1] + [2]x_4 POL(REMOVE'(x_1, x_2)) = 0 POL(REMOVE''(x_1, x_2)) = [2]x_2 POL(and(x_1, x_2)) = [1] POL(c100(x_1)) = x_1 POL(c105(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c107(x_1)) = x_1 POL(c108(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c110(x_1)) = x_1 POL(c111(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c113(x_1)) = x_1 POL(c114(x_1)) = x_1 POL(c39(x_1)) = x_1 POL(c48(x_1)) = x_1 POL(c52(x_1)) = x_1 POL(c54(x_1)) = x_1 POL(c55(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c56(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c69(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1, x_2)) = x_1 + x_2 POL(c80(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(c83(x_1)) = x_1 POL(c87(x_1, x_2)) = x_1 + x_2 POL(c89(x_1)) = x_1 POL(c90(x_1, x_2)) = x_1 + x_2 POL(c92(x_1)) = x_1 POL(c93(x_1, x_2)) = x_1 + x_2 POL(c95(x_1)) = x_1 POL(c96(x_1)) = x_1 POL(c97(x_1)) = x_1 POL(c99(x_1)) = x_1 POL(eq(x_1, x_2)) = 0 POL(eq#1(x_1, x_2)) = [1] + x_2 + x_2^2 POL(eq#2(x_1)) = [1] POL(eq#3(x_1, x_2, x_3)) = [1] + x_2 + x_3 + x_3^2 + x_2*x_3 + x_2^2 POL(nil) = 0 POL(remove(x_1, x_2)) = x_2 POL(remove#1(x_1, x_2)) = x_1 POL(remove#2(x_1, x_2, x_3, x_4)) = [1] + x_3 + x_4 ---------------------------------------- (20) Obligation: Complexity Dependency Tuples Problem Rules: remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false and(z0, z1) -> #and(z0, z1) #equal(z0, z1) -> #eq(z0, z1) #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true Tuples: #EQ'(#neg(z0), #neg(z1)) -> c48(#EQ'(z0, z1)) #EQ'(#pos(z0), #pos(z1)) -> c52(#EQ'(z0, z1)) #EQ'(#s(z0), #s(z1)) -> c54(#EQ'(z0, z1)) #EQ''(#neg(z0), #neg(z1)) -> c69(#EQ''(z0, z1)) #EQ''(#pos(z0), #pos(z1)) -> c73(#EQ''(z0, z1)) #EQ''(#s(z0), #s(z1)) -> c75(#EQ''(z0, z1)) #EQUAL'(z0, z1) -> c80(#EQ''(z0, z1)) EQ'(z0, z1) -> c82(EQ#1'(z0, z1)) EQ#1'(::(z0, z1), z2) -> c83(EQ#3'(z2, z0, z1)) NUB'(z0) -> c89(NUB#1'(z0)) NUB#1'(::(z0, z1)) -> c90(NUB'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, z1) -> c92(REMOVE#1'(z1, z0)) REMOVE#1'(::(z0, z1), z2) -> c93(REMOVE#2'(eq(z2, z0), z2, z0, z1), EQ'(z2, z0)) REMOVE#2'(#false, z0, z1, z2) -> c95(REMOVE'(z0, z2)) REMOVE#2'(#true, z0, z1, z2) -> c96(REMOVE'(z0, z2)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c55(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c56(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z1, z3)) #EQ''(::(z0, z1), ::(z2, z3)) -> c76(#EQ''(z0, z2), #EQ''(z1, z3)) EQ#3'(::(z0, z1), z2, z3) -> c87(#EQUAL'(z2, z0), EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) S tuples: #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) K tuples: NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) Defined Rule Symbols: remove_2, remove#1_2, remove#2_4, eq_2, eq#1_2, eq#3_3, and_2, #equal_2, #eq_2, #and_2, eq#2_1 Defined Pair Symbols: #EQ'_2, #EQ''_2, #EQUAL'_2, EQ'_2, EQ#1'_2, NUB'_1, NUB#1'_1, REMOVE'_2, REMOVE#1'_2, REMOVE#2'_4, #EQUAL''_2, EQ''_2, EQ#1''_2, NUB''_1, NUB#1''_1, REMOVE''_2, REMOVE#1''_2, REMOVE#2''_4, EQ#3'_3, EQ#3''_3 Compound Symbols: c48_1, c52_1, c54_1, c69_1, c73_1, c75_1, c80_1, c82_1, c83_1, c89_1, c90_2, c92_1, c93_2, c95_1, c96_1, c97_1, c99_1, c100_1, c107_1, c108_3, c110_1, c111_3, c113_1, c114_1, c55_3, c56_3, c76_2, c87_2, c105_3, c39_1 ---------------------------------------- (21) CdtKnowledgeProof (BOTH BOUNDS(ID, ID)) The following tuples could be moved from S to K by knowledge propagation: REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) ---------------------------------------- (22) Obligation: Complexity Dependency Tuples Problem Rules: remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false and(z0, z1) -> #and(z0, z1) #equal(z0, z1) -> #eq(z0, z1) #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true Tuples: #EQ'(#neg(z0), #neg(z1)) -> c48(#EQ'(z0, z1)) #EQ'(#pos(z0), #pos(z1)) -> c52(#EQ'(z0, z1)) #EQ'(#s(z0), #s(z1)) -> c54(#EQ'(z0, z1)) #EQ''(#neg(z0), #neg(z1)) -> c69(#EQ''(z0, z1)) #EQ''(#pos(z0), #pos(z1)) -> c73(#EQ''(z0, z1)) #EQ''(#s(z0), #s(z1)) -> c75(#EQ''(z0, z1)) #EQUAL'(z0, z1) -> c80(#EQ''(z0, z1)) EQ'(z0, z1) -> c82(EQ#1'(z0, z1)) EQ#1'(::(z0, z1), z2) -> c83(EQ#3'(z2, z0, z1)) NUB'(z0) -> c89(NUB#1'(z0)) NUB#1'(::(z0, z1)) -> c90(NUB'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, z1) -> c92(REMOVE#1'(z1, z0)) REMOVE#1'(::(z0, z1), z2) -> c93(REMOVE#2'(eq(z2, z0), z2, z0, z1), EQ'(z2, z0)) REMOVE#2'(#false, z0, z1, z2) -> c95(REMOVE'(z0, z2)) REMOVE#2'(#true, z0, z1, z2) -> c96(REMOVE'(z0, z2)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c55(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c56(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z1, z3)) #EQ''(::(z0, z1), ::(z2, z3)) -> c76(#EQ''(z0, z2), #EQ''(z1, z3)) EQ#3'(::(z0, z1), z2, z3) -> c87(#EQUAL'(z2, z0), EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) S tuples: #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) K tuples: NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) Defined Rule Symbols: remove_2, remove#1_2, remove#2_4, eq_2, eq#1_2, eq#3_3, and_2, #equal_2, #eq_2, #and_2, eq#2_1 Defined Pair Symbols: #EQ'_2, #EQ''_2, #EQUAL'_2, EQ'_2, EQ#1'_2, NUB'_1, NUB#1'_1, REMOVE'_2, REMOVE#1'_2, REMOVE#2'_4, #EQUAL''_2, EQ''_2, EQ#1''_2, NUB''_1, NUB#1''_1, REMOVE''_2, REMOVE#1''_2, REMOVE#2''_4, EQ#3'_3, EQ#3''_3 Compound Symbols: c48_1, c52_1, c54_1, c69_1, c73_1, c75_1, c80_1, c82_1, c83_1, c89_1, c90_2, c92_1, c93_2, c95_1, c96_1, c97_1, c99_1, c100_1, c107_1, c108_3, c110_1, c111_3, c113_1, c114_1, c55_3, c56_3, c76_2, c87_2, c105_3, c39_1 ---------------------------------------- (23) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2))) Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S. #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) We considered the (Usable) Rules: remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove(z0, z1) -> remove#1(z1, z0) remove#1(nil, z0) -> nil And the Tuples: #EQ'(#neg(z0), #neg(z1)) -> c48(#EQ'(z0, z1)) #EQ'(#pos(z0), #pos(z1)) -> c52(#EQ'(z0, z1)) #EQ'(#s(z0), #s(z1)) -> c54(#EQ'(z0, z1)) #EQ''(#neg(z0), #neg(z1)) -> c69(#EQ''(z0, z1)) #EQ''(#pos(z0), #pos(z1)) -> c73(#EQ''(z0, z1)) #EQ''(#s(z0), #s(z1)) -> c75(#EQ''(z0, z1)) #EQUAL'(z0, z1) -> c80(#EQ''(z0, z1)) EQ'(z0, z1) -> c82(EQ#1'(z0, z1)) EQ#1'(::(z0, z1), z2) -> c83(EQ#3'(z2, z0, z1)) NUB'(z0) -> c89(NUB#1'(z0)) NUB#1'(::(z0, z1)) -> c90(NUB'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, z1) -> c92(REMOVE#1'(z1, z0)) REMOVE#1'(::(z0, z1), z2) -> c93(REMOVE#2'(eq(z2, z0), z2, z0, z1), EQ'(z2, z0)) REMOVE#2'(#false, z0, z1, z2) -> c95(REMOVE'(z0, z2)) REMOVE#2'(#true, z0, z1, z2) -> c96(REMOVE'(z0, z2)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c55(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c56(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z1, z3)) #EQ''(::(z0, z1), ::(z2, z3)) -> c76(#EQ''(z0, z2), #EQ''(z1, z3)) EQ#3'(::(z0, z1), z2, z3) -> c87(#EQUAL'(z2, z0), EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) 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(#EQUAL'(x_1, x_2)) = 0 POL(#EQUAL''(x_1, x_2)) = [1] + x_2 POL(#and(x_1, x_2)) = [2] POL(#eq(x_1, x_2)) = [2] POL(#equal(x_1, x_2)) = 0 POL(#false) = 0 POL(#neg(x_1)) = 0 POL(#pos(x_1)) = 0 POL(#s(x_1)) = 0 POL(#true) = 0 POL(::(x_1, x_2)) = [1] + x_1 + x_2 POL(EQ#1'(x_1, x_2)) = 0 POL(EQ#1''(x_1, x_2)) = x_2 POL(EQ#3'(x_1, x_2, x_3)) = 0 POL(EQ#3''(x_1, x_2, x_3)) = x_1 POL(EQ'(x_1, x_2)) = 0 POL(EQ''(x_1, x_2)) = x_2 POL(NUB#1'(x_1)) = 0 POL(NUB#1''(x_1)) = [2]x_1^2 POL(NUB'(x_1)) = 0 POL(NUB''(x_1)) = [2]x_1^2 POL(REMOVE#1'(x_1, x_2)) = 0 POL(REMOVE#1''(x_1, x_2)) = x_1 POL(REMOVE#2'(x_1, x_2, x_3, x_4)) = 0 POL(REMOVE#2''(x_1, x_2, x_3, x_4)) = x_4 POL(REMOVE'(x_1, x_2)) = 0 POL(REMOVE''(x_1, x_2)) = x_2 POL(and(x_1, x_2)) = [1] POL(c100(x_1)) = x_1 POL(c105(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c107(x_1)) = x_1 POL(c108(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c110(x_1)) = x_1 POL(c111(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c113(x_1)) = x_1 POL(c114(x_1)) = x_1 POL(c39(x_1)) = x_1 POL(c48(x_1)) = x_1 POL(c52(x_1)) = x_1 POL(c54(x_1)) = x_1 POL(c55(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c56(x_1, x_2, x_3)) = x_1 + x_2 + x_3 POL(c69(x_1)) = x_1 POL(c73(x_1)) = x_1 POL(c75(x_1)) = x_1 POL(c76(x_1, x_2)) = x_1 + x_2 POL(c80(x_1)) = x_1 POL(c82(x_1)) = x_1 POL(c83(x_1)) = x_1 POL(c87(x_1, x_2)) = x_1 + x_2 POL(c89(x_1)) = x_1 POL(c90(x_1, x_2)) = x_1 + x_2 POL(c92(x_1)) = x_1 POL(c93(x_1, x_2)) = x_1 + x_2 POL(c95(x_1)) = x_1 POL(c96(x_1)) = x_1 POL(c97(x_1)) = x_1 POL(c99(x_1)) = x_1 POL(eq(x_1, x_2)) = 0 POL(eq#1(x_1, x_2)) = [1] + x_2 + x_2^2 POL(eq#2(x_1)) = [1] POL(eq#3(x_1, x_2, x_3)) = [1] + x_2 + x_3 + x_3^2 + x_2*x_3 + x_2^2 POL(nil) = 0 POL(remove(x_1, x_2)) = x_1 + x_2 POL(remove#1(x_1, x_2)) = x_1 + x_2 POL(remove#2(x_1, x_2, x_3, x_4)) = [1] + x_2 + x_3 + x_4 ---------------------------------------- (24) Obligation: Complexity Dependency Tuples Problem Rules: remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false and(z0, z1) -> #and(z0, z1) #equal(z0, z1) -> #eq(z0, z1) #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true Tuples: #EQ'(#neg(z0), #neg(z1)) -> c48(#EQ'(z0, z1)) #EQ'(#pos(z0), #pos(z1)) -> c52(#EQ'(z0, z1)) #EQ'(#s(z0), #s(z1)) -> c54(#EQ'(z0, z1)) #EQ''(#neg(z0), #neg(z1)) -> c69(#EQ''(z0, z1)) #EQ''(#pos(z0), #pos(z1)) -> c73(#EQ''(z0, z1)) #EQ''(#s(z0), #s(z1)) -> c75(#EQ''(z0, z1)) #EQUAL'(z0, z1) -> c80(#EQ''(z0, z1)) EQ'(z0, z1) -> c82(EQ#1'(z0, z1)) EQ#1'(::(z0, z1), z2) -> c83(EQ#3'(z2, z0, z1)) NUB'(z0) -> c89(NUB#1'(z0)) NUB#1'(::(z0, z1)) -> c90(NUB'(remove(z0, z1)), REMOVE'(z0, z1)) REMOVE'(z0, z1) -> c92(REMOVE#1'(z1, z0)) REMOVE#1'(::(z0, z1), z2) -> c93(REMOVE#2'(eq(z2, z0), z2, z0, z1), EQ'(z2, z0)) REMOVE#2'(#false, z0, z1, z2) -> c95(REMOVE'(z0, z2)) REMOVE#2'(#true, z0, z1, z2) -> c96(REMOVE'(z0, z2)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c55(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c56(#EQ''(z0, z2), #EQ''(z1, z3), #EQ'(z1, z3)) #EQ''(::(z0, z1), ::(z2, z3)) -> c76(#EQ''(z0, z2), #EQ''(z1, z3)) EQ#3'(::(z0, z1), z2, z3) -> c87(#EQUAL'(z2, z0), EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) S tuples: EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) K tuples: NUB''(z0) -> c107(NUB#1''(z0)) NUB#1''(::(z0, z1)) -> c108(NUB''(remove(z0, z1)), REMOVE'(z0, z1), REMOVE''(z0, z1)) REMOVE#2''(#true, z0, z1, z2) -> c114(REMOVE''(z0, z2)) REMOVE#1''(::(z0, z1), z2) -> c111(REMOVE#2''(eq(z2, z0), z2, z0, z1), EQ'(z2, z0), EQ''(z2, z0)) REMOVE#2''(#false, z0, z1, z2) -> c113(REMOVE''(z0, z2)) REMOVE''(z0, z1) -> c110(REMOVE#1''(z1, z0)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) Defined Rule Symbols: remove_2, remove#1_2, remove#2_4, eq_2, eq#1_2, eq#3_3, and_2, #equal_2, #eq_2, #and_2, eq#2_1 Defined Pair Symbols: #EQ'_2, #EQ''_2, #EQUAL'_2, EQ'_2, EQ#1'_2, NUB'_1, NUB#1'_1, REMOVE'_2, REMOVE#1'_2, REMOVE#2'_4, #EQUAL''_2, EQ''_2, EQ#1''_2, NUB''_1, NUB#1''_1, REMOVE''_2, REMOVE#1''_2, REMOVE#2''_4, EQ#3'_3, EQ#3''_3 Compound Symbols: c48_1, c52_1, c54_1, c69_1, c73_1, c75_1, c80_1, c82_1, c83_1, c89_1, c90_2, c92_1, c93_2, c95_1, c96_1, c97_1, c99_1, c100_1, c107_1, c108_3, c110_1, c111_3, c113_1, c114_1, c55_3, c56_3, c76_2, c87_2, c105_3, c39_1 ---------------------------------------- (25) CdtKnowledgeProof (FINISHED) The following tuples could be moved from S to K by knowledge propagation: EQ''(z0, z1) -> c99(EQ#1''(z0, z1)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) EQ#1''(::(z0, z1), z2) -> c100(EQ#3''(z2, z0, z1)) EQ#3''(::(z0, z1), z2, z3) -> c105(#EQUAL'(z2, z0), EQ'(z3, z1), EQ''(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL'(z2, z0)) EQ#3''(::(z0, z1), z2, z3) -> c39(EQ'(z3, z1)) EQ#3''(::(z0, z1), z2, z3) -> c39(#EQUAL''(z2, z0)) #EQUAL''(z0, z1) -> c97(#EQ'(z0, z1)) Now S is empty ---------------------------------------- (26) BOUNDS(1, 1) ---------------------------------------- (27) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (28) 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: #EQUAL(z0, z1) -> c21(#EQ(z0, z1)) AND(z0, z1) -> c22(#AND(z0, z1)) EQ(z0, z1) -> c23(EQ#1(z0, z1)) EQ#1(::(z0, z1), z2) -> c24(EQ#3(z2, z0, z1)) EQ#1(nil, z0) -> c25(EQ#2(z0)) EQ#2(::(z0, z1)) -> c26 EQ#2(nil) -> c27 EQ#3(::(z0, z1), z2, z3) -> c28(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0)) EQ#3(::(z0, z1), z2, z3) -> c29(AND(#equal(z2, z0), eq(z3, z1)), EQ(z3, z1)) EQ#3(nil, z0, z1) -> c30 NUB(z0) -> c31(NUB#1(z0)) NUB#1(::(z0, z1)) -> c32(NUB(remove(z0, z1)), REMOVE(z0, z1)) NUB#1(nil) -> c33 REMOVE(z0, z1) -> c34(REMOVE#1(z1, z0)) REMOVE#1(::(z0, z1), z2) -> c35(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) REMOVE#1(nil, z0) -> c36 REMOVE#2(#false, z0, z1, z2) -> c37(REMOVE(z0, z2)) REMOVE#2(#true, z0, z1, z2) -> c38(REMOVE(z0, z2)) The (relative) TRS S consists of the following rules: #AND(#false, #false) -> c #AND(#false, #true) -> c1 #AND(#true, #false) -> c2 #AND(#true, #true) -> c3 #EQ(#0, #0) -> c4 #EQ(#0, #neg(z0)) -> c5 #EQ(#0, #pos(z0)) -> c6 #EQ(#0, #s(z0)) -> c7 #EQ(#neg(z0), #0) -> c8 #EQ(#neg(z0), #neg(z1)) -> c9(#EQ(z0, z1)) #EQ(#neg(z0), #pos(z1)) -> c10 #EQ(#pos(z0), #0) -> c11 #EQ(#pos(z0), #neg(z1)) -> c12 #EQ(#pos(z0), #pos(z1)) -> c13(#EQ(z0, z1)) #EQ(#s(z0), #0) -> c14 #EQ(#s(z0), #s(z1)) -> c15(#EQ(z0, z1)) #EQ(::(z0, z1), ::(z2, z3)) -> c16(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z0, z2)) #EQ(::(z0, z1), ::(z2, z3)) -> c17(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z1, z3)) #EQ(::(z0, z1), nil) -> c18 #EQ(nil, ::(z0, z1)) -> c19 #EQ(nil, nil) -> c20 #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #equal(z0, z1) -> #eq(z0, z1) and(z0, z1) -> #and(z0, z1) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false nub(z0) -> nub#1(z0) nub#1(::(z0, z1)) -> ::(z0, nub(remove(z0, z1))) nub#1(nil) -> nil remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) Rewrite Strategy: INNERMOST ---------------------------------------- (29) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence EQ#1(::(z0, z1), ::(z01_3, z12_3)) ->^+ c24(c29(AND(#equal(z0, z01_3), eq(z1, z12_3)), c23(EQ#1(z1, z12_3)))) gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1,0]. The pumping substitution is [z1 / ::(z0, z1), z12_3 / ::(z01_3, z12_3)]. The result substitution is [ ]. ---------------------------------------- (30) Complex Obligation (BEST) ---------------------------------------- (31) 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: #EQUAL(z0, z1) -> c21(#EQ(z0, z1)) AND(z0, z1) -> c22(#AND(z0, z1)) EQ(z0, z1) -> c23(EQ#1(z0, z1)) EQ#1(::(z0, z1), z2) -> c24(EQ#3(z2, z0, z1)) EQ#1(nil, z0) -> c25(EQ#2(z0)) EQ#2(::(z0, z1)) -> c26 EQ#2(nil) -> c27 EQ#3(::(z0, z1), z2, z3) -> c28(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0)) EQ#3(::(z0, z1), z2, z3) -> c29(AND(#equal(z2, z0), eq(z3, z1)), EQ(z3, z1)) EQ#3(nil, z0, z1) -> c30 NUB(z0) -> c31(NUB#1(z0)) NUB#1(::(z0, z1)) -> c32(NUB(remove(z0, z1)), REMOVE(z0, z1)) NUB#1(nil) -> c33 REMOVE(z0, z1) -> c34(REMOVE#1(z1, z0)) REMOVE#1(::(z0, z1), z2) -> c35(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) REMOVE#1(nil, z0) -> c36 REMOVE#2(#false, z0, z1, z2) -> c37(REMOVE(z0, z2)) REMOVE#2(#true, z0, z1, z2) -> c38(REMOVE(z0, z2)) The (relative) TRS S consists of the following rules: #AND(#false, #false) -> c #AND(#false, #true) -> c1 #AND(#true, #false) -> c2 #AND(#true, #true) -> c3 #EQ(#0, #0) -> c4 #EQ(#0, #neg(z0)) -> c5 #EQ(#0, #pos(z0)) -> c6 #EQ(#0, #s(z0)) -> c7 #EQ(#neg(z0), #0) -> c8 #EQ(#neg(z0), #neg(z1)) -> c9(#EQ(z0, z1)) #EQ(#neg(z0), #pos(z1)) -> c10 #EQ(#pos(z0), #0) -> c11 #EQ(#pos(z0), #neg(z1)) -> c12 #EQ(#pos(z0), #pos(z1)) -> c13(#EQ(z0, z1)) #EQ(#s(z0), #0) -> c14 #EQ(#s(z0), #s(z1)) -> c15(#EQ(z0, z1)) #EQ(::(z0, z1), ::(z2, z3)) -> c16(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z0, z2)) #EQ(::(z0, z1), ::(z2, z3)) -> c17(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z1, z3)) #EQ(::(z0, z1), nil) -> c18 #EQ(nil, ::(z0, z1)) -> c19 #EQ(nil, nil) -> c20 #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #equal(z0, z1) -> #eq(z0, z1) and(z0, z1) -> #and(z0, z1) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false nub(z0) -> nub#1(z0) nub#1(::(z0, z1)) -> ::(z0, nub(remove(z0, z1))) nub#1(nil) -> nil remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) Rewrite Strategy: INNERMOST ---------------------------------------- (32) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (33) BOUNDS(n^1, INF) ---------------------------------------- (34) 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: #EQUAL(z0, z1) -> c21(#EQ(z0, z1)) AND(z0, z1) -> c22(#AND(z0, z1)) EQ(z0, z1) -> c23(EQ#1(z0, z1)) EQ#1(::(z0, z1), z2) -> c24(EQ#3(z2, z0, z1)) EQ#1(nil, z0) -> c25(EQ#2(z0)) EQ#2(::(z0, z1)) -> c26 EQ#2(nil) -> c27 EQ#3(::(z0, z1), z2, z3) -> c28(AND(#equal(z2, z0), eq(z3, z1)), #EQUAL(z2, z0)) EQ#3(::(z0, z1), z2, z3) -> c29(AND(#equal(z2, z0), eq(z3, z1)), EQ(z3, z1)) EQ#3(nil, z0, z1) -> c30 NUB(z0) -> c31(NUB#1(z0)) NUB#1(::(z0, z1)) -> c32(NUB(remove(z0, z1)), REMOVE(z0, z1)) NUB#1(nil) -> c33 REMOVE(z0, z1) -> c34(REMOVE#1(z1, z0)) REMOVE#1(::(z0, z1), z2) -> c35(REMOVE#2(eq(z2, z0), z2, z0, z1), EQ(z2, z0)) REMOVE#1(nil, z0) -> c36 REMOVE#2(#false, z0, z1, z2) -> c37(REMOVE(z0, z2)) REMOVE#2(#true, z0, z1, z2) -> c38(REMOVE(z0, z2)) The (relative) TRS S consists of the following rules: #AND(#false, #false) -> c #AND(#false, #true) -> c1 #AND(#true, #false) -> c2 #AND(#true, #true) -> c3 #EQ(#0, #0) -> c4 #EQ(#0, #neg(z0)) -> c5 #EQ(#0, #pos(z0)) -> c6 #EQ(#0, #s(z0)) -> c7 #EQ(#neg(z0), #0) -> c8 #EQ(#neg(z0), #neg(z1)) -> c9(#EQ(z0, z1)) #EQ(#neg(z0), #pos(z1)) -> c10 #EQ(#pos(z0), #0) -> c11 #EQ(#pos(z0), #neg(z1)) -> c12 #EQ(#pos(z0), #pos(z1)) -> c13(#EQ(z0, z1)) #EQ(#s(z0), #0) -> c14 #EQ(#s(z0), #s(z1)) -> c15(#EQ(z0, z1)) #EQ(::(z0, z1), ::(z2, z3)) -> c16(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z0, z2)) #EQ(::(z0, z1), ::(z2, z3)) -> c17(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ(z1, z3)) #EQ(::(z0, z1), nil) -> c18 #EQ(nil, ::(z0, z1)) -> c19 #EQ(nil, nil) -> c20 #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #eq(#0, #0) -> #true #eq(#0, #neg(z0)) -> #false #eq(#0, #pos(z0)) -> #false #eq(#0, #s(z0)) -> #false #eq(#neg(z0), #0) -> #false #eq(#neg(z0), #neg(z1)) -> #eq(z0, z1) #eq(#neg(z0), #pos(z1)) -> #false #eq(#pos(z0), #0) -> #false #eq(#pos(z0), #neg(z1)) -> #false #eq(#pos(z0), #pos(z1)) -> #eq(z0, z1) #eq(#s(z0), #0) -> #false #eq(#s(z0), #s(z1)) -> #eq(z0, z1) #eq(::(z0, z1), ::(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #eq(::(z0, z1), nil) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #equal(z0, z1) -> #eq(z0, z1) and(z0, z1) -> #and(z0, z1) eq(z0, z1) -> eq#1(z0, z1) eq#1(::(z0, z1), z2) -> eq#3(z2, z0, z1) eq#1(nil, z0) -> eq#2(z0) eq#2(::(z0, z1)) -> #false eq#2(nil) -> #true eq#3(::(z0, z1), z2, z3) -> and(#equal(z2, z0), eq(z3, z1)) eq#3(nil, z0, z1) -> #false nub(z0) -> nub#1(z0) nub#1(::(z0, z1)) -> ::(z0, nub(remove(z0, z1))) nub#1(nil) -> nil remove(z0, z1) -> remove#1(z1, z0) remove#1(::(z0, z1), z2) -> remove#2(eq(z2, z0), z2, z0, z1) remove#1(nil, z0) -> nil remove#2(#false, z0, z1, z2) -> ::(z1, remove(z0, z2)) remove#2(#true, z0, z1, z2) -> remove(z0, z2) Rewrite Strategy: INNERMOST