WORST_CASE(Omega(n^1),?) 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, INF). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 1729 ms] (2) CpxRelTRS (3) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (4) TRS for Loop Detection (5) DecreasingLoopProof [LOWER BOUND(ID), 167 ms] (6) BEST (7) proven lower bound (8) LowerBoundPropagationProof [FINISHED, 0 ms] (9) BOUNDS(n^1, INF) (10) TRS for Loop Detection ---------------------------------------- (0) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: #EQUAL(z0, z1) -> c42(#EQ'(z0, z1)) #GREATER(z0, z1) -> c43(#CKGT(#compare(z0, z1)), #COMPARE(z0, z1)) APPEND(z0, z1) -> c44(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c45(APPEND(z1, z2)) APPEND#1(nil, z0) -> c46 INSERT(z0, z1) -> c47(INSERT#1(z0, z1, z0)) INSERT#1(tuple#2(z0, z1), z2, z3) -> c48(INSERT#2(z2, z1, z0, z3)) INSERT#2(::(z0, z1), z2, z3, z4) -> c49(INSERT#3(z0, z2, z1, z3, z4)) INSERT#2(nil, z0, z1, z2) -> c50 INSERT#3(tuple#2(z0, z1), z2, z3, z4, z5) -> c51(INSERT#4(#equal(z1, z2), z1, z3, z4, z0, z5), #EQUAL(z1, z2)) INSERT#4(#false, z0, z1, z2, z3, z4) -> c52(INSERT(z4, z1)) INSERT#4(#true, z0, z1, z2, z3, z4) -> c53 QUICKSORT(z0) -> c54(QUICKSORT#1(z0)) QUICKSORT#1(::(z0, z1)) -> c55(QUICKSORT#2(splitqs(z0, z1), z0), SPLITQS(z0, z1)) QUICKSORT#1(nil) -> c56 QUICKSORT#2(tuple#2(z0, z1), z2) -> c57(APPEND(quicksort(z0), ::(z2, quicksort(z1))), QUICKSORT(z0)) QUICKSORT#2(tuple#2(z0, z1), z2) -> c58(APPEND(quicksort(z0), ::(z2, quicksort(z1))), QUICKSORT(z1)) SORTALL(z0) -> c59(SORTALL#1(z0)) SORTALL#1(::(z0, z1)) -> c60(SORTALL#2(z0, z1)) SORTALL#1(nil) -> c61 SORTALL#2(tuple#2(z0, z1), z2) -> c62(QUICKSORT(z0)) SORTALL#2(tuple#2(z0, z1), z2) -> c63(SORTALL(z2)) SPLIT(z0) -> c64(SPLIT#1(z0)) SPLIT#1(::(z0, z1)) -> c65(INSERT(z0, split(z1)), SPLIT(z1)) SPLIT#1(nil) -> c66 SPLITANDSORT(z0) -> c67(SORTALL(split(z0)), SPLIT(z0)) SPLITQS(z0, z1) -> c68(SPLITQS#1(z1, z0)) SPLITQS#1(::(z0, z1), z2) -> c69(SPLITQS#2(splitqs(z2, z1), z2, z0), SPLITQS(z2, z1)) SPLITQS#1(nil, z0) -> c70 SPLITQS#2(tuple#2(z0, z1), z2, z3) -> c71(SPLITQS#3(#greater(z3, z2), z0, z1, z3), #GREATER(z3, z2)) SPLITQS#3(#false, z0, z1, z2) -> c72 SPLITQS#3(#true, z0, z1, z2) -> c73 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 #CKGT(#EQ) -> c4 #CKGT(#GT) -> c5 #CKGT(#LT) -> c6 #COMPARE(#0, #0) -> c7 #COMPARE(#0, #neg(z0)) -> c8 #COMPARE(#0, #pos(z0)) -> c9 #COMPARE(#0, #s(z0)) -> c10 #COMPARE(#neg(z0), #0) -> c11 #COMPARE(#neg(z0), #neg(z1)) -> c12(#COMPARE(z1, z0)) #COMPARE(#neg(z0), #pos(z1)) -> c13 #COMPARE(#pos(z0), #0) -> c14 #COMPARE(#pos(z0), #neg(z1)) -> c15 #COMPARE(#pos(z0), #pos(z1)) -> c16(#COMPARE(z0, z1)) #COMPARE(#s(z0), #0) -> c17 #COMPARE(#s(z0), #s(z1)) -> c18(#COMPARE(z0, z1)) #EQ'(#0, #0) -> c19 #EQ'(#0, #neg(z0)) -> c20 #EQ'(#0, #pos(z0)) -> c21 #EQ'(#0, #s(z0)) -> c22 #EQ'(#neg(z0), #0) -> c23 #EQ'(#neg(z0), #neg(z1)) -> c24(#EQ'(z0, z1)) #EQ'(#neg(z0), #pos(z1)) -> c25 #EQ'(#pos(z0), #0) -> c26 #EQ'(#pos(z0), #neg(z1)) -> c27 #EQ'(#pos(z0), #pos(z1)) -> c28(#EQ'(z0, z1)) #EQ'(#s(z0), #0) -> c29 #EQ'(#s(z0), #s(z1)) -> c30(#EQ'(z0, z1)) #EQ'(::(z0, z1), ::(z2, z3)) -> c31(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c32(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #EQ'(::(z0, z1), nil) -> c33 #EQ'(::(z0, z1), tuple#2(z2, z3)) -> c34 #EQ'(nil, ::(z0, z1)) -> c35 #EQ'(nil, nil) -> c36 #EQ'(nil, tuple#2(z0, z1)) -> c37 #EQ'(tuple#2(z0, z1), ::(z2, z3)) -> c38 #EQ'(tuple#2(z0, z1), nil) -> c39 #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c40(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c41(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(z0)) -> #GT #compare(#0, #pos(z0)) -> #LT #compare(#0, #s(z0)) -> #LT #compare(#neg(z0), #0) -> #LT #compare(#neg(z0), #neg(z1)) -> #compare(z1, z0) #compare(#neg(z0), #pos(z1)) -> #LT #compare(#pos(z0), #0) -> #GT #compare(#pos(z0), #neg(z1)) -> #GT #compare(#pos(z0), #pos(z1)) -> #compare(z0, z1) #compare(#s(z0), #0) -> #GT #compare(#s(z0), #s(z1)) -> #compare(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(::(z0, z1), tuple#2(z2, z3)) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #eq(nil, tuple#2(z0, z1)) -> #false #eq(tuple#2(z0, z1), ::(z2, z3)) -> #false #eq(tuple#2(z0, z1), nil) -> #false #eq(tuple#2(z0, z1), tuple#2(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #equal(z0, z1) -> #eq(z0, z1) #greater(z0, z1) -> #ckgt(#compare(z0, z1)) append(z0, z1) -> append#1(z0, z1) append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) append#1(nil, z0) -> z0 insert(z0, z1) -> insert#1(z0, z1, z0) insert#1(tuple#2(z0, z1), z2, z3) -> insert#2(z2, z1, z0, z3) insert#2(::(z0, z1), z2, z3, z4) -> insert#3(z0, z2, z1, z3, z4) insert#2(nil, z0, z1, z2) -> ::(tuple#2(::(z1, nil), z0), nil) insert#3(tuple#2(z0, z1), z2, z3, z4, z5) -> insert#4(#equal(z1, z2), z1, z3, z4, z0, z5) insert#4(#false, z0, z1, z2, z3, z4) -> ::(tuple#2(z3, z0), insert(z4, z1)) insert#4(#true, z0, z1, z2, z3, z4) -> ::(tuple#2(::(z2, z3), z0), z1) quicksort(z0) -> quicksort#1(z0) quicksort#1(::(z0, z1)) -> quicksort#2(splitqs(z0, z1), z0) quicksort#1(nil) -> nil quicksort#2(tuple#2(z0, z1), z2) -> append(quicksort(z0), ::(z2, quicksort(z1))) sortAll(z0) -> sortAll#1(z0) sortAll#1(::(z0, z1)) -> sortAll#2(z0, z1) sortAll#1(nil) -> nil sortAll#2(tuple#2(z0, z1), z2) -> ::(tuple#2(quicksort(z0), z1), sortAll(z2)) split(z0) -> split#1(z0) split#1(::(z0, z1)) -> insert(z0, split(z1)) split#1(nil) -> nil splitAndSort(z0) -> sortAll(split(z0)) splitqs(z0, z1) -> splitqs#1(z1, z0) splitqs#1(::(z0, z1), z2) -> splitqs#2(splitqs(z2, z1), z2, z0) splitqs#1(nil, z0) -> tuple#2(nil, nil) splitqs#2(tuple#2(z0, z1), z2, z3) -> splitqs#3(#greater(z3, z2), z0, z1, z3) splitqs#3(#false, z0, z1, z2) -> tuple#2(::(z2, z0), z1) splitqs#3(#true, z0, z1, z2) -> tuple#2(z0, ::(z2, z1)) 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, INF). The TRS R consists of the following rules: #EQUAL(z0, z1) -> c42(#EQ'(z0, z1)) #GREATER(z0, z1) -> c43(#CKGT(#compare(z0, z1)), #COMPARE(z0, z1)) APPEND(z0, z1) -> c44(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c45(APPEND(z1, z2)) APPEND#1(nil, z0) -> c46 INSERT(z0, z1) -> c47(INSERT#1(z0, z1, z0)) INSERT#1(tuple#2(z0, z1), z2, z3) -> c48(INSERT#2(z2, z1, z0, z3)) INSERT#2(::(z0, z1), z2, z3, z4) -> c49(INSERT#3(z0, z2, z1, z3, z4)) INSERT#2(nil, z0, z1, z2) -> c50 INSERT#3(tuple#2(z0, z1), z2, z3, z4, z5) -> c51(INSERT#4(#equal(z1, z2), z1, z3, z4, z0, z5), #EQUAL(z1, z2)) INSERT#4(#false, z0, z1, z2, z3, z4) -> c52(INSERT(z4, z1)) INSERT#4(#true, z0, z1, z2, z3, z4) -> c53 QUICKSORT(z0) -> c54(QUICKSORT#1(z0)) QUICKSORT#1(::(z0, z1)) -> c55(QUICKSORT#2(splitqs(z0, z1), z0), SPLITQS(z0, z1)) QUICKSORT#1(nil) -> c56 QUICKSORT#2(tuple#2(z0, z1), z2) -> c57(APPEND(quicksort(z0), ::(z2, quicksort(z1))), QUICKSORT(z0)) QUICKSORT#2(tuple#2(z0, z1), z2) -> c58(APPEND(quicksort(z0), ::(z2, quicksort(z1))), QUICKSORT(z1)) SORTALL(z0) -> c59(SORTALL#1(z0)) SORTALL#1(::(z0, z1)) -> c60(SORTALL#2(z0, z1)) SORTALL#1(nil) -> c61 SORTALL#2(tuple#2(z0, z1), z2) -> c62(QUICKSORT(z0)) SORTALL#2(tuple#2(z0, z1), z2) -> c63(SORTALL(z2)) SPLIT(z0) -> c64(SPLIT#1(z0)) SPLIT#1(::(z0, z1)) -> c65(INSERT(z0, split(z1)), SPLIT(z1)) SPLIT#1(nil) -> c66 SPLITANDSORT(z0) -> c67(SORTALL(split(z0)), SPLIT(z0)) SPLITQS(z0, z1) -> c68(SPLITQS#1(z1, z0)) SPLITQS#1(::(z0, z1), z2) -> c69(SPLITQS#2(splitqs(z2, z1), z2, z0), SPLITQS(z2, z1)) SPLITQS#1(nil, z0) -> c70 SPLITQS#2(tuple#2(z0, z1), z2, z3) -> c71(SPLITQS#3(#greater(z3, z2), z0, z1, z3), #GREATER(z3, z2)) SPLITQS#3(#false, z0, z1, z2) -> c72 SPLITQS#3(#true, z0, z1, z2) -> c73 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 #CKGT(#EQ) -> c4 #CKGT(#GT) -> c5 #CKGT(#LT) -> c6 #COMPARE(#0, #0) -> c7 #COMPARE(#0, #neg(z0)) -> c8 #COMPARE(#0, #pos(z0)) -> c9 #COMPARE(#0, #s(z0)) -> c10 #COMPARE(#neg(z0), #0) -> c11 #COMPARE(#neg(z0), #neg(z1)) -> c12(#COMPARE(z1, z0)) #COMPARE(#neg(z0), #pos(z1)) -> c13 #COMPARE(#pos(z0), #0) -> c14 #COMPARE(#pos(z0), #neg(z1)) -> c15 #COMPARE(#pos(z0), #pos(z1)) -> c16(#COMPARE(z0, z1)) #COMPARE(#s(z0), #0) -> c17 #COMPARE(#s(z0), #s(z1)) -> c18(#COMPARE(z0, z1)) #EQ'(#0, #0) -> c19 #EQ'(#0, #neg(z0)) -> c20 #EQ'(#0, #pos(z0)) -> c21 #EQ'(#0, #s(z0)) -> c22 #EQ'(#neg(z0), #0) -> c23 #EQ'(#neg(z0), #neg(z1)) -> c24(#EQ'(z0, z1)) #EQ'(#neg(z0), #pos(z1)) -> c25 #EQ'(#pos(z0), #0) -> c26 #EQ'(#pos(z0), #neg(z1)) -> c27 #EQ'(#pos(z0), #pos(z1)) -> c28(#EQ'(z0, z1)) #EQ'(#s(z0), #0) -> c29 #EQ'(#s(z0), #s(z1)) -> c30(#EQ'(z0, z1)) #EQ'(::(z0, z1), ::(z2, z3)) -> c31(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c32(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #EQ'(::(z0, z1), nil) -> c33 #EQ'(::(z0, z1), tuple#2(z2, z3)) -> c34 #EQ'(nil, ::(z0, z1)) -> c35 #EQ'(nil, nil) -> c36 #EQ'(nil, tuple#2(z0, z1)) -> c37 #EQ'(tuple#2(z0, z1), ::(z2, z3)) -> c38 #EQ'(tuple#2(z0, z1), nil) -> c39 #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c40(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c41(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(z0)) -> #GT #compare(#0, #pos(z0)) -> #LT #compare(#0, #s(z0)) -> #LT #compare(#neg(z0), #0) -> #LT #compare(#neg(z0), #neg(z1)) -> #compare(z1, z0) #compare(#neg(z0), #pos(z1)) -> #LT #compare(#pos(z0), #0) -> #GT #compare(#pos(z0), #neg(z1)) -> #GT #compare(#pos(z0), #pos(z1)) -> #compare(z0, z1) #compare(#s(z0), #0) -> #GT #compare(#s(z0), #s(z1)) -> #compare(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(::(z0, z1), tuple#2(z2, z3)) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #eq(nil, tuple#2(z0, z1)) -> #false #eq(tuple#2(z0, z1), ::(z2, z3)) -> #false #eq(tuple#2(z0, z1), nil) -> #false #eq(tuple#2(z0, z1), tuple#2(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #equal(z0, z1) -> #eq(z0, z1) #greater(z0, z1) -> #ckgt(#compare(z0, z1)) append(z0, z1) -> append#1(z0, z1) append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) append#1(nil, z0) -> z0 insert(z0, z1) -> insert#1(z0, z1, z0) insert#1(tuple#2(z0, z1), z2, z3) -> insert#2(z2, z1, z0, z3) insert#2(::(z0, z1), z2, z3, z4) -> insert#3(z0, z2, z1, z3, z4) insert#2(nil, z0, z1, z2) -> ::(tuple#2(::(z1, nil), z0), nil) insert#3(tuple#2(z0, z1), z2, z3, z4, z5) -> insert#4(#equal(z1, z2), z1, z3, z4, z0, z5) insert#4(#false, z0, z1, z2, z3, z4) -> ::(tuple#2(z3, z0), insert(z4, z1)) insert#4(#true, z0, z1, z2, z3, z4) -> ::(tuple#2(::(z2, z3), z0), z1) quicksort(z0) -> quicksort#1(z0) quicksort#1(::(z0, z1)) -> quicksort#2(splitqs(z0, z1), z0) quicksort#1(nil) -> nil quicksort#2(tuple#2(z0, z1), z2) -> append(quicksort(z0), ::(z2, quicksort(z1))) sortAll(z0) -> sortAll#1(z0) sortAll#1(::(z0, z1)) -> sortAll#2(z0, z1) sortAll#1(nil) -> nil sortAll#2(tuple#2(z0, z1), z2) -> ::(tuple#2(quicksort(z0), z1), sortAll(z2)) split(z0) -> split#1(z0) split#1(::(z0, z1)) -> insert(z0, split(z1)) split#1(nil) -> nil splitAndSort(z0) -> sortAll(split(z0)) splitqs(z0, z1) -> splitqs#1(z1, z0) splitqs#1(::(z0, z1), z2) -> splitqs#2(splitqs(z2, z1), z2, z0) splitqs#1(nil, z0) -> tuple#2(nil, nil) splitqs#2(tuple#2(z0, z1), z2, z3) -> splitqs#3(#greater(z3, z2), z0, z1, z3) splitqs#3(#false, z0, z1, z2) -> tuple#2(::(z2, z0), z1) splitqs#3(#true, z0, z1, z2) -> tuple#2(z0, ::(z2, z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (3) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID)) Transformed a relative TRS into a decreasing-loop problem. ---------------------------------------- (4) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: #EQUAL(z0, z1) -> c42(#EQ'(z0, z1)) #GREATER(z0, z1) -> c43(#CKGT(#compare(z0, z1)), #COMPARE(z0, z1)) APPEND(z0, z1) -> c44(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c45(APPEND(z1, z2)) APPEND#1(nil, z0) -> c46 INSERT(z0, z1) -> c47(INSERT#1(z0, z1, z0)) INSERT#1(tuple#2(z0, z1), z2, z3) -> c48(INSERT#2(z2, z1, z0, z3)) INSERT#2(::(z0, z1), z2, z3, z4) -> c49(INSERT#3(z0, z2, z1, z3, z4)) INSERT#2(nil, z0, z1, z2) -> c50 INSERT#3(tuple#2(z0, z1), z2, z3, z4, z5) -> c51(INSERT#4(#equal(z1, z2), z1, z3, z4, z0, z5), #EQUAL(z1, z2)) INSERT#4(#false, z0, z1, z2, z3, z4) -> c52(INSERT(z4, z1)) INSERT#4(#true, z0, z1, z2, z3, z4) -> c53 QUICKSORT(z0) -> c54(QUICKSORT#1(z0)) QUICKSORT#1(::(z0, z1)) -> c55(QUICKSORT#2(splitqs(z0, z1), z0), SPLITQS(z0, z1)) QUICKSORT#1(nil) -> c56 QUICKSORT#2(tuple#2(z0, z1), z2) -> c57(APPEND(quicksort(z0), ::(z2, quicksort(z1))), QUICKSORT(z0)) QUICKSORT#2(tuple#2(z0, z1), z2) -> c58(APPEND(quicksort(z0), ::(z2, quicksort(z1))), QUICKSORT(z1)) SORTALL(z0) -> c59(SORTALL#1(z0)) SORTALL#1(::(z0, z1)) -> c60(SORTALL#2(z0, z1)) SORTALL#1(nil) -> c61 SORTALL#2(tuple#2(z0, z1), z2) -> c62(QUICKSORT(z0)) SORTALL#2(tuple#2(z0, z1), z2) -> c63(SORTALL(z2)) SPLIT(z0) -> c64(SPLIT#1(z0)) SPLIT#1(::(z0, z1)) -> c65(INSERT(z0, split(z1)), SPLIT(z1)) SPLIT#1(nil) -> c66 SPLITANDSORT(z0) -> c67(SORTALL(split(z0)), SPLIT(z0)) SPLITQS(z0, z1) -> c68(SPLITQS#1(z1, z0)) SPLITQS#1(::(z0, z1), z2) -> c69(SPLITQS#2(splitqs(z2, z1), z2, z0), SPLITQS(z2, z1)) SPLITQS#1(nil, z0) -> c70 SPLITQS#2(tuple#2(z0, z1), z2, z3) -> c71(SPLITQS#3(#greater(z3, z2), z0, z1, z3), #GREATER(z3, z2)) SPLITQS#3(#false, z0, z1, z2) -> c72 SPLITQS#3(#true, z0, z1, z2) -> c73 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 #CKGT(#EQ) -> c4 #CKGT(#GT) -> c5 #CKGT(#LT) -> c6 #COMPARE(#0, #0) -> c7 #COMPARE(#0, #neg(z0)) -> c8 #COMPARE(#0, #pos(z0)) -> c9 #COMPARE(#0, #s(z0)) -> c10 #COMPARE(#neg(z0), #0) -> c11 #COMPARE(#neg(z0), #neg(z1)) -> c12(#COMPARE(z1, z0)) #COMPARE(#neg(z0), #pos(z1)) -> c13 #COMPARE(#pos(z0), #0) -> c14 #COMPARE(#pos(z0), #neg(z1)) -> c15 #COMPARE(#pos(z0), #pos(z1)) -> c16(#COMPARE(z0, z1)) #COMPARE(#s(z0), #0) -> c17 #COMPARE(#s(z0), #s(z1)) -> c18(#COMPARE(z0, z1)) #EQ'(#0, #0) -> c19 #EQ'(#0, #neg(z0)) -> c20 #EQ'(#0, #pos(z0)) -> c21 #EQ'(#0, #s(z0)) -> c22 #EQ'(#neg(z0), #0) -> c23 #EQ'(#neg(z0), #neg(z1)) -> c24(#EQ'(z0, z1)) #EQ'(#neg(z0), #pos(z1)) -> c25 #EQ'(#pos(z0), #0) -> c26 #EQ'(#pos(z0), #neg(z1)) -> c27 #EQ'(#pos(z0), #pos(z1)) -> c28(#EQ'(z0, z1)) #EQ'(#s(z0), #0) -> c29 #EQ'(#s(z0), #s(z1)) -> c30(#EQ'(z0, z1)) #EQ'(::(z0, z1), ::(z2, z3)) -> c31(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c32(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #EQ'(::(z0, z1), nil) -> c33 #EQ'(::(z0, z1), tuple#2(z2, z3)) -> c34 #EQ'(nil, ::(z0, z1)) -> c35 #EQ'(nil, nil) -> c36 #EQ'(nil, tuple#2(z0, z1)) -> c37 #EQ'(tuple#2(z0, z1), ::(z2, z3)) -> c38 #EQ'(tuple#2(z0, z1), nil) -> c39 #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c40(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c41(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(z0)) -> #GT #compare(#0, #pos(z0)) -> #LT #compare(#0, #s(z0)) -> #LT #compare(#neg(z0), #0) -> #LT #compare(#neg(z0), #neg(z1)) -> #compare(z1, z0) #compare(#neg(z0), #pos(z1)) -> #LT #compare(#pos(z0), #0) -> #GT #compare(#pos(z0), #neg(z1)) -> #GT #compare(#pos(z0), #pos(z1)) -> #compare(z0, z1) #compare(#s(z0), #0) -> #GT #compare(#s(z0), #s(z1)) -> #compare(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(::(z0, z1), tuple#2(z2, z3)) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #eq(nil, tuple#2(z0, z1)) -> #false #eq(tuple#2(z0, z1), ::(z2, z3)) -> #false #eq(tuple#2(z0, z1), nil) -> #false #eq(tuple#2(z0, z1), tuple#2(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #equal(z0, z1) -> #eq(z0, z1) #greater(z0, z1) -> #ckgt(#compare(z0, z1)) append(z0, z1) -> append#1(z0, z1) append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) append#1(nil, z0) -> z0 insert(z0, z1) -> insert#1(z0, z1, z0) insert#1(tuple#2(z0, z1), z2, z3) -> insert#2(z2, z1, z0, z3) insert#2(::(z0, z1), z2, z3, z4) -> insert#3(z0, z2, z1, z3, z4) insert#2(nil, z0, z1, z2) -> ::(tuple#2(::(z1, nil), z0), nil) insert#3(tuple#2(z0, z1), z2, z3, z4, z5) -> insert#4(#equal(z1, z2), z1, z3, z4, z0, z5) insert#4(#false, z0, z1, z2, z3, z4) -> ::(tuple#2(z3, z0), insert(z4, z1)) insert#4(#true, z0, z1, z2, z3, z4) -> ::(tuple#2(::(z2, z3), z0), z1) quicksort(z0) -> quicksort#1(z0) quicksort#1(::(z0, z1)) -> quicksort#2(splitqs(z0, z1), z0) quicksort#1(nil) -> nil quicksort#2(tuple#2(z0, z1), z2) -> append(quicksort(z0), ::(z2, quicksort(z1))) sortAll(z0) -> sortAll#1(z0) sortAll#1(::(z0, z1)) -> sortAll#2(z0, z1) sortAll#1(nil) -> nil sortAll#2(tuple#2(z0, z1), z2) -> ::(tuple#2(quicksort(z0), z1), sortAll(z2)) split(z0) -> split#1(z0) split#1(::(z0, z1)) -> insert(z0, split(z1)) split#1(nil) -> nil splitAndSort(z0) -> sortAll(split(z0)) splitqs(z0, z1) -> splitqs#1(z1, z0) splitqs#1(::(z0, z1), z2) -> splitqs#2(splitqs(z2, z1), z2, z0) splitqs#1(nil, z0) -> tuple#2(nil, nil) splitqs#2(tuple#2(z0, z1), z2, z3) -> splitqs#3(#greater(z3, z2), z0, z1, z3) splitqs#3(#false, z0, z1, z2) -> tuple#2(::(z2, z0), z1) splitqs#3(#true, z0, z1, z2) -> tuple#2(z0, ::(z2, z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (5) DecreasingLoopProof (LOWER BOUND(ID)) The following loop(s) give(s) rise to the lower bound Omega(n^1): The rewrite sequence APPEND(::(z01_2, z12_2), z1) ->^+ c44(c45(APPEND(z12_2, z1))) gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0]. The pumping substitution is [z12_2 / ::(z01_2, z12_2)]. The result substitution is [ ]. ---------------------------------------- (6) Complex Obligation (BEST) ---------------------------------------- (7) 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, INF). The TRS R consists of the following rules: #EQUAL(z0, z1) -> c42(#EQ'(z0, z1)) #GREATER(z0, z1) -> c43(#CKGT(#compare(z0, z1)), #COMPARE(z0, z1)) APPEND(z0, z1) -> c44(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c45(APPEND(z1, z2)) APPEND#1(nil, z0) -> c46 INSERT(z0, z1) -> c47(INSERT#1(z0, z1, z0)) INSERT#1(tuple#2(z0, z1), z2, z3) -> c48(INSERT#2(z2, z1, z0, z3)) INSERT#2(::(z0, z1), z2, z3, z4) -> c49(INSERT#3(z0, z2, z1, z3, z4)) INSERT#2(nil, z0, z1, z2) -> c50 INSERT#3(tuple#2(z0, z1), z2, z3, z4, z5) -> c51(INSERT#4(#equal(z1, z2), z1, z3, z4, z0, z5), #EQUAL(z1, z2)) INSERT#4(#false, z0, z1, z2, z3, z4) -> c52(INSERT(z4, z1)) INSERT#4(#true, z0, z1, z2, z3, z4) -> c53 QUICKSORT(z0) -> c54(QUICKSORT#1(z0)) QUICKSORT#1(::(z0, z1)) -> c55(QUICKSORT#2(splitqs(z0, z1), z0), SPLITQS(z0, z1)) QUICKSORT#1(nil) -> c56 QUICKSORT#2(tuple#2(z0, z1), z2) -> c57(APPEND(quicksort(z0), ::(z2, quicksort(z1))), QUICKSORT(z0)) QUICKSORT#2(tuple#2(z0, z1), z2) -> c58(APPEND(quicksort(z0), ::(z2, quicksort(z1))), QUICKSORT(z1)) SORTALL(z0) -> c59(SORTALL#1(z0)) SORTALL#1(::(z0, z1)) -> c60(SORTALL#2(z0, z1)) SORTALL#1(nil) -> c61 SORTALL#2(tuple#2(z0, z1), z2) -> c62(QUICKSORT(z0)) SORTALL#2(tuple#2(z0, z1), z2) -> c63(SORTALL(z2)) SPLIT(z0) -> c64(SPLIT#1(z0)) SPLIT#1(::(z0, z1)) -> c65(INSERT(z0, split(z1)), SPLIT(z1)) SPLIT#1(nil) -> c66 SPLITANDSORT(z0) -> c67(SORTALL(split(z0)), SPLIT(z0)) SPLITQS(z0, z1) -> c68(SPLITQS#1(z1, z0)) SPLITQS#1(::(z0, z1), z2) -> c69(SPLITQS#2(splitqs(z2, z1), z2, z0), SPLITQS(z2, z1)) SPLITQS#1(nil, z0) -> c70 SPLITQS#2(tuple#2(z0, z1), z2, z3) -> c71(SPLITQS#3(#greater(z3, z2), z0, z1, z3), #GREATER(z3, z2)) SPLITQS#3(#false, z0, z1, z2) -> c72 SPLITQS#3(#true, z0, z1, z2) -> c73 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 #CKGT(#EQ) -> c4 #CKGT(#GT) -> c5 #CKGT(#LT) -> c6 #COMPARE(#0, #0) -> c7 #COMPARE(#0, #neg(z0)) -> c8 #COMPARE(#0, #pos(z0)) -> c9 #COMPARE(#0, #s(z0)) -> c10 #COMPARE(#neg(z0), #0) -> c11 #COMPARE(#neg(z0), #neg(z1)) -> c12(#COMPARE(z1, z0)) #COMPARE(#neg(z0), #pos(z1)) -> c13 #COMPARE(#pos(z0), #0) -> c14 #COMPARE(#pos(z0), #neg(z1)) -> c15 #COMPARE(#pos(z0), #pos(z1)) -> c16(#COMPARE(z0, z1)) #COMPARE(#s(z0), #0) -> c17 #COMPARE(#s(z0), #s(z1)) -> c18(#COMPARE(z0, z1)) #EQ'(#0, #0) -> c19 #EQ'(#0, #neg(z0)) -> c20 #EQ'(#0, #pos(z0)) -> c21 #EQ'(#0, #s(z0)) -> c22 #EQ'(#neg(z0), #0) -> c23 #EQ'(#neg(z0), #neg(z1)) -> c24(#EQ'(z0, z1)) #EQ'(#neg(z0), #pos(z1)) -> c25 #EQ'(#pos(z0), #0) -> c26 #EQ'(#pos(z0), #neg(z1)) -> c27 #EQ'(#pos(z0), #pos(z1)) -> c28(#EQ'(z0, z1)) #EQ'(#s(z0), #0) -> c29 #EQ'(#s(z0), #s(z1)) -> c30(#EQ'(z0, z1)) #EQ'(::(z0, z1), ::(z2, z3)) -> c31(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c32(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #EQ'(::(z0, z1), nil) -> c33 #EQ'(::(z0, z1), tuple#2(z2, z3)) -> c34 #EQ'(nil, ::(z0, z1)) -> c35 #EQ'(nil, nil) -> c36 #EQ'(nil, tuple#2(z0, z1)) -> c37 #EQ'(tuple#2(z0, z1), ::(z2, z3)) -> c38 #EQ'(tuple#2(z0, z1), nil) -> c39 #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c40(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c41(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(z0)) -> #GT #compare(#0, #pos(z0)) -> #LT #compare(#0, #s(z0)) -> #LT #compare(#neg(z0), #0) -> #LT #compare(#neg(z0), #neg(z1)) -> #compare(z1, z0) #compare(#neg(z0), #pos(z1)) -> #LT #compare(#pos(z0), #0) -> #GT #compare(#pos(z0), #neg(z1)) -> #GT #compare(#pos(z0), #pos(z1)) -> #compare(z0, z1) #compare(#s(z0), #0) -> #GT #compare(#s(z0), #s(z1)) -> #compare(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(::(z0, z1), tuple#2(z2, z3)) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #eq(nil, tuple#2(z0, z1)) -> #false #eq(tuple#2(z0, z1), ::(z2, z3)) -> #false #eq(tuple#2(z0, z1), nil) -> #false #eq(tuple#2(z0, z1), tuple#2(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #equal(z0, z1) -> #eq(z0, z1) #greater(z0, z1) -> #ckgt(#compare(z0, z1)) append(z0, z1) -> append#1(z0, z1) append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) append#1(nil, z0) -> z0 insert(z0, z1) -> insert#1(z0, z1, z0) insert#1(tuple#2(z0, z1), z2, z3) -> insert#2(z2, z1, z0, z3) insert#2(::(z0, z1), z2, z3, z4) -> insert#3(z0, z2, z1, z3, z4) insert#2(nil, z0, z1, z2) -> ::(tuple#2(::(z1, nil), z0), nil) insert#3(tuple#2(z0, z1), z2, z3, z4, z5) -> insert#4(#equal(z1, z2), z1, z3, z4, z0, z5) insert#4(#false, z0, z1, z2, z3, z4) -> ::(tuple#2(z3, z0), insert(z4, z1)) insert#4(#true, z0, z1, z2, z3, z4) -> ::(tuple#2(::(z2, z3), z0), z1) quicksort(z0) -> quicksort#1(z0) quicksort#1(::(z0, z1)) -> quicksort#2(splitqs(z0, z1), z0) quicksort#1(nil) -> nil quicksort#2(tuple#2(z0, z1), z2) -> append(quicksort(z0), ::(z2, quicksort(z1))) sortAll(z0) -> sortAll#1(z0) sortAll#1(::(z0, z1)) -> sortAll#2(z0, z1) sortAll#1(nil) -> nil sortAll#2(tuple#2(z0, z1), z2) -> ::(tuple#2(quicksort(z0), z1), sortAll(z2)) split(z0) -> split#1(z0) split#1(::(z0, z1)) -> insert(z0, split(z1)) split#1(nil) -> nil splitAndSort(z0) -> sortAll(split(z0)) splitqs(z0, z1) -> splitqs#1(z1, z0) splitqs#1(::(z0, z1), z2) -> splitqs#2(splitqs(z2, z1), z2, z0) splitqs#1(nil, z0) -> tuple#2(nil, nil) splitqs#2(tuple#2(z0, z1), z2, z3) -> splitqs#3(#greater(z3, z2), z0, z1, z3) splitqs#3(#false, z0, z1, z2) -> tuple#2(::(z2, z0), z1) splitqs#3(#true, z0, z1, z2) -> tuple#2(z0, ::(z2, z1)) Rewrite Strategy: INNERMOST ---------------------------------------- (8) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (9) BOUNDS(n^1, INF) ---------------------------------------- (10) Obligation: Analyzing the following TRS for decreasing loops: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: #EQUAL(z0, z1) -> c42(#EQ'(z0, z1)) #GREATER(z0, z1) -> c43(#CKGT(#compare(z0, z1)), #COMPARE(z0, z1)) APPEND(z0, z1) -> c44(APPEND#1(z0, z1)) APPEND#1(::(z0, z1), z2) -> c45(APPEND(z1, z2)) APPEND#1(nil, z0) -> c46 INSERT(z0, z1) -> c47(INSERT#1(z0, z1, z0)) INSERT#1(tuple#2(z0, z1), z2, z3) -> c48(INSERT#2(z2, z1, z0, z3)) INSERT#2(::(z0, z1), z2, z3, z4) -> c49(INSERT#3(z0, z2, z1, z3, z4)) INSERT#2(nil, z0, z1, z2) -> c50 INSERT#3(tuple#2(z0, z1), z2, z3, z4, z5) -> c51(INSERT#4(#equal(z1, z2), z1, z3, z4, z0, z5), #EQUAL(z1, z2)) INSERT#4(#false, z0, z1, z2, z3, z4) -> c52(INSERT(z4, z1)) INSERT#4(#true, z0, z1, z2, z3, z4) -> c53 QUICKSORT(z0) -> c54(QUICKSORT#1(z0)) QUICKSORT#1(::(z0, z1)) -> c55(QUICKSORT#2(splitqs(z0, z1), z0), SPLITQS(z0, z1)) QUICKSORT#1(nil) -> c56 QUICKSORT#2(tuple#2(z0, z1), z2) -> c57(APPEND(quicksort(z0), ::(z2, quicksort(z1))), QUICKSORT(z0)) QUICKSORT#2(tuple#2(z0, z1), z2) -> c58(APPEND(quicksort(z0), ::(z2, quicksort(z1))), QUICKSORT(z1)) SORTALL(z0) -> c59(SORTALL#1(z0)) SORTALL#1(::(z0, z1)) -> c60(SORTALL#2(z0, z1)) SORTALL#1(nil) -> c61 SORTALL#2(tuple#2(z0, z1), z2) -> c62(QUICKSORT(z0)) SORTALL#2(tuple#2(z0, z1), z2) -> c63(SORTALL(z2)) SPLIT(z0) -> c64(SPLIT#1(z0)) SPLIT#1(::(z0, z1)) -> c65(INSERT(z0, split(z1)), SPLIT(z1)) SPLIT#1(nil) -> c66 SPLITANDSORT(z0) -> c67(SORTALL(split(z0)), SPLIT(z0)) SPLITQS(z0, z1) -> c68(SPLITQS#1(z1, z0)) SPLITQS#1(::(z0, z1), z2) -> c69(SPLITQS#2(splitqs(z2, z1), z2, z0), SPLITQS(z2, z1)) SPLITQS#1(nil, z0) -> c70 SPLITQS#2(tuple#2(z0, z1), z2, z3) -> c71(SPLITQS#3(#greater(z3, z2), z0, z1, z3), #GREATER(z3, z2)) SPLITQS#3(#false, z0, z1, z2) -> c72 SPLITQS#3(#true, z0, z1, z2) -> c73 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 #CKGT(#EQ) -> c4 #CKGT(#GT) -> c5 #CKGT(#LT) -> c6 #COMPARE(#0, #0) -> c7 #COMPARE(#0, #neg(z0)) -> c8 #COMPARE(#0, #pos(z0)) -> c9 #COMPARE(#0, #s(z0)) -> c10 #COMPARE(#neg(z0), #0) -> c11 #COMPARE(#neg(z0), #neg(z1)) -> c12(#COMPARE(z1, z0)) #COMPARE(#neg(z0), #pos(z1)) -> c13 #COMPARE(#pos(z0), #0) -> c14 #COMPARE(#pos(z0), #neg(z1)) -> c15 #COMPARE(#pos(z0), #pos(z1)) -> c16(#COMPARE(z0, z1)) #COMPARE(#s(z0), #0) -> c17 #COMPARE(#s(z0), #s(z1)) -> c18(#COMPARE(z0, z1)) #EQ'(#0, #0) -> c19 #EQ'(#0, #neg(z0)) -> c20 #EQ'(#0, #pos(z0)) -> c21 #EQ'(#0, #s(z0)) -> c22 #EQ'(#neg(z0), #0) -> c23 #EQ'(#neg(z0), #neg(z1)) -> c24(#EQ'(z0, z1)) #EQ'(#neg(z0), #pos(z1)) -> c25 #EQ'(#pos(z0), #0) -> c26 #EQ'(#pos(z0), #neg(z1)) -> c27 #EQ'(#pos(z0), #pos(z1)) -> c28(#EQ'(z0, z1)) #EQ'(#s(z0), #0) -> c29 #EQ'(#s(z0), #s(z1)) -> c30(#EQ'(z0, z1)) #EQ'(::(z0, z1), ::(z2, z3)) -> c31(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(::(z0, z1), ::(z2, z3)) -> c32(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #EQ'(::(z0, z1), nil) -> c33 #EQ'(::(z0, z1), tuple#2(z2, z3)) -> c34 #EQ'(nil, ::(z0, z1)) -> c35 #EQ'(nil, nil) -> c36 #EQ'(nil, tuple#2(z0, z1)) -> c37 #EQ'(tuple#2(z0, z1), ::(z2, z3)) -> c38 #EQ'(tuple#2(z0, z1), nil) -> c39 #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c40(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z0, z2)) #EQ'(tuple#2(z0, z1), tuple#2(z2, z3)) -> c41(#AND(#eq(z0, z2), #eq(z1, z3)), #EQ'(z1, z3)) #and(#false, #false) -> #false #and(#false, #true) -> #false #and(#true, #false) -> #false #and(#true, #true) -> #true #ckgt(#EQ) -> #false #ckgt(#GT) -> #true #ckgt(#LT) -> #false #compare(#0, #0) -> #EQ #compare(#0, #neg(z0)) -> #GT #compare(#0, #pos(z0)) -> #LT #compare(#0, #s(z0)) -> #LT #compare(#neg(z0), #0) -> #LT #compare(#neg(z0), #neg(z1)) -> #compare(z1, z0) #compare(#neg(z0), #pos(z1)) -> #LT #compare(#pos(z0), #0) -> #GT #compare(#pos(z0), #neg(z1)) -> #GT #compare(#pos(z0), #pos(z1)) -> #compare(z0, z1) #compare(#s(z0), #0) -> #GT #compare(#s(z0), #s(z1)) -> #compare(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(::(z0, z1), tuple#2(z2, z3)) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, nil) -> #true #eq(nil, tuple#2(z0, z1)) -> #false #eq(tuple#2(z0, z1), ::(z2, z3)) -> #false #eq(tuple#2(z0, z1), nil) -> #false #eq(tuple#2(z0, z1), tuple#2(z2, z3)) -> #and(#eq(z0, z2), #eq(z1, z3)) #equal(z0, z1) -> #eq(z0, z1) #greater(z0, z1) -> #ckgt(#compare(z0, z1)) append(z0, z1) -> append#1(z0, z1) append#1(::(z0, z1), z2) -> ::(z0, append(z1, z2)) append#1(nil, z0) -> z0 insert(z0, z1) -> insert#1(z0, z1, z0) insert#1(tuple#2(z0, z1), z2, z3) -> insert#2(z2, z1, z0, z3) insert#2(::(z0, z1), z2, z3, z4) -> insert#3(z0, z2, z1, z3, z4) insert#2(nil, z0, z1, z2) -> ::(tuple#2(::(z1, nil), z0), nil) insert#3(tuple#2(z0, z1), z2, z3, z4, z5) -> insert#4(#equal(z1, z2), z1, z3, z4, z0, z5) insert#4(#false, z0, z1, z2, z3, z4) -> ::(tuple#2(z3, z0), insert(z4, z1)) insert#4(#true, z0, z1, z2, z3, z4) -> ::(tuple#2(::(z2, z3), z0), z1) quicksort(z0) -> quicksort#1(z0) quicksort#1(::(z0, z1)) -> quicksort#2(splitqs(z0, z1), z0) quicksort#1(nil) -> nil quicksort#2(tuple#2(z0, z1), z2) -> append(quicksort(z0), ::(z2, quicksort(z1))) sortAll(z0) -> sortAll#1(z0) sortAll#1(::(z0, z1)) -> sortAll#2(z0, z1) sortAll#1(nil) -> nil sortAll#2(tuple#2(z0, z1), z2) -> ::(tuple#2(quicksort(z0), z1), sortAll(z2)) split(z0) -> split#1(z0) split#1(::(z0, z1)) -> insert(z0, split(z1)) split#1(nil) -> nil splitAndSort(z0) -> sortAll(split(z0)) splitqs(z0, z1) -> splitqs#1(z1, z0) splitqs#1(::(z0, z1), z2) -> splitqs#2(splitqs(z2, z1), z2, z0) splitqs#1(nil, z0) -> tuple#2(nil, nil) splitqs#2(tuple#2(z0, z1), z2, z3) -> splitqs#3(#greater(z3, z2), z0, z1, z3) splitqs#3(#false, z0, z1, z2) -> tuple#2(::(z2, z0), z1) splitqs#3(#true, z0, z1, z2) -> tuple#2(z0, ::(z2, z1)) Rewrite Strategy: INNERMOST