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) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (2) CpxRelTRS (3) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (4) typed CpxTrs (5) OrderProof [LOWER BOUND(ID), 0 ms] (6) typed CpxTrs (7) RewriteLemmaProof [LOWER BOUND(ID), 307 ms] (8) BEST (9) proven lower bound (10) LowerBoundPropagationProof [FINISHED, 0 ms] (11) BOUNDS(n^1, INF) (12) typed CpxTrs (13) RewriteLemmaProof [LOWER BOUND(ID), 0 ms] (14) typed CpxTrs ---------------------------------------- (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: LT0(Cons(z0, z1), Cons(z2, z3)) -> c6(LT0(z1, z3)) LT0(z0, Nil) -> c7 G(z0, Nil) -> c8 G(z0, Cons(z1, z2)) -> c9(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) F(z0, Nil) -> c10 F(z0, Cons(z1, z2)) -> c11(F(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))), F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) F(z0, Cons(z1, z2)) -> c12(F(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))), F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) NUMBER42 -> c13 GOAL(z0, z1) -> c14(F(z0, z1)) GOAL(z0, z1) -> c15(G(z0, z1)) The (relative) TRS S consists of the following rules: G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c(G(z1, Cons(Cons(Nil, Nil), z2))) G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c1(G(z0, z2)) F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c2 F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c3 F[ITE][FALSE][ITE](False, z0, z1) -> c4 F[ITE][FALSE][ITE](True, z0, z1) -> c5 g[Ite][False][Ite](False, Cons(z0, z1), z2) -> g(z1, Cons(Cons(Nil, Nil), z2)) g[Ite][False][Ite](True, z0, Cons(z1, z2)) -> g(z0, z2) f[Ite][False][Ite](False, Cons(z0, z1), z2) -> z1 f[Ite][False][Ite](True, z0, Cons(z1, z2)) -> z2 f[Ite][False][Ite](False, z0, z1) -> Cons(Cons(Nil, Nil), z1) f[Ite][False][Ite](True, z0, z1) -> z0 lt0(Cons(z0, z1), Cons(z2, z3)) -> lt0(z1, z3) lt0(z0, Nil) -> False g(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) g(z0, Cons(z1, z2)) -> g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) f(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) f(z0, Cons(z1, z2)) -> f(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))) number42 -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) goal(z0, z1) -> Cons(f(z0, z1), Cons(g(z0, z1), Nil)) Rewrite Strategy: INNERMOST ---------------------------------------- (1) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (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: LT0(Cons(z0, z1), Cons(z2, z3)) -> c6(LT0(z1, z3)) LT0(z0, Nil) -> c7 G(z0, Nil) -> c8 G(z0, Cons(z1, z2)) -> c9(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) F(z0, Nil) -> c10 F(z0, Cons(z1, z2)) -> c11(F(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))), F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) F(z0, Cons(z1, z2)) -> c12(F(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))), F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) NUMBER42 -> c13 GOAL(z0, z1) -> c14(F(z0, z1)) GOAL(z0, z1) -> c15(G(z0, z1)) The (relative) TRS S consists of the following rules: G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c(G(z1, Cons(Cons(Nil, Nil), z2))) G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c1(G(z0, z2)) F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c2 F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c3 F[ITE][FALSE][ITE](False, z0, z1) -> c4 F[ITE][FALSE][ITE](True, z0, z1) -> c5 g[Ite][False][Ite](False, Cons(z0, z1), z2) -> g(z1, Cons(Cons(Nil, Nil), z2)) g[Ite][False][Ite](True, z0, Cons(z1, z2)) -> g(z0, z2) f[Ite][False][Ite](False, Cons(z0, z1), z2) -> z1 f[Ite][False][Ite](True, z0, Cons(z1, z2)) -> z2 f[Ite][False][Ite](False, z0, z1) -> Cons(Cons(Nil, Nil), z1) f[Ite][False][Ite](True, z0, z1) -> z0 lt0(Cons(z0, z1), Cons(z2, z3)) -> lt0(z1, z3) lt0(z0, Nil) -> False g(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) g(z0, Cons(z1, z2)) -> g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) f(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) f(z0, Cons(z1, z2)) -> f(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))) number42 -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) goal(z0, z1) -> Cons(f(z0, z1), Cons(g(z0, z1), Nil)) Rewrite Strategy: INNERMOST ---------------------------------------- (3) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (4) Obligation: Innermost TRS: Rules: LT0(Cons(z0, z1), Cons(z2, z3)) -> c6(LT0(z1, z3)) LT0(z0, Nil) -> c7 G(z0, Nil) -> c8 G(z0, Cons(z1, z2)) -> c9(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) F(z0, Nil) -> c10 F(z0, Cons(z1, z2)) -> c11(F(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))), F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) F(z0, Cons(z1, z2)) -> c12(F(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))), F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) NUMBER42 -> c13 GOAL(z0, z1) -> c14(F(z0, z1)) GOAL(z0, z1) -> c15(G(z0, z1)) G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c(G(z1, Cons(Cons(Nil, Nil), z2))) G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c1(G(z0, z2)) F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c2 F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c3 F[ITE][FALSE][ITE](False, z0, z1) -> c4 F[ITE][FALSE][ITE](True, z0, z1) -> c5 g[Ite][False][Ite](False, Cons(z0, z1), z2) -> g(z1, Cons(Cons(Nil, Nil), z2)) g[Ite][False][Ite](True, z0, Cons(z1, z2)) -> g(z0, z2) f[Ite][False][Ite](False, Cons(z0, z1), z2) -> z1 f[Ite][False][Ite](True, z0, Cons(z1, z2)) -> z2 f[Ite][False][Ite](False, z0, z1) -> Cons(Cons(Nil, Nil), z1) f[Ite][False][Ite](True, z0, z1) -> z0 lt0(Cons(z0, z1), Cons(z2, z3)) -> lt0(z1, z3) lt0(z0, Nil) -> False g(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) g(z0, Cons(z1, z2)) -> g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) f(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) f(z0, Cons(z1, z2)) -> f(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))) number42 -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) goal(z0, z1) -> Cons(f(z0, z1), Cons(g(z0, z1), Nil)) Types: LT0 :: Cons:Nil -> Cons:Nil -> c6:c7 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c6 :: c6:c7 -> c6:c7 Nil :: Cons:Nil c7 :: c6:c7 G :: Cons:Nil -> Cons:Nil -> c8:c9 c8 :: c8:c9 c9 :: c:c1 -> c6:c7 -> c8:c9 G[ITE][FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c:c1 lt0 :: Cons:Nil -> Cons:Nil -> False:True F :: Cons:Nil -> Cons:Nil -> c10:c11:c12 c10 :: c10:c11:c12 c11 :: c10:c11:c12 -> c2:c3:c4:c5 -> c6:c7 -> c10:c11:c12 f[Ite][False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil F[ITE][FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c2:c3:c4:c5 c12 :: c10:c11:c12 -> c2:c3:c4:c5 -> c6:c7 -> c10:c11:c12 NUMBER42 :: c13 c13 :: c13 GOAL :: Cons:Nil -> Cons:Nil -> c14:c15 c14 :: c10:c11:c12 -> c14:c15 c15 :: c8:c9 -> c14:c15 False :: False:True c :: c8:c9 -> c:c1 True :: False:True c1 :: c8:c9 -> c:c1 c2 :: c2:c3:c4:c5 c3 :: c2:c3:c4:c5 c4 :: c2:c3:c4:c5 c5 :: c2:c3:c4:c5 g[Ite][False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil g :: Cons:Nil -> Cons:Nil -> Cons:Nil f :: Cons:Nil -> Cons:Nil -> Cons:Nil number42 :: Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil hole_c6:c71_16 :: c6:c7 hole_Cons:Nil2_16 :: Cons:Nil hole_c8:c93_16 :: c8:c9 hole_c:c14_16 :: c:c1 hole_False:True5_16 :: False:True hole_c10:c11:c126_16 :: c10:c11:c12 hole_c2:c3:c4:c57_16 :: c2:c3:c4:c5 hole_c138_16 :: c13 hole_c14:c159_16 :: c14:c15 gen_c6:c710_16 :: Nat -> c6:c7 gen_Cons:Nil11_16 :: Nat -> Cons:Nil gen_c10:c11:c1212_16 :: Nat -> c10:c11:c12 ---------------------------------------- (5) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: LT0, G, lt0, F, g, f They will be analysed ascendingly in the following order: LT0 < G LT0 < F lt0 < G lt0 < F lt0 < g lt0 < f ---------------------------------------- (6) Obligation: Innermost TRS: Rules: LT0(Cons(z0, z1), Cons(z2, z3)) -> c6(LT0(z1, z3)) LT0(z0, Nil) -> c7 G(z0, Nil) -> c8 G(z0, Cons(z1, z2)) -> c9(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) F(z0, Nil) -> c10 F(z0, Cons(z1, z2)) -> c11(F(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))), F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) F(z0, Cons(z1, z2)) -> c12(F(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))), F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) NUMBER42 -> c13 GOAL(z0, z1) -> c14(F(z0, z1)) GOAL(z0, z1) -> c15(G(z0, z1)) G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c(G(z1, Cons(Cons(Nil, Nil), z2))) G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c1(G(z0, z2)) F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c2 F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c3 F[ITE][FALSE][ITE](False, z0, z1) -> c4 F[ITE][FALSE][ITE](True, z0, z1) -> c5 g[Ite][False][Ite](False, Cons(z0, z1), z2) -> g(z1, Cons(Cons(Nil, Nil), z2)) g[Ite][False][Ite](True, z0, Cons(z1, z2)) -> g(z0, z2) f[Ite][False][Ite](False, Cons(z0, z1), z2) -> z1 f[Ite][False][Ite](True, z0, Cons(z1, z2)) -> z2 f[Ite][False][Ite](False, z0, z1) -> Cons(Cons(Nil, Nil), z1) f[Ite][False][Ite](True, z0, z1) -> z0 lt0(Cons(z0, z1), Cons(z2, z3)) -> lt0(z1, z3) lt0(z0, Nil) -> False g(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) g(z0, Cons(z1, z2)) -> g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) f(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) f(z0, Cons(z1, z2)) -> f(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))) number42 -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) goal(z0, z1) -> Cons(f(z0, z1), Cons(g(z0, z1), Nil)) Types: LT0 :: Cons:Nil -> Cons:Nil -> c6:c7 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c6 :: c6:c7 -> c6:c7 Nil :: Cons:Nil c7 :: c6:c7 G :: Cons:Nil -> Cons:Nil -> c8:c9 c8 :: c8:c9 c9 :: c:c1 -> c6:c7 -> c8:c9 G[ITE][FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c:c1 lt0 :: Cons:Nil -> Cons:Nil -> False:True F :: Cons:Nil -> Cons:Nil -> c10:c11:c12 c10 :: c10:c11:c12 c11 :: c10:c11:c12 -> c2:c3:c4:c5 -> c6:c7 -> c10:c11:c12 f[Ite][False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil F[ITE][FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c2:c3:c4:c5 c12 :: c10:c11:c12 -> c2:c3:c4:c5 -> c6:c7 -> c10:c11:c12 NUMBER42 :: c13 c13 :: c13 GOAL :: Cons:Nil -> Cons:Nil -> c14:c15 c14 :: c10:c11:c12 -> c14:c15 c15 :: c8:c9 -> c14:c15 False :: False:True c :: c8:c9 -> c:c1 True :: False:True c1 :: c8:c9 -> c:c1 c2 :: c2:c3:c4:c5 c3 :: c2:c3:c4:c5 c4 :: c2:c3:c4:c5 c5 :: c2:c3:c4:c5 g[Ite][False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil g :: Cons:Nil -> Cons:Nil -> Cons:Nil f :: Cons:Nil -> Cons:Nil -> Cons:Nil number42 :: Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil hole_c6:c71_16 :: c6:c7 hole_Cons:Nil2_16 :: Cons:Nil hole_c8:c93_16 :: c8:c9 hole_c:c14_16 :: c:c1 hole_False:True5_16 :: False:True hole_c10:c11:c126_16 :: c10:c11:c12 hole_c2:c3:c4:c57_16 :: c2:c3:c4:c5 hole_c138_16 :: c13 hole_c14:c159_16 :: c14:c15 gen_c6:c710_16 :: Nat -> c6:c7 gen_Cons:Nil11_16 :: Nat -> Cons:Nil gen_c10:c11:c1212_16 :: Nat -> c10:c11:c12 Generator Equations: gen_c6:c710_16(0) <=> c7 gen_c6:c710_16(+(x, 1)) <=> c6(gen_c6:c710_16(x)) gen_Cons:Nil11_16(0) <=> Nil gen_Cons:Nil11_16(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil11_16(x)) gen_c10:c11:c1212_16(0) <=> c10 gen_c10:c11:c1212_16(+(x, 1)) <=> c11(gen_c10:c11:c1212_16(x), c2, c7) The following defined symbols remain to be analysed: LT0, G, lt0, F, g, f They will be analysed ascendingly in the following order: LT0 < G LT0 < F lt0 < G lt0 < F lt0 < g lt0 < f ---------------------------------------- (7) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: LT0(gen_Cons:Nil11_16(n14_16), gen_Cons:Nil11_16(n14_16)) -> gen_c6:c710_16(n14_16), rt in Omega(1 + n14_16) Induction Base: LT0(gen_Cons:Nil11_16(0), gen_Cons:Nil11_16(0)) ->_R^Omega(1) c7 Induction Step: LT0(gen_Cons:Nil11_16(+(n14_16, 1)), gen_Cons:Nil11_16(+(n14_16, 1))) ->_R^Omega(1) c6(LT0(gen_Cons:Nil11_16(n14_16), gen_Cons:Nil11_16(n14_16))) ->_IH c6(gen_c6:c710_16(c15_16)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (8) Complex Obligation (BEST) ---------------------------------------- (9) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: LT0(Cons(z0, z1), Cons(z2, z3)) -> c6(LT0(z1, z3)) LT0(z0, Nil) -> c7 G(z0, Nil) -> c8 G(z0, Cons(z1, z2)) -> c9(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) F(z0, Nil) -> c10 F(z0, Cons(z1, z2)) -> c11(F(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))), F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) F(z0, Cons(z1, z2)) -> c12(F(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))), F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) NUMBER42 -> c13 GOAL(z0, z1) -> c14(F(z0, z1)) GOAL(z0, z1) -> c15(G(z0, z1)) G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c(G(z1, Cons(Cons(Nil, Nil), z2))) G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c1(G(z0, z2)) F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c2 F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c3 F[ITE][FALSE][ITE](False, z0, z1) -> c4 F[ITE][FALSE][ITE](True, z0, z1) -> c5 g[Ite][False][Ite](False, Cons(z0, z1), z2) -> g(z1, Cons(Cons(Nil, Nil), z2)) g[Ite][False][Ite](True, z0, Cons(z1, z2)) -> g(z0, z2) f[Ite][False][Ite](False, Cons(z0, z1), z2) -> z1 f[Ite][False][Ite](True, z0, Cons(z1, z2)) -> z2 f[Ite][False][Ite](False, z0, z1) -> Cons(Cons(Nil, Nil), z1) f[Ite][False][Ite](True, z0, z1) -> z0 lt0(Cons(z0, z1), Cons(z2, z3)) -> lt0(z1, z3) lt0(z0, Nil) -> False g(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) g(z0, Cons(z1, z2)) -> g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) f(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) f(z0, Cons(z1, z2)) -> f(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))) number42 -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) goal(z0, z1) -> Cons(f(z0, z1), Cons(g(z0, z1), Nil)) Types: LT0 :: Cons:Nil -> Cons:Nil -> c6:c7 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c6 :: c6:c7 -> c6:c7 Nil :: Cons:Nil c7 :: c6:c7 G :: Cons:Nil -> Cons:Nil -> c8:c9 c8 :: c8:c9 c9 :: c:c1 -> c6:c7 -> c8:c9 G[ITE][FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c:c1 lt0 :: Cons:Nil -> Cons:Nil -> False:True F :: Cons:Nil -> Cons:Nil -> c10:c11:c12 c10 :: c10:c11:c12 c11 :: c10:c11:c12 -> c2:c3:c4:c5 -> c6:c7 -> c10:c11:c12 f[Ite][False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil F[ITE][FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c2:c3:c4:c5 c12 :: c10:c11:c12 -> c2:c3:c4:c5 -> c6:c7 -> c10:c11:c12 NUMBER42 :: c13 c13 :: c13 GOAL :: Cons:Nil -> Cons:Nil -> c14:c15 c14 :: c10:c11:c12 -> c14:c15 c15 :: c8:c9 -> c14:c15 False :: False:True c :: c8:c9 -> c:c1 True :: False:True c1 :: c8:c9 -> c:c1 c2 :: c2:c3:c4:c5 c3 :: c2:c3:c4:c5 c4 :: c2:c3:c4:c5 c5 :: c2:c3:c4:c5 g[Ite][False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil g :: Cons:Nil -> Cons:Nil -> Cons:Nil f :: Cons:Nil -> Cons:Nil -> Cons:Nil number42 :: Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil hole_c6:c71_16 :: c6:c7 hole_Cons:Nil2_16 :: Cons:Nil hole_c8:c93_16 :: c8:c9 hole_c:c14_16 :: c:c1 hole_False:True5_16 :: False:True hole_c10:c11:c126_16 :: c10:c11:c12 hole_c2:c3:c4:c57_16 :: c2:c3:c4:c5 hole_c138_16 :: c13 hole_c14:c159_16 :: c14:c15 gen_c6:c710_16 :: Nat -> c6:c7 gen_Cons:Nil11_16 :: Nat -> Cons:Nil gen_c10:c11:c1212_16 :: Nat -> c10:c11:c12 Generator Equations: gen_c6:c710_16(0) <=> c7 gen_c6:c710_16(+(x, 1)) <=> c6(gen_c6:c710_16(x)) gen_Cons:Nil11_16(0) <=> Nil gen_Cons:Nil11_16(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil11_16(x)) gen_c10:c11:c1212_16(0) <=> c10 gen_c10:c11:c1212_16(+(x, 1)) <=> c11(gen_c10:c11:c1212_16(x), c2, c7) The following defined symbols remain to be analysed: LT0, G, lt0, F, g, f They will be analysed ascendingly in the following order: LT0 < G LT0 < F lt0 < G lt0 < F lt0 < g lt0 < f ---------------------------------------- (10) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (11) BOUNDS(n^1, INF) ---------------------------------------- (12) Obligation: Innermost TRS: Rules: LT0(Cons(z0, z1), Cons(z2, z3)) -> c6(LT0(z1, z3)) LT0(z0, Nil) -> c7 G(z0, Nil) -> c8 G(z0, Cons(z1, z2)) -> c9(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) F(z0, Nil) -> c10 F(z0, Cons(z1, z2)) -> c11(F(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))), F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) F(z0, Cons(z1, z2)) -> c12(F(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))), F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) NUMBER42 -> c13 GOAL(z0, z1) -> c14(F(z0, z1)) GOAL(z0, z1) -> c15(G(z0, z1)) G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c(G(z1, Cons(Cons(Nil, Nil), z2))) G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c1(G(z0, z2)) F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c2 F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c3 F[ITE][FALSE][ITE](False, z0, z1) -> c4 F[ITE][FALSE][ITE](True, z0, z1) -> c5 g[Ite][False][Ite](False, Cons(z0, z1), z2) -> g(z1, Cons(Cons(Nil, Nil), z2)) g[Ite][False][Ite](True, z0, Cons(z1, z2)) -> g(z0, z2) f[Ite][False][Ite](False, Cons(z0, z1), z2) -> z1 f[Ite][False][Ite](True, z0, Cons(z1, z2)) -> z2 f[Ite][False][Ite](False, z0, z1) -> Cons(Cons(Nil, Nil), z1) f[Ite][False][Ite](True, z0, z1) -> z0 lt0(Cons(z0, z1), Cons(z2, z3)) -> lt0(z1, z3) lt0(z0, Nil) -> False g(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) g(z0, Cons(z1, z2)) -> g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) f(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) f(z0, Cons(z1, z2)) -> f(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))) number42 -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) goal(z0, z1) -> Cons(f(z0, z1), Cons(g(z0, z1), Nil)) Types: LT0 :: Cons:Nil -> Cons:Nil -> c6:c7 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c6 :: c6:c7 -> c6:c7 Nil :: Cons:Nil c7 :: c6:c7 G :: Cons:Nil -> Cons:Nil -> c8:c9 c8 :: c8:c9 c9 :: c:c1 -> c6:c7 -> c8:c9 G[ITE][FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c:c1 lt0 :: Cons:Nil -> Cons:Nil -> False:True F :: Cons:Nil -> Cons:Nil -> c10:c11:c12 c10 :: c10:c11:c12 c11 :: c10:c11:c12 -> c2:c3:c4:c5 -> c6:c7 -> c10:c11:c12 f[Ite][False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil F[ITE][FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c2:c3:c4:c5 c12 :: c10:c11:c12 -> c2:c3:c4:c5 -> c6:c7 -> c10:c11:c12 NUMBER42 :: c13 c13 :: c13 GOAL :: Cons:Nil -> Cons:Nil -> c14:c15 c14 :: c10:c11:c12 -> c14:c15 c15 :: c8:c9 -> c14:c15 False :: False:True c :: c8:c9 -> c:c1 True :: False:True c1 :: c8:c9 -> c:c1 c2 :: c2:c3:c4:c5 c3 :: c2:c3:c4:c5 c4 :: c2:c3:c4:c5 c5 :: c2:c3:c4:c5 g[Ite][False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil g :: Cons:Nil -> Cons:Nil -> Cons:Nil f :: Cons:Nil -> Cons:Nil -> Cons:Nil number42 :: Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil hole_c6:c71_16 :: c6:c7 hole_Cons:Nil2_16 :: Cons:Nil hole_c8:c93_16 :: c8:c9 hole_c:c14_16 :: c:c1 hole_False:True5_16 :: False:True hole_c10:c11:c126_16 :: c10:c11:c12 hole_c2:c3:c4:c57_16 :: c2:c3:c4:c5 hole_c138_16 :: c13 hole_c14:c159_16 :: c14:c15 gen_c6:c710_16 :: Nat -> c6:c7 gen_Cons:Nil11_16 :: Nat -> Cons:Nil gen_c10:c11:c1212_16 :: Nat -> c10:c11:c12 Lemmas: LT0(gen_Cons:Nil11_16(n14_16), gen_Cons:Nil11_16(n14_16)) -> gen_c6:c710_16(n14_16), rt in Omega(1 + n14_16) Generator Equations: gen_c6:c710_16(0) <=> c7 gen_c6:c710_16(+(x, 1)) <=> c6(gen_c6:c710_16(x)) gen_Cons:Nil11_16(0) <=> Nil gen_Cons:Nil11_16(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil11_16(x)) gen_c10:c11:c1212_16(0) <=> c10 gen_c10:c11:c1212_16(+(x, 1)) <=> c11(gen_c10:c11:c1212_16(x), c2, c7) The following defined symbols remain to be analysed: lt0, G, F, g, f They will be analysed ascendingly in the following order: lt0 < G lt0 < F lt0 < g lt0 < f ---------------------------------------- (13) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: lt0(gen_Cons:Nil11_16(n516_16), gen_Cons:Nil11_16(n516_16)) -> False, rt in Omega(0) Induction Base: lt0(gen_Cons:Nil11_16(0), gen_Cons:Nil11_16(0)) ->_R^Omega(0) False Induction Step: lt0(gen_Cons:Nil11_16(+(n516_16, 1)), gen_Cons:Nil11_16(+(n516_16, 1))) ->_R^Omega(0) lt0(gen_Cons:Nil11_16(n516_16), gen_Cons:Nil11_16(n516_16)) ->_IH False We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (14) Obligation: Innermost TRS: Rules: LT0(Cons(z0, z1), Cons(z2, z3)) -> c6(LT0(z1, z3)) LT0(z0, Nil) -> c7 G(z0, Nil) -> c8 G(z0, Cons(z1, z2)) -> c9(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) F(z0, Nil) -> c10 F(z0, Cons(z1, z2)) -> c11(F(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))), F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) F(z0, Cons(z1, z2)) -> c12(F(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))), F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil))) NUMBER42 -> c13 GOAL(z0, z1) -> c14(F(z0, z1)) GOAL(z0, z1) -> c15(G(z0, z1)) G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c(G(z1, Cons(Cons(Nil, Nil), z2))) G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c1(G(z0, z2)) F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) -> c2 F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c3 F[ITE][FALSE][ITE](False, z0, z1) -> c4 F[ITE][FALSE][ITE](True, z0, z1) -> c5 g[Ite][False][Ite](False, Cons(z0, z1), z2) -> g(z1, Cons(Cons(Nil, Nil), z2)) g[Ite][False][Ite](True, z0, Cons(z1, z2)) -> g(z0, z2) f[Ite][False][Ite](False, Cons(z0, z1), z2) -> z1 f[Ite][False][Ite](True, z0, Cons(z1, z2)) -> z2 f[Ite][False][Ite](False, z0, z1) -> Cons(Cons(Nil, Nil), z1) f[Ite][False][Ite](True, z0, z1) -> z0 lt0(Cons(z0, z1), Cons(z2, z3)) -> lt0(z1, z3) lt0(z0, Nil) -> False g(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) g(z0, Cons(z1, z2)) -> g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)) f(z0, Nil) -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) f(z0, Cons(z1, z2)) -> f(f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))) number42 -> Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil)))))))))))))))))))))))))))))))))))))))))) goal(z0, z1) -> Cons(f(z0, z1), Cons(g(z0, z1), Nil)) Types: LT0 :: Cons:Nil -> Cons:Nil -> c6:c7 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c6 :: c6:c7 -> c6:c7 Nil :: Cons:Nil c7 :: c6:c7 G :: Cons:Nil -> Cons:Nil -> c8:c9 c8 :: c8:c9 c9 :: c:c1 -> c6:c7 -> c8:c9 G[ITE][FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c:c1 lt0 :: Cons:Nil -> Cons:Nil -> False:True F :: Cons:Nil -> Cons:Nil -> c10:c11:c12 c10 :: c10:c11:c12 c11 :: c10:c11:c12 -> c2:c3:c4:c5 -> c6:c7 -> c10:c11:c12 f[Ite][False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil F[ITE][FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c2:c3:c4:c5 c12 :: c10:c11:c12 -> c2:c3:c4:c5 -> c6:c7 -> c10:c11:c12 NUMBER42 :: c13 c13 :: c13 GOAL :: Cons:Nil -> Cons:Nil -> c14:c15 c14 :: c10:c11:c12 -> c14:c15 c15 :: c8:c9 -> c14:c15 False :: False:True c :: c8:c9 -> c:c1 True :: False:True c1 :: c8:c9 -> c:c1 c2 :: c2:c3:c4:c5 c3 :: c2:c3:c4:c5 c4 :: c2:c3:c4:c5 c5 :: c2:c3:c4:c5 g[Ite][False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil g :: Cons:Nil -> Cons:Nil -> Cons:Nil f :: Cons:Nil -> Cons:Nil -> Cons:Nil number42 :: Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil hole_c6:c71_16 :: c6:c7 hole_Cons:Nil2_16 :: Cons:Nil hole_c8:c93_16 :: c8:c9 hole_c:c14_16 :: c:c1 hole_False:True5_16 :: False:True hole_c10:c11:c126_16 :: c10:c11:c12 hole_c2:c3:c4:c57_16 :: c2:c3:c4:c5 hole_c138_16 :: c13 hole_c14:c159_16 :: c14:c15 gen_c6:c710_16 :: Nat -> c6:c7 gen_Cons:Nil11_16 :: Nat -> Cons:Nil gen_c10:c11:c1212_16 :: Nat -> c10:c11:c12 Lemmas: LT0(gen_Cons:Nil11_16(n14_16), gen_Cons:Nil11_16(n14_16)) -> gen_c6:c710_16(n14_16), rt in Omega(1 + n14_16) lt0(gen_Cons:Nil11_16(n516_16), gen_Cons:Nil11_16(n516_16)) -> False, rt in Omega(0) Generator Equations: gen_c6:c710_16(0) <=> c7 gen_c6:c710_16(+(x, 1)) <=> c6(gen_c6:c710_16(x)) gen_Cons:Nil11_16(0) <=> Nil gen_Cons:Nil11_16(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil11_16(x)) gen_c10:c11:c1212_16(0) <=> c10 gen_c10:c11:c1212_16(+(x, 1)) <=> c11(gen_c10:c11:c1212_16(x), c2, c7) The following defined symbols remain to be analysed: G, F, g, f