WORST_CASE(Omega(n^1),?) proof of /export/starexec/sandbox2/benchmark/theBenchmark.trs # AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 963 ms] (2) CpxRelTRS (3) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (4) TRS for Loop Detection (5) DecreasingLoopProof [LOWER BOUND(ID), 383 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: #LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1)) MERGE(z0, z1) -> c16(MERGE#1(z0, z1)) MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1)) MERGE#1(nil, z0) -> c18 MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0)) MERGE#2(nil, z0, z1) -> c20 MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3)) MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3))) MERGESORT(z0) -> c23(MERGESORT#1(z0)) MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0)) MERGESORT#1(nil) -> c25 MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1)))) MERGESORT#2(nil, z0) -> c27 MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0)) MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1)) MSPLIT(z0) -> c30(MSPLIT#1(z0)) MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0)) MSPLIT#1(nil) -> c32 MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1)) MSPLIT#2(nil, z0) -> c34 MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35 The (relative) TRS S consists of the following rules: #CKLT(#EQ) -> c #CKLT(#GT) -> c1 #CKLT(#LT) -> c2 #COMPARE(#0, #0) -> c3 #COMPARE(#0, #neg(z0)) -> c4 #COMPARE(#0, #pos(z0)) -> c5 #COMPARE(#0, #s(z0)) -> c6 #COMPARE(#neg(z0), #0) -> c7 #COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0)) #COMPARE(#neg(z0), #pos(z1)) -> c9 #COMPARE(#pos(z0), #0) -> c10 #COMPARE(#pos(z0), #neg(z1)) -> c11 #COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1)) #COMPARE(#s(z0), #0) -> c13 #COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1)) #cklt(#EQ) -> #false #cklt(#GT) -> #false #cklt(#LT) -> #true #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) #less(z0, z1) -> #cklt(#compare(z0, z1)) merge(z0, z1) -> merge#1(z0, z1) merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1) merge#1(nil, z0) -> z0 merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1) merge#2(nil, z0, z1) -> ::(z0, z1) merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3)) merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3))) mergesort(z0) -> mergesort#1(z0) mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0) mergesort#1(nil) -> nil mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1)))) mergesort#2(nil, z0) -> ::(z0, nil) mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1)) msplit(z0) -> msplit#1(z0) msplit#1(::(z0, z1)) -> msplit#2(z1, z0) msplit#1(nil) -> tuple#2(nil, nil) msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0) msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil) msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, 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: #LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1)) MERGE(z0, z1) -> c16(MERGE#1(z0, z1)) MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1)) MERGE#1(nil, z0) -> c18 MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0)) MERGE#2(nil, z0, z1) -> c20 MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3)) MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3))) MERGESORT(z0) -> c23(MERGESORT#1(z0)) MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0)) MERGESORT#1(nil) -> c25 MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1)))) MERGESORT#2(nil, z0) -> c27 MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0)) MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1)) MSPLIT(z0) -> c30(MSPLIT#1(z0)) MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0)) MSPLIT#1(nil) -> c32 MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1)) MSPLIT#2(nil, z0) -> c34 MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35 The (relative) TRS S consists of the following rules: #CKLT(#EQ) -> c #CKLT(#GT) -> c1 #CKLT(#LT) -> c2 #COMPARE(#0, #0) -> c3 #COMPARE(#0, #neg(z0)) -> c4 #COMPARE(#0, #pos(z0)) -> c5 #COMPARE(#0, #s(z0)) -> c6 #COMPARE(#neg(z0), #0) -> c7 #COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0)) #COMPARE(#neg(z0), #pos(z1)) -> c9 #COMPARE(#pos(z0), #0) -> c10 #COMPARE(#pos(z0), #neg(z1)) -> c11 #COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1)) #COMPARE(#s(z0), #0) -> c13 #COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1)) #cklt(#EQ) -> #false #cklt(#GT) -> #false #cklt(#LT) -> #true #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) #less(z0, z1) -> #cklt(#compare(z0, z1)) merge(z0, z1) -> merge#1(z0, z1) merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1) merge#1(nil, z0) -> z0 merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1) merge#2(nil, z0, z1) -> ::(z0, z1) merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3)) merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3))) mergesort(z0) -> mergesort#1(z0) mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0) mergesort#1(nil) -> nil mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1)))) mergesort#2(nil, z0) -> ::(z0, nil) mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1)) msplit(z0) -> msplit#1(z0) msplit#1(::(z0, z1)) -> msplit#2(z1, z0) msplit#1(nil) -> tuple#2(nil, nil) msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0) msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil) msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, 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: #LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1)) MERGE(z0, z1) -> c16(MERGE#1(z0, z1)) MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1)) MERGE#1(nil, z0) -> c18 MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0)) MERGE#2(nil, z0, z1) -> c20 MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3)) MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3))) MERGESORT(z0) -> c23(MERGESORT#1(z0)) MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0)) MERGESORT#1(nil) -> c25 MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1)))) MERGESORT#2(nil, z0) -> c27 MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0)) MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1)) MSPLIT(z0) -> c30(MSPLIT#1(z0)) MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0)) MSPLIT#1(nil) -> c32 MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1)) MSPLIT#2(nil, z0) -> c34 MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35 The (relative) TRS S consists of the following rules: #CKLT(#EQ) -> c #CKLT(#GT) -> c1 #CKLT(#LT) -> c2 #COMPARE(#0, #0) -> c3 #COMPARE(#0, #neg(z0)) -> c4 #COMPARE(#0, #pos(z0)) -> c5 #COMPARE(#0, #s(z0)) -> c6 #COMPARE(#neg(z0), #0) -> c7 #COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0)) #COMPARE(#neg(z0), #pos(z1)) -> c9 #COMPARE(#pos(z0), #0) -> c10 #COMPARE(#pos(z0), #neg(z1)) -> c11 #COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1)) #COMPARE(#s(z0), #0) -> c13 #COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1)) #cklt(#EQ) -> #false #cklt(#GT) -> #false #cklt(#LT) -> #true #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) #less(z0, z1) -> #cklt(#compare(z0, z1)) merge(z0, z1) -> merge#1(z0, z1) merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1) merge#1(nil, z0) -> z0 merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1) merge#2(nil, z0, z1) -> ::(z0, z1) merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3)) merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3))) mergesort(z0) -> mergesort#1(z0) mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0) mergesort#1(nil) -> nil mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1)))) mergesort#2(nil, z0) -> ::(z0, nil) mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1)) msplit(z0) -> msplit#1(z0) msplit#1(::(z0, z1)) -> msplit#2(z1, z0) msplit#1(nil) -> tuple#2(nil, nil) msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0) msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil) msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, 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 MSPLIT(::(z01_1, ::(z01_0, z12_0))) ->^+ c30(c31(c33(MSPLIT#3(msplit(z12_0), z01_1, z01_0), MSPLIT(z12_0)))) gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0,1]. The pumping substitution is [z12_0 / ::(z01_1, ::(z01_0, z12_0))]. 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: #LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1)) MERGE(z0, z1) -> c16(MERGE#1(z0, z1)) MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1)) MERGE#1(nil, z0) -> c18 MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0)) MERGE#2(nil, z0, z1) -> c20 MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3)) MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3))) MERGESORT(z0) -> c23(MERGESORT#1(z0)) MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0)) MERGESORT#1(nil) -> c25 MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1)))) MERGESORT#2(nil, z0) -> c27 MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0)) MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1)) MSPLIT(z0) -> c30(MSPLIT#1(z0)) MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0)) MSPLIT#1(nil) -> c32 MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1)) MSPLIT#2(nil, z0) -> c34 MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35 The (relative) TRS S consists of the following rules: #CKLT(#EQ) -> c #CKLT(#GT) -> c1 #CKLT(#LT) -> c2 #COMPARE(#0, #0) -> c3 #COMPARE(#0, #neg(z0)) -> c4 #COMPARE(#0, #pos(z0)) -> c5 #COMPARE(#0, #s(z0)) -> c6 #COMPARE(#neg(z0), #0) -> c7 #COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0)) #COMPARE(#neg(z0), #pos(z1)) -> c9 #COMPARE(#pos(z0), #0) -> c10 #COMPARE(#pos(z0), #neg(z1)) -> c11 #COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1)) #COMPARE(#s(z0), #0) -> c13 #COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1)) #cklt(#EQ) -> #false #cklt(#GT) -> #false #cklt(#LT) -> #true #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) #less(z0, z1) -> #cklt(#compare(z0, z1)) merge(z0, z1) -> merge#1(z0, z1) merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1) merge#1(nil, z0) -> z0 merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1) merge#2(nil, z0, z1) -> ::(z0, z1) merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3)) merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3))) mergesort(z0) -> mergesort#1(z0) mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0) mergesort#1(nil) -> nil mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1)))) mergesort#2(nil, z0) -> ::(z0, nil) mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1)) msplit(z0) -> msplit#1(z0) msplit#1(::(z0, z1)) -> msplit#2(z1, z0) msplit#1(nil) -> tuple#2(nil, nil) msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0) msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil) msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, 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: #LESS(z0, z1) -> c15(#CKLT(#compare(z0, z1)), #COMPARE(z0, z1)) MERGE(z0, z1) -> c16(MERGE#1(z0, z1)) MERGE#1(::(z0, z1), z2) -> c17(MERGE#2(z2, z0, z1)) MERGE#1(nil, z0) -> c18 MERGE#2(::(z0, z1), z2, z3) -> c19(MERGE#3(#less(z2, z0), z2, z3, z0, z1), #LESS(z2, z0)) MERGE#2(nil, z0, z1) -> c20 MERGE#3(#false, z0, z1, z2, z3) -> c21(MERGE(::(z0, z1), z3)) MERGE#3(#true, z0, z1, z2, z3) -> c22(MERGE(z1, ::(z2, z3))) MERGESORT(z0) -> c23(MERGESORT#1(z0)) MERGESORT#1(::(z0, z1)) -> c24(MERGESORT#2(z1, z0)) MERGESORT#1(nil) -> c25 MERGESORT#2(::(z0, z1), z2) -> c26(MERGESORT#3(msplit(::(z2, ::(z0, z1)))), MSPLIT(::(z2, ::(z0, z1)))) MERGESORT#2(nil, z0) -> c27 MERGESORT#3(tuple#2(z0, z1)) -> c28(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z0)) MERGESORT#3(tuple#2(z0, z1)) -> c29(MERGE(mergesort(z0), mergesort(z1)), MERGESORT(z1)) MSPLIT(z0) -> c30(MSPLIT#1(z0)) MSPLIT#1(::(z0, z1)) -> c31(MSPLIT#2(z1, z0)) MSPLIT#1(nil) -> c32 MSPLIT#2(::(z0, z1), z2) -> c33(MSPLIT#3(msplit(z1), z2, z0), MSPLIT(z1)) MSPLIT#2(nil, z0) -> c34 MSPLIT#3(tuple#2(z0, z1), z2, z3) -> c35 The (relative) TRS S consists of the following rules: #CKLT(#EQ) -> c #CKLT(#GT) -> c1 #CKLT(#LT) -> c2 #COMPARE(#0, #0) -> c3 #COMPARE(#0, #neg(z0)) -> c4 #COMPARE(#0, #pos(z0)) -> c5 #COMPARE(#0, #s(z0)) -> c6 #COMPARE(#neg(z0), #0) -> c7 #COMPARE(#neg(z0), #neg(z1)) -> c8(#COMPARE(z1, z0)) #COMPARE(#neg(z0), #pos(z1)) -> c9 #COMPARE(#pos(z0), #0) -> c10 #COMPARE(#pos(z0), #neg(z1)) -> c11 #COMPARE(#pos(z0), #pos(z1)) -> c12(#COMPARE(z0, z1)) #COMPARE(#s(z0), #0) -> c13 #COMPARE(#s(z0), #s(z1)) -> c14(#COMPARE(z0, z1)) #cklt(#EQ) -> #false #cklt(#GT) -> #false #cklt(#LT) -> #true #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) #less(z0, z1) -> #cklt(#compare(z0, z1)) merge(z0, z1) -> merge#1(z0, z1) merge#1(::(z0, z1), z2) -> merge#2(z2, z0, z1) merge#1(nil, z0) -> z0 merge#2(::(z0, z1), z2, z3) -> merge#3(#less(z2, z0), z2, z3, z0, z1) merge#2(nil, z0, z1) -> ::(z0, z1) merge#3(#false, z0, z1, z2, z3) -> ::(z2, merge(::(z0, z1), z3)) merge#3(#true, z0, z1, z2, z3) -> ::(z0, merge(z1, ::(z2, z3))) mergesort(z0) -> mergesort#1(z0) mergesort#1(::(z0, z1)) -> mergesort#2(z1, z0) mergesort#1(nil) -> nil mergesort#2(::(z0, z1), z2) -> mergesort#3(msplit(::(z2, ::(z0, z1)))) mergesort#2(nil, z0) -> ::(z0, nil) mergesort#3(tuple#2(z0, z1)) -> merge(mergesort(z0), mergesort(z1)) msplit(z0) -> msplit#1(z0) msplit#1(::(z0, z1)) -> msplit#2(z1, z0) msplit#1(nil) -> tuple#2(nil, nil) msplit#2(::(z0, z1), z2) -> msplit#3(msplit(z1), z2, z0) msplit#2(nil, z0) -> tuple#2(::(z0, nil), nil) msplit#3(tuple#2(z0, z1), z2, z3) -> tuple#2(::(z2, z0), ::(z3, z1)) Rewrite Strategy: INNERMOST