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), 2522 ms] (2) CpxRelTRS (3) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms] (4) TRS for Loop Detection (5) DecreasingLoopProof [LOWER BOUND(ID), 129 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) -> c35(#EQ(z0, z1)) APPENDREVERSE(z0, z1) -> c36(APPENDREVERSE#1(z0, z1)) APPENDREVERSE#1(::(z0, z1), z2) -> c37(APPENDREVERSE(z1, ::(z0, z2))) APPENDREVERSE#1(nil, z0) -> c38 BFS(z0, z1, z2) -> c39(BFS#1(z0, z1, z2)) BFS#1(::(z0, z1), z2, z3) -> c40(BFS#3(z0, z2, z1, z3)) BFS#1(nil, z0, z1) -> c41(BFS#2(z0, z1)) BFS#2(::(z0, z1), z2) -> c42(BFS(reverse(::(z0, z1)), nil, z2), REVERSE(::(z0, z1))) BFS#2(nil, z0) -> c43 BFS#3(leaf, z0, z1, z2) -> c44(BFS(z1, z0, z2)) BFS#3(node(z0, z1, z2), z3, z4, z5) -> c45(BFS#4(#equal(z5, z0), z3, z1, z2, z4, z5, z0), #EQUAL(z5, z0)) BFS#4(#false, z0, z1, z2, z3, z4, z5) -> c46(BFS(z3, ::(z2, ::(z1, z0)), z4)) BFS#4(#true, z0, z1, z2, z3, z4, z5) -> c47 BFS2(z0, z1) -> c48(BFS2#1(dobfs(z0, z1), z1), DOBFS(z0, z1)) BFS2#1(z0, z1) -> c49(DOBFS(z0, z1)) DFS(z0, z1) -> c50(DFS#1(z0, z1)) DFS#1(::(z0, z1), z2) -> c51(DFS#2(z0, z0, z1, z2)) DFS#1(nil, z0) -> c52 DFS#2(leaf, z0, z1, z2) -> c53(DFS(z1, z2)) DFS#2(node(z0, z1, z2), z3, z4, z5) -> c54(DFS#3(#equal(z0, z5), z3, z1, z2, z4, z5), #EQUAL(z0, z5)) DFS#3(#false, z0, z1, z2, z3, z4) -> c55(DFS(::(z1, ::(z2, z3)), z4)) DFS#3(#true, z0, z1, z2, z3, z4) -> c56 DOBFS(z0, z1) -> c57(BFS(::(z0, nil), nil, z1)) DODFS(z0, z1) -> c58(DFS(::(z0, nil), z1)) REVERSE(z0) -> c59(APPENDREVERSE(z0, nil)) 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), leaf) -> c18 #EQ(::(z0, z1), nil) -> c19 #EQ(::(z0, z1), node(z2, z3, z4)) -> c20 #EQ(leaf, ::(z0, z1)) -> c21 #EQ(leaf, leaf) -> c22 #EQ(leaf, nil) -> c23 #EQ(leaf, node(z0, z1, z2)) -> c24 #EQ(nil, ::(z0, z1)) -> c25 #EQ(nil, leaf) -> c26 #EQ(nil, nil) -> c27 #EQ(nil, node(z0, z1, z2)) -> c28 #EQ(node(z0, z1, z2), ::(z3, z4)) -> c29 #EQ(node(z0, z1, z2), leaf) -> c30 #EQ(node(z0, z1, z2), nil) -> c31 #EQ(node(z0, z1, z2), node(z3, z4, z5)) -> c32(#AND(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))), #EQ(z0, z3)) #EQ(node(z0, z1, z2), node(z3, z4, z5)) -> c33(#AND(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))), #AND(#eq(z1, z4), #eq(z2, z5)), #EQ(z1, z4)) #EQ(node(z0, z1, z2), node(z3, z4, z5)) -> c34(#AND(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))), #AND(#eq(z1, z4), #eq(z2, z5)), #EQ(z2, z5)) #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), leaf) -> #false #eq(::(z0, z1), nil) -> #false #eq(::(z0, z1), node(z2, z3, z4)) -> #false #eq(leaf, ::(z0, z1)) -> #false #eq(leaf, leaf) -> #true #eq(leaf, nil) -> #false #eq(leaf, node(z0, z1, z2)) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, leaf) -> #false #eq(nil, nil) -> #true #eq(nil, node(z0, z1, z2)) -> #false #eq(node(z0, z1, z2), ::(z3, z4)) -> #false #eq(node(z0, z1, z2), leaf) -> #false #eq(node(z0, z1, z2), nil) -> #false #eq(node(z0, z1, z2), node(z3, z4, z5)) -> #and(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))) #equal(z0, z1) -> #eq(z0, z1) appendreverse(z0, z1) -> appendreverse#1(z0, z1) appendreverse#1(::(z0, z1), z2) -> appendreverse(z1, ::(z0, z2)) appendreverse#1(nil, z0) -> z0 bfs(z0, z1, z2) -> bfs#1(z0, z1, z2) bfs#1(::(z0, z1), z2, z3) -> bfs#3(z0, z2, z1, z3) bfs#1(nil, z0, z1) -> bfs#2(z0, z1) bfs#2(::(z0, z1), z2) -> bfs(reverse(::(z0, z1)), nil, z2) bfs#2(nil, z0) -> leaf bfs#3(leaf, z0, z1, z2) -> bfs(z1, z0, z2) bfs#3(node(z0, z1, z2), z3, z4, z5) -> bfs#4(#equal(z5, z0), z3, z1, z2, z4, z5, z0) bfs#4(#false, z0, z1, z2, z3, z4, z5) -> bfs(z3, ::(z2, ::(z1, z0)), z4) bfs#4(#true, z0, z1, z2, z3, z4, z5) -> node(z5, z1, z2) bfs2(z0, z1) -> bfs2#1(dobfs(z0, z1), z1) bfs2#1(z0, z1) -> dobfs(z0, z1) dfs(z0, z1) -> dfs#1(z0, z1) dfs#1(::(z0, z1), z2) -> dfs#2(z0, z0, z1, z2) dfs#1(nil, z0) -> leaf dfs#2(leaf, z0, z1, z2) -> dfs(z1, z2) dfs#2(node(z0, z1, z2), z3, z4, z5) -> dfs#3(#equal(z0, z5), z3, z1, z2, z4, z5) dfs#3(#false, z0, z1, z2, z3, z4) -> dfs(::(z1, ::(z2, z3)), z4) dfs#3(#true, z0, z1, z2, z3, z4) -> z0 dobfs(z0, z1) -> bfs(::(z0, nil), nil, z1) dodfs(z0, z1) -> dfs(::(z0, nil), z1) reverse(z0) -> appendreverse(z0, nil) 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) -> c35(#EQ(z0, z1)) APPENDREVERSE(z0, z1) -> c36(APPENDREVERSE#1(z0, z1)) APPENDREVERSE#1(::(z0, z1), z2) -> c37(APPENDREVERSE(z1, ::(z0, z2))) APPENDREVERSE#1(nil, z0) -> c38 BFS(z0, z1, z2) -> c39(BFS#1(z0, z1, z2)) BFS#1(::(z0, z1), z2, z3) -> c40(BFS#3(z0, z2, z1, z3)) BFS#1(nil, z0, z1) -> c41(BFS#2(z0, z1)) BFS#2(::(z0, z1), z2) -> c42(BFS(reverse(::(z0, z1)), nil, z2), REVERSE(::(z0, z1))) BFS#2(nil, z0) -> c43 BFS#3(leaf, z0, z1, z2) -> c44(BFS(z1, z0, z2)) BFS#3(node(z0, z1, z2), z3, z4, z5) -> c45(BFS#4(#equal(z5, z0), z3, z1, z2, z4, z5, z0), #EQUAL(z5, z0)) BFS#4(#false, z0, z1, z2, z3, z4, z5) -> c46(BFS(z3, ::(z2, ::(z1, z0)), z4)) BFS#4(#true, z0, z1, z2, z3, z4, z5) -> c47 BFS2(z0, z1) -> c48(BFS2#1(dobfs(z0, z1), z1), DOBFS(z0, z1)) BFS2#1(z0, z1) -> c49(DOBFS(z0, z1)) DFS(z0, z1) -> c50(DFS#1(z0, z1)) DFS#1(::(z0, z1), z2) -> c51(DFS#2(z0, z0, z1, z2)) DFS#1(nil, z0) -> c52 DFS#2(leaf, z0, z1, z2) -> c53(DFS(z1, z2)) DFS#2(node(z0, z1, z2), z3, z4, z5) -> c54(DFS#3(#equal(z0, z5), z3, z1, z2, z4, z5), #EQUAL(z0, z5)) DFS#3(#false, z0, z1, z2, z3, z4) -> c55(DFS(::(z1, ::(z2, z3)), z4)) DFS#3(#true, z0, z1, z2, z3, z4) -> c56 DOBFS(z0, z1) -> c57(BFS(::(z0, nil), nil, z1)) DODFS(z0, z1) -> c58(DFS(::(z0, nil), z1)) REVERSE(z0) -> c59(APPENDREVERSE(z0, nil)) 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), leaf) -> c18 #EQ(::(z0, z1), nil) -> c19 #EQ(::(z0, z1), node(z2, z3, z4)) -> c20 #EQ(leaf, ::(z0, z1)) -> c21 #EQ(leaf, leaf) -> c22 #EQ(leaf, nil) -> c23 #EQ(leaf, node(z0, z1, z2)) -> c24 #EQ(nil, ::(z0, z1)) -> c25 #EQ(nil, leaf) -> c26 #EQ(nil, nil) -> c27 #EQ(nil, node(z0, z1, z2)) -> c28 #EQ(node(z0, z1, z2), ::(z3, z4)) -> c29 #EQ(node(z0, z1, z2), leaf) -> c30 #EQ(node(z0, z1, z2), nil) -> c31 #EQ(node(z0, z1, z2), node(z3, z4, z5)) -> c32(#AND(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))), #EQ(z0, z3)) #EQ(node(z0, z1, z2), node(z3, z4, z5)) -> c33(#AND(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))), #AND(#eq(z1, z4), #eq(z2, z5)), #EQ(z1, z4)) #EQ(node(z0, z1, z2), node(z3, z4, z5)) -> c34(#AND(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))), #AND(#eq(z1, z4), #eq(z2, z5)), #EQ(z2, z5)) #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), leaf) -> #false #eq(::(z0, z1), nil) -> #false #eq(::(z0, z1), node(z2, z3, z4)) -> #false #eq(leaf, ::(z0, z1)) -> #false #eq(leaf, leaf) -> #true #eq(leaf, nil) -> #false #eq(leaf, node(z0, z1, z2)) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, leaf) -> #false #eq(nil, nil) -> #true #eq(nil, node(z0, z1, z2)) -> #false #eq(node(z0, z1, z2), ::(z3, z4)) -> #false #eq(node(z0, z1, z2), leaf) -> #false #eq(node(z0, z1, z2), nil) -> #false #eq(node(z0, z1, z2), node(z3, z4, z5)) -> #and(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))) #equal(z0, z1) -> #eq(z0, z1) appendreverse(z0, z1) -> appendreverse#1(z0, z1) appendreverse#1(::(z0, z1), z2) -> appendreverse(z1, ::(z0, z2)) appendreverse#1(nil, z0) -> z0 bfs(z0, z1, z2) -> bfs#1(z0, z1, z2) bfs#1(::(z0, z1), z2, z3) -> bfs#3(z0, z2, z1, z3) bfs#1(nil, z0, z1) -> bfs#2(z0, z1) bfs#2(::(z0, z1), z2) -> bfs(reverse(::(z0, z1)), nil, z2) bfs#2(nil, z0) -> leaf bfs#3(leaf, z0, z1, z2) -> bfs(z1, z0, z2) bfs#3(node(z0, z1, z2), z3, z4, z5) -> bfs#4(#equal(z5, z0), z3, z1, z2, z4, z5, z0) bfs#4(#false, z0, z1, z2, z3, z4, z5) -> bfs(z3, ::(z2, ::(z1, z0)), z4) bfs#4(#true, z0, z1, z2, z3, z4, z5) -> node(z5, z1, z2) bfs2(z0, z1) -> bfs2#1(dobfs(z0, z1), z1) bfs2#1(z0, z1) -> dobfs(z0, z1) dfs(z0, z1) -> dfs#1(z0, z1) dfs#1(::(z0, z1), z2) -> dfs#2(z0, z0, z1, z2) dfs#1(nil, z0) -> leaf dfs#2(leaf, z0, z1, z2) -> dfs(z1, z2) dfs#2(node(z0, z1, z2), z3, z4, z5) -> dfs#3(#equal(z0, z5), z3, z1, z2, z4, z5) dfs#3(#false, z0, z1, z2, z3, z4) -> dfs(::(z1, ::(z2, z3)), z4) dfs#3(#true, z0, z1, z2, z3, z4) -> z0 dobfs(z0, z1) -> bfs(::(z0, nil), nil, z1) dodfs(z0, z1) -> dfs(::(z0, nil), z1) reverse(z0) -> appendreverse(z0, nil) 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) -> c35(#EQ(z0, z1)) APPENDREVERSE(z0, z1) -> c36(APPENDREVERSE#1(z0, z1)) APPENDREVERSE#1(::(z0, z1), z2) -> c37(APPENDREVERSE(z1, ::(z0, z2))) APPENDREVERSE#1(nil, z0) -> c38 BFS(z0, z1, z2) -> c39(BFS#1(z0, z1, z2)) BFS#1(::(z0, z1), z2, z3) -> c40(BFS#3(z0, z2, z1, z3)) BFS#1(nil, z0, z1) -> c41(BFS#2(z0, z1)) BFS#2(::(z0, z1), z2) -> c42(BFS(reverse(::(z0, z1)), nil, z2), REVERSE(::(z0, z1))) BFS#2(nil, z0) -> c43 BFS#3(leaf, z0, z1, z2) -> c44(BFS(z1, z0, z2)) BFS#3(node(z0, z1, z2), z3, z4, z5) -> c45(BFS#4(#equal(z5, z0), z3, z1, z2, z4, z5, z0), #EQUAL(z5, z0)) BFS#4(#false, z0, z1, z2, z3, z4, z5) -> c46(BFS(z3, ::(z2, ::(z1, z0)), z4)) BFS#4(#true, z0, z1, z2, z3, z4, z5) -> c47 BFS2(z0, z1) -> c48(BFS2#1(dobfs(z0, z1), z1), DOBFS(z0, z1)) BFS2#1(z0, z1) -> c49(DOBFS(z0, z1)) DFS(z0, z1) -> c50(DFS#1(z0, z1)) DFS#1(::(z0, z1), z2) -> c51(DFS#2(z0, z0, z1, z2)) DFS#1(nil, z0) -> c52 DFS#2(leaf, z0, z1, z2) -> c53(DFS(z1, z2)) DFS#2(node(z0, z1, z2), z3, z4, z5) -> c54(DFS#3(#equal(z0, z5), z3, z1, z2, z4, z5), #EQUAL(z0, z5)) DFS#3(#false, z0, z1, z2, z3, z4) -> c55(DFS(::(z1, ::(z2, z3)), z4)) DFS#3(#true, z0, z1, z2, z3, z4) -> c56 DOBFS(z0, z1) -> c57(BFS(::(z0, nil), nil, z1)) DODFS(z0, z1) -> c58(DFS(::(z0, nil), z1)) REVERSE(z0) -> c59(APPENDREVERSE(z0, nil)) 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), leaf) -> c18 #EQ(::(z0, z1), nil) -> c19 #EQ(::(z0, z1), node(z2, z3, z4)) -> c20 #EQ(leaf, ::(z0, z1)) -> c21 #EQ(leaf, leaf) -> c22 #EQ(leaf, nil) -> c23 #EQ(leaf, node(z0, z1, z2)) -> c24 #EQ(nil, ::(z0, z1)) -> c25 #EQ(nil, leaf) -> c26 #EQ(nil, nil) -> c27 #EQ(nil, node(z0, z1, z2)) -> c28 #EQ(node(z0, z1, z2), ::(z3, z4)) -> c29 #EQ(node(z0, z1, z2), leaf) -> c30 #EQ(node(z0, z1, z2), nil) -> c31 #EQ(node(z0, z1, z2), node(z3, z4, z5)) -> c32(#AND(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))), #EQ(z0, z3)) #EQ(node(z0, z1, z2), node(z3, z4, z5)) -> c33(#AND(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))), #AND(#eq(z1, z4), #eq(z2, z5)), #EQ(z1, z4)) #EQ(node(z0, z1, z2), node(z3, z4, z5)) -> c34(#AND(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))), #AND(#eq(z1, z4), #eq(z2, z5)), #EQ(z2, z5)) #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), leaf) -> #false #eq(::(z0, z1), nil) -> #false #eq(::(z0, z1), node(z2, z3, z4)) -> #false #eq(leaf, ::(z0, z1)) -> #false #eq(leaf, leaf) -> #true #eq(leaf, nil) -> #false #eq(leaf, node(z0, z1, z2)) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, leaf) -> #false #eq(nil, nil) -> #true #eq(nil, node(z0, z1, z2)) -> #false #eq(node(z0, z1, z2), ::(z3, z4)) -> #false #eq(node(z0, z1, z2), leaf) -> #false #eq(node(z0, z1, z2), nil) -> #false #eq(node(z0, z1, z2), node(z3, z4, z5)) -> #and(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))) #equal(z0, z1) -> #eq(z0, z1) appendreverse(z0, z1) -> appendreverse#1(z0, z1) appendreverse#1(::(z0, z1), z2) -> appendreverse(z1, ::(z0, z2)) appendreverse#1(nil, z0) -> z0 bfs(z0, z1, z2) -> bfs#1(z0, z1, z2) bfs#1(::(z0, z1), z2, z3) -> bfs#3(z0, z2, z1, z3) bfs#1(nil, z0, z1) -> bfs#2(z0, z1) bfs#2(::(z0, z1), z2) -> bfs(reverse(::(z0, z1)), nil, z2) bfs#2(nil, z0) -> leaf bfs#3(leaf, z0, z1, z2) -> bfs(z1, z0, z2) bfs#3(node(z0, z1, z2), z3, z4, z5) -> bfs#4(#equal(z5, z0), z3, z1, z2, z4, z5, z0) bfs#4(#false, z0, z1, z2, z3, z4, z5) -> bfs(z3, ::(z2, ::(z1, z0)), z4) bfs#4(#true, z0, z1, z2, z3, z4, z5) -> node(z5, z1, z2) bfs2(z0, z1) -> bfs2#1(dobfs(z0, z1), z1) bfs2#1(z0, z1) -> dobfs(z0, z1) dfs(z0, z1) -> dfs#1(z0, z1) dfs#1(::(z0, z1), z2) -> dfs#2(z0, z0, z1, z2) dfs#1(nil, z0) -> leaf dfs#2(leaf, z0, z1, z2) -> dfs(z1, z2) dfs#2(node(z0, z1, z2), z3, z4, z5) -> dfs#3(#equal(z0, z5), z3, z1, z2, z4, z5) dfs#3(#false, z0, z1, z2, z3, z4) -> dfs(::(z1, ::(z2, z3)), z4) dfs#3(#true, z0, z1, z2, z3, z4) -> z0 dobfs(z0, z1) -> bfs(::(z0, nil), nil, z1) dodfs(z0, z1) -> dfs(::(z0, nil), z1) reverse(z0) -> appendreverse(z0, nil) 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 APPENDREVERSE#1(::(z0, z1), z2) ->^+ c37(c36(APPENDREVERSE#1(z1, ::(z0, z2)))) gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0]. The pumping substitution is [z1 / ::(z0, z1)]. The result substitution is [z2 / ::(z0, z2)]. ---------------------------------------- (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) -> c35(#EQ(z0, z1)) APPENDREVERSE(z0, z1) -> c36(APPENDREVERSE#1(z0, z1)) APPENDREVERSE#1(::(z0, z1), z2) -> c37(APPENDREVERSE(z1, ::(z0, z2))) APPENDREVERSE#1(nil, z0) -> c38 BFS(z0, z1, z2) -> c39(BFS#1(z0, z1, z2)) BFS#1(::(z0, z1), z2, z3) -> c40(BFS#3(z0, z2, z1, z3)) BFS#1(nil, z0, z1) -> c41(BFS#2(z0, z1)) BFS#2(::(z0, z1), z2) -> c42(BFS(reverse(::(z0, z1)), nil, z2), REVERSE(::(z0, z1))) BFS#2(nil, z0) -> c43 BFS#3(leaf, z0, z1, z2) -> c44(BFS(z1, z0, z2)) BFS#3(node(z0, z1, z2), z3, z4, z5) -> c45(BFS#4(#equal(z5, z0), z3, z1, z2, z4, z5, z0), #EQUAL(z5, z0)) BFS#4(#false, z0, z1, z2, z3, z4, z5) -> c46(BFS(z3, ::(z2, ::(z1, z0)), z4)) BFS#4(#true, z0, z1, z2, z3, z4, z5) -> c47 BFS2(z0, z1) -> c48(BFS2#1(dobfs(z0, z1), z1), DOBFS(z0, z1)) BFS2#1(z0, z1) -> c49(DOBFS(z0, z1)) DFS(z0, z1) -> c50(DFS#1(z0, z1)) DFS#1(::(z0, z1), z2) -> c51(DFS#2(z0, z0, z1, z2)) DFS#1(nil, z0) -> c52 DFS#2(leaf, z0, z1, z2) -> c53(DFS(z1, z2)) DFS#2(node(z0, z1, z2), z3, z4, z5) -> c54(DFS#3(#equal(z0, z5), z3, z1, z2, z4, z5), #EQUAL(z0, z5)) DFS#3(#false, z0, z1, z2, z3, z4) -> c55(DFS(::(z1, ::(z2, z3)), z4)) DFS#3(#true, z0, z1, z2, z3, z4) -> c56 DOBFS(z0, z1) -> c57(BFS(::(z0, nil), nil, z1)) DODFS(z0, z1) -> c58(DFS(::(z0, nil), z1)) REVERSE(z0) -> c59(APPENDREVERSE(z0, nil)) 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), leaf) -> c18 #EQ(::(z0, z1), nil) -> c19 #EQ(::(z0, z1), node(z2, z3, z4)) -> c20 #EQ(leaf, ::(z0, z1)) -> c21 #EQ(leaf, leaf) -> c22 #EQ(leaf, nil) -> c23 #EQ(leaf, node(z0, z1, z2)) -> c24 #EQ(nil, ::(z0, z1)) -> c25 #EQ(nil, leaf) -> c26 #EQ(nil, nil) -> c27 #EQ(nil, node(z0, z1, z2)) -> c28 #EQ(node(z0, z1, z2), ::(z3, z4)) -> c29 #EQ(node(z0, z1, z2), leaf) -> c30 #EQ(node(z0, z1, z2), nil) -> c31 #EQ(node(z0, z1, z2), node(z3, z4, z5)) -> c32(#AND(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))), #EQ(z0, z3)) #EQ(node(z0, z1, z2), node(z3, z4, z5)) -> c33(#AND(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))), #AND(#eq(z1, z4), #eq(z2, z5)), #EQ(z1, z4)) #EQ(node(z0, z1, z2), node(z3, z4, z5)) -> c34(#AND(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))), #AND(#eq(z1, z4), #eq(z2, z5)), #EQ(z2, z5)) #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), leaf) -> #false #eq(::(z0, z1), nil) -> #false #eq(::(z0, z1), node(z2, z3, z4)) -> #false #eq(leaf, ::(z0, z1)) -> #false #eq(leaf, leaf) -> #true #eq(leaf, nil) -> #false #eq(leaf, node(z0, z1, z2)) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, leaf) -> #false #eq(nil, nil) -> #true #eq(nil, node(z0, z1, z2)) -> #false #eq(node(z0, z1, z2), ::(z3, z4)) -> #false #eq(node(z0, z1, z2), leaf) -> #false #eq(node(z0, z1, z2), nil) -> #false #eq(node(z0, z1, z2), node(z3, z4, z5)) -> #and(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))) #equal(z0, z1) -> #eq(z0, z1) appendreverse(z0, z1) -> appendreverse#1(z0, z1) appendreverse#1(::(z0, z1), z2) -> appendreverse(z1, ::(z0, z2)) appendreverse#1(nil, z0) -> z0 bfs(z0, z1, z2) -> bfs#1(z0, z1, z2) bfs#1(::(z0, z1), z2, z3) -> bfs#3(z0, z2, z1, z3) bfs#1(nil, z0, z1) -> bfs#2(z0, z1) bfs#2(::(z0, z1), z2) -> bfs(reverse(::(z0, z1)), nil, z2) bfs#2(nil, z0) -> leaf bfs#3(leaf, z0, z1, z2) -> bfs(z1, z0, z2) bfs#3(node(z0, z1, z2), z3, z4, z5) -> bfs#4(#equal(z5, z0), z3, z1, z2, z4, z5, z0) bfs#4(#false, z0, z1, z2, z3, z4, z5) -> bfs(z3, ::(z2, ::(z1, z0)), z4) bfs#4(#true, z0, z1, z2, z3, z4, z5) -> node(z5, z1, z2) bfs2(z0, z1) -> bfs2#1(dobfs(z0, z1), z1) bfs2#1(z0, z1) -> dobfs(z0, z1) dfs(z0, z1) -> dfs#1(z0, z1) dfs#1(::(z0, z1), z2) -> dfs#2(z0, z0, z1, z2) dfs#1(nil, z0) -> leaf dfs#2(leaf, z0, z1, z2) -> dfs(z1, z2) dfs#2(node(z0, z1, z2), z3, z4, z5) -> dfs#3(#equal(z0, z5), z3, z1, z2, z4, z5) dfs#3(#false, z0, z1, z2, z3, z4) -> dfs(::(z1, ::(z2, z3)), z4) dfs#3(#true, z0, z1, z2, z3, z4) -> z0 dobfs(z0, z1) -> bfs(::(z0, nil), nil, z1) dodfs(z0, z1) -> dfs(::(z0, nil), z1) reverse(z0) -> appendreverse(z0, nil) 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) -> c35(#EQ(z0, z1)) APPENDREVERSE(z0, z1) -> c36(APPENDREVERSE#1(z0, z1)) APPENDREVERSE#1(::(z0, z1), z2) -> c37(APPENDREVERSE(z1, ::(z0, z2))) APPENDREVERSE#1(nil, z0) -> c38 BFS(z0, z1, z2) -> c39(BFS#1(z0, z1, z2)) BFS#1(::(z0, z1), z2, z3) -> c40(BFS#3(z0, z2, z1, z3)) BFS#1(nil, z0, z1) -> c41(BFS#2(z0, z1)) BFS#2(::(z0, z1), z2) -> c42(BFS(reverse(::(z0, z1)), nil, z2), REVERSE(::(z0, z1))) BFS#2(nil, z0) -> c43 BFS#3(leaf, z0, z1, z2) -> c44(BFS(z1, z0, z2)) BFS#3(node(z0, z1, z2), z3, z4, z5) -> c45(BFS#4(#equal(z5, z0), z3, z1, z2, z4, z5, z0), #EQUAL(z5, z0)) BFS#4(#false, z0, z1, z2, z3, z4, z5) -> c46(BFS(z3, ::(z2, ::(z1, z0)), z4)) BFS#4(#true, z0, z1, z2, z3, z4, z5) -> c47 BFS2(z0, z1) -> c48(BFS2#1(dobfs(z0, z1), z1), DOBFS(z0, z1)) BFS2#1(z0, z1) -> c49(DOBFS(z0, z1)) DFS(z0, z1) -> c50(DFS#1(z0, z1)) DFS#1(::(z0, z1), z2) -> c51(DFS#2(z0, z0, z1, z2)) DFS#1(nil, z0) -> c52 DFS#2(leaf, z0, z1, z2) -> c53(DFS(z1, z2)) DFS#2(node(z0, z1, z2), z3, z4, z5) -> c54(DFS#3(#equal(z0, z5), z3, z1, z2, z4, z5), #EQUAL(z0, z5)) DFS#3(#false, z0, z1, z2, z3, z4) -> c55(DFS(::(z1, ::(z2, z3)), z4)) DFS#3(#true, z0, z1, z2, z3, z4) -> c56 DOBFS(z0, z1) -> c57(BFS(::(z0, nil), nil, z1)) DODFS(z0, z1) -> c58(DFS(::(z0, nil), z1)) REVERSE(z0) -> c59(APPENDREVERSE(z0, nil)) 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), leaf) -> c18 #EQ(::(z0, z1), nil) -> c19 #EQ(::(z0, z1), node(z2, z3, z4)) -> c20 #EQ(leaf, ::(z0, z1)) -> c21 #EQ(leaf, leaf) -> c22 #EQ(leaf, nil) -> c23 #EQ(leaf, node(z0, z1, z2)) -> c24 #EQ(nil, ::(z0, z1)) -> c25 #EQ(nil, leaf) -> c26 #EQ(nil, nil) -> c27 #EQ(nil, node(z0, z1, z2)) -> c28 #EQ(node(z0, z1, z2), ::(z3, z4)) -> c29 #EQ(node(z0, z1, z2), leaf) -> c30 #EQ(node(z0, z1, z2), nil) -> c31 #EQ(node(z0, z1, z2), node(z3, z4, z5)) -> c32(#AND(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))), #EQ(z0, z3)) #EQ(node(z0, z1, z2), node(z3, z4, z5)) -> c33(#AND(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))), #AND(#eq(z1, z4), #eq(z2, z5)), #EQ(z1, z4)) #EQ(node(z0, z1, z2), node(z3, z4, z5)) -> c34(#AND(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))), #AND(#eq(z1, z4), #eq(z2, z5)), #EQ(z2, z5)) #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), leaf) -> #false #eq(::(z0, z1), nil) -> #false #eq(::(z0, z1), node(z2, z3, z4)) -> #false #eq(leaf, ::(z0, z1)) -> #false #eq(leaf, leaf) -> #true #eq(leaf, nil) -> #false #eq(leaf, node(z0, z1, z2)) -> #false #eq(nil, ::(z0, z1)) -> #false #eq(nil, leaf) -> #false #eq(nil, nil) -> #true #eq(nil, node(z0, z1, z2)) -> #false #eq(node(z0, z1, z2), ::(z3, z4)) -> #false #eq(node(z0, z1, z2), leaf) -> #false #eq(node(z0, z1, z2), nil) -> #false #eq(node(z0, z1, z2), node(z3, z4, z5)) -> #and(#eq(z0, z3), #and(#eq(z1, z4), #eq(z2, z5))) #equal(z0, z1) -> #eq(z0, z1) appendreverse(z0, z1) -> appendreverse#1(z0, z1) appendreverse#1(::(z0, z1), z2) -> appendreverse(z1, ::(z0, z2)) appendreverse#1(nil, z0) -> z0 bfs(z0, z1, z2) -> bfs#1(z0, z1, z2) bfs#1(::(z0, z1), z2, z3) -> bfs#3(z0, z2, z1, z3) bfs#1(nil, z0, z1) -> bfs#2(z0, z1) bfs#2(::(z0, z1), z2) -> bfs(reverse(::(z0, z1)), nil, z2) bfs#2(nil, z0) -> leaf bfs#3(leaf, z0, z1, z2) -> bfs(z1, z0, z2) bfs#3(node(z0, z1, z2), z3, z4, z5) -> bfs#4(#equal(z5, z0), z3, z1, z2, z4, z5, z0) bfs#4(#false, z0, z1, z2, z3, z4, z5) -> bfs(z3, ::(z2, ::(z1, z0)), z4) bfs#4(#true, z0, z1, z2, z3, z4, z5) -> node(z5, z1, z2) bfs2(z0, z1) -> bfs2#1(dobfs(z0, z1), z1) bfs2#1(z0, z1) -> dobfs(z0, z1) dfs(z0, z1) -> dfs#1(z0, z1) dfs#1(::(z0, z1), z2) -> dfs#2(z0, z0, z1, z2) dfs#1(nil, z0) -> leaf dfs#2(leaf, z0, z1, z2) -> dfs(z1, z2) dfs#2(node(z0, z1, z2), z3, z4, z5) -> dfs#3(#equal(z0, z5), z3, z1, z2, z4, z5) dfs#3(#false, z0, z1, z2, z3, z4) -> dfs(::(z1, ::(z2, z3)), z4) dfs#3(#true, z0, z1, z2, z3, z4) -> z0 dobfs(z0, z1) -> bfs(::(z0, nil), nil, z1) dodfs(z0, z1) -> dfs(::(z0, nil), z1) reverse(z0) -> appendreverse(z0, nil) Rewrite Strategy: INNERMOST