WORST_CASE(Omega(n^2),O(n^3)) proof of input_tHBTvHkrTG.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^2, n^3). (0) CpxTRS (1) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms] (2) CpxWeightedTrs (3) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CpxTypedWeightedTrs (5) CompletionProof [UPPER BOUND(ID), 3 ms] (6) CpxTypedWeightedCompleteTrs (7) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxTypedWeightedCompleteTrs (9) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (10) CpxRNTS (11) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CpxRNTS (13) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CpxRNTS (15) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (16) CpxRNTS (17) IntTrsBoundProof [UPPER BOUND(ID), 368 ms] (18) CpxRNTS (19) IntTrsBoundProof [UPPER BOUND(ID), 59 ms] (20) CpxRNTS (21) ResultPropagationProof [UPPER BOUND(ID), 1 ms] (22) CpxRNTS (23) IntTrsBoundProof [UPPER BOUND(ID), 293 ms] (24) CpxRNTS (25) IntTrsBoundProof [UPPER BOUND(ID), 186 ms] (26) CpxRNTS (27) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (28) CpxRNTS (29) IntTrsBoundProof [UPPER BOUND(ID), 720 ms] (30) CpxRNTS (31) IntTrsBoundProof [UPPER BOUND(ID), 324 ms] (32) CpxRNTS (33) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (34) CpxRNTS (35) IntTrsBoundProof [UPPER BOUND(ID), 1383 ms] (36) CpxRNTS (37) IntTrsBoundProof [UPPER BOUND(ID), 553 ms] (38) CpxRNTS (39) ResultPropagationProof [UPPER BOUND(ID), 0 ms] (40) CpxRNTS (41) IntTrsBoundProof [UPPER BOUND(ID), 536 ms] (42) CpxRNTS (43) IntTrsBoundProof [UPPER BOUND(ID), 126 ms] (44) CpxRNTS (45) FinalProof [FINISHED, 0 ms] (46) BOUNDS(1, n^3) (47) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms] (48) CdtProblem (49) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (50) CpxRelTRS (51) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (52) CpxRelTRS (53) TypeInferenceProof [BOTH BOUNDS(ID, ID), 4 ms] (54) typed CpxTrs (55) OrderProof [LOWER BOUND(ID), 0 ms] (56) typed CpxTrs (57) RewriteLemmaProof [LOWER BOUND(ID), 416 ms] (58) BEST (59) proven lower bound (60) LowerBoundPropagationProof [FINISHED, 0 ms] (61) BOUNDS(n^1, INF) (62) typed CpxTrs (63) RewriteLemmaProof [LOWER BOUND(ID), 127 ms] (64) typed CpxTrs (65) RewriteLemmaProof [LOWER BOUND(ID), 38 ms] (66) typed CpxTrs (67) RewriteLemmaProof [LOWER BOUND(ID), 674 ms] (68) typed CpxTrs (69) RewriteLemmaProof [LOWER BOUND(ID), 58 ms] (70) typed CpxTrs (71) RewriteLemmaProof [LOWER BOUND(ID), 72 ms] (72) typed CpxTrs (73) RewriteLemmaProof [LOWER BOUND(ID), 18.4 s] (74) BEST (75) proven lower bound (76) LowerBoundPropagationProof [FINISHED, 0 ms] (77) BOUNDS(n^2, INF) (78) typed CpxTrs (79) RewriteLemmaProof [LOWER BOUND(ID), 1164 ms] (80) BOUNDS(1, INF) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^2, n^3). The TRS R consists of the following rules: eq(0, 0) -> true eq(0, s(m)) -> false eq(s(n), 0) -> false eq(s(n), s(m)) -> eq(n, m) le(0, m) -> true le(s(n), 0) -> false le(s(n), s(m)) -> le(n, m) min(cons(0, nil)) -> 0 min(cons(s(n), nil)) -> s(n) min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x))) if_min(true, cons(n, cons(m, x))) -> min(cons(n, x)) if_min(false, cons(n, cons(m, x))) -> min(cons(m, x)) replace(n, m, nil) -> nil replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)) if_replace(true, n, m, cons(k, x)) -> cons(m, x) if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x)) sort(nil) -> nil sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) RelTrsToWeightedTrsProof (UPPER BOUND(ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^3). The TRS R consists of the following rules: eq(0, 0) -> true [1] eq(0, s(m)) -> false [1] eq(s(n), 0) -> false [1] eq(s(n), s(m)) -> eq(n, m) [1] le(0, m) -> true [1] le(s(n), 0) -> false [1] le(s(n), s(m)) -> le(n, m) [1] min(cons(0, nil)) -> 0 [1] min(cons(s(n), nil)) -> s(n) [1] min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x))) [1] if_min(true, cons(n, cons(m, x))) -> min(cons(n, x)) [1] if_min(false, cons(n, cons(m, x))) -> min(cons(m, x)) [1] replace(n, m, nil) -> nil [1] replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)) [1] if_replace(true, n, m, cons(k, x)) -> cons(m, x) [1] if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x)) [1] sort(nil) -> nil [1] sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))) [1] Rewrite Strategy: INNERMOST ---------------------------------------- (3) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (4) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: eq(0, 0) -> true [1] eq(0, s(m)) -> false [1] eq(s(n), 0) -> false [1] eq(s(n), s(m)) -> eq(n, m) [1] le(0, m) -> true [1] le(s(n), 0) -> false [1] le(s(n), s(m)) -> le(n, m) [1] min(cons(0, nil)) -> 0 [1] min(cons(s(n), nil)) -> s(n) [1] min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x))) [1] if_min(true, cons(n, cons(m, x))) -> min(cons(n, x)) [1] if_min(false, cons(n, cons(m, x))) -> min(cons(m, x)) [1] replace(n, m, nil) -> nil [1] replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)) [1] if_replace(true, n, m, cons(k, x)) -> cons(m, x) [1] if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x)) [1] sort(nil) -> nil [1] sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))) [1] The TRS has the following type information: eq :: 0:s -> 0:s -> true:false 0 :: 0:s true :: true:false s :: 0:s -> 0:s false :: true:false le :: 0:s -> 0:s -> true:false min :: nil:cons -> 0:s cons :: 0:s -> nil:cons -> nil:cons nil :: nil:cons if_min :: true:false -> nil:cons -> 0:s replace :: 0:s -> 0:s -> nil:cons -> nil:cons if_replace :: true:false -> 0:s -> 0:s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons Rewrite Strategy: INNERMOST ---------------------------------------- (5) CompletionProof (UPPER BOUND(ID)) The transformation into a RNTS is sound, since: (a) The obligation is a constructor system where every type has a constant constructor, (b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols: sort_1 (c) The following functions are completely defined: replace_3 min_1 eq_2 le_2 if_replace_4 if_min_2 Due to the following rules being added: min(v0) -> 0 [0] if_replace(v0, v1, v2, v3) -> nil [0] if_min(v0, v1) -> 0 [0] And the following fresh constants: none ---------------------------------------- (6) Obligation: Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: eq(0, 0) -> true [1] eq(0, s(m)) -> false [1] eq(s(n), 0) -> false [1] eq(s(n), s(m)) -> eq(n, m) [1] le(0, m) -> true [1] le(s(n), 0) -> false [1] le(s(n), s(m)) -> le(n, m) [1] min(cons(0, nil)) -> 0 [1] min(cons(s(n), nil)) -> s(n) [1] min(cons(n, cons(m, x))) -> if_min(le(n, m), cons(n, cons(m, x))) [1] if_min(true, cons(n, cons(m, x))) -> min(cons(n, x)) [1] if_min(false, cons(n, cons(m, x))) -> min(cons(m, x)) [1] replace(n, m, nil) -> nil [1] replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)) [1] if_replace(true, n, m, cons(k, x)) -> cons(m, x) [1] if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x)) [1] sort(nil) -> nil [1] sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(min(cons(n, x)), n, x))) [1] min(v0) -> 0 [0] if_replace(v0, v1, v2, v3) -> nil [0] if_min(v0, v1) -> 0 [0] The TRS has the following type information: eq :: 0:s -> 0:s -> true:false 0 :: 0:s true :: true:false s :: 0:s -> 0:s false :: true:false le :: 0:s -> 0:s -> true:false min :: nil:cons -> 0:s cons :: 0:s -> nil:cons -> nil:cons nil :: nil:cons if_min :: true:false -> nil:cons -> 0:s replace :: 0:s -> 0:s -> nil:cons -> nil:cons if_replace :: true:false -> 0:s -> 0:s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons Rewrite Strategy: INNERMOST ---------------------------------------- (7) NarrowingProof (BOTH BOUNDS(ID, ID)) Narrowed the inner basic terms of all right-hand sides by a single narrowing step. ---------------------------------------- (8) Obligation: Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: eq(0, 0) -> true [1] eq(0, s(m)) -> false [1] eq(s(n), 0) -> false [1] eq(s(n), s(m)) -> eq(n, m) [1] le(0, m) -> true [1] le(s(n), 0) -> false [1] le(s(n), s(m)) -> le(n, m) [1] min(cons(0, nil)) -> 0 [1] min(cons(s(n), nil)) -> s(n) [1] min(cons(0, cons(m, x))) -> if_min(true, cons(0, cons(m, x))) [2] min(cons(s(n'), cons(0, x))) -> if_min(false, cons(s(n'), cons(0, x))) [2] min(cons(s(n''), cons(s(m'), x))) -> if_min(le(n'', m'), cons(s(n''), cons(s(m'), x))) [2] if_min(true, cons(n, cons(m, x))) -> min(cons(n, x)) [1] if_min(false, cons(n, cons(m, x))) -> min(cons(m, x)) [1] replace(n, m, nil) -> nil [1] replace(0, m, cons(0, x)) -> if_replace(true, 0, m, cons(0, x)) [2] replace(0, m, cons(s(m''), x)) -> if_replace(false, 0, m, cons(s(m''), x)) [2] replace(s(n1), m, cons(0, x)) -> if_replace(false, s(n1), m, cons(0, x)) [2] replace(s(n2), m, cons(s(m1), x)) -> if_replace(eq(n2, m1), s(n2), m, cons(s(m1), x)) [2] if_replace(true, n, m, cons(k, x)) -> cons(m, x) [1] if_replace(false, n, m, cons(k, x)) -> cons(k, replace(n, m, x)) [1] sort(nil) -> nil [1] sort(cons(0, nil)) -> cons(min(cons(0, nil)), sort(replace(0, 0, nil))) [2] sort(cons(s(n3), nil)) -> cons(min(cons(s(n3), nil)), sort(replace(s(n3), s(n3), nil))) [2] sort(cons(n, cons(m2, x'))) -> cons(min(cons(n, cons(m2, x'))), sort(replace(if_min(le(n, m2), cons(n, cons(m2, x'))), n, cons(m2, x')))) [2] sort(cons(n, x)) -> cons(min(cons(n, x)), sort(replace(0, n, x))) [1] min(v0) -> 0 [0] if_replace(v0, v1, v2, v3) -> nil [0] if_min(v0, v1) -> 0 [0] The TRS has the following type information: eq :: 0:s -> 0:s -> true:false 0 :: 0:s true :: true:false s :: 0:s -> 0:s false :: true:false le :: 0:s -> 0:s -> true:false min :: nil:cons -> 0:s cons :: 0:s -> nil:cons -> nil:cons nil :: nil:cons if_min :: true:false -> nil:cons -> 0:s replace :: 0:s -> 0:s -> nil:cons -> nil:cons if_replace :: true:false -> 0:s -> 0:s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons Rewrite Strategy: INNERMOST ---------------------------------------- (9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: 0 => 0 true => 1 false => 0 nil => 0 ---------------------------------------- (10) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 1 }-> eq(n, m) :|: n >= 0, z' = 1 + m, z = 1 + n, m >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' = 1 + m, m >= 0 eq(z, z') -{ 1 }-> 0 :|: n >= 0, z = 1 + n, z' = 0 if_min(z, z') -{ 1 }-> min(1 + m + x) :|: n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 1 }-> min(1 + n + x) :|: n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + k + replace(n, m, x) :|: n >= 0, x >= 0, z1 = 1 + k + x, z' = n, k >= 0, z = 0, z'' = m, m >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + m + x :|: n >= 0, z = 1, x >= 0, z1 = 1 + k + x, z' = n, k >= 0, z'' = m, m >= 0 le(z, z') -{ 1 }-> le(n, m) :|: n >= 0, z' = 1 + m, z = 1 + n, m >= 0 le(z, z') -{ 1 }-> 1 :|: z' = m, z = 0, m >= 0 le(z, z') -{ 1 }-> 0 :|: n >= 0, z = 1 + n, z' = 0 min(z) -{ 2 }-> if_min(le(n'', m'), 1 + (1 + n'') + (1 + (1 + m') + x)) :|: x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 2 }-> if_min(1, 1 + 0 + (1 + m + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 2 }-> if_min(0, 1 + (1 + n') + (1 + 0 + x)) :|: x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 min(z) -{ 1 }-> 1 + n :|: z = 1 + (1 + n) + 0, n >= 0 replace(z, z', z'') -{ 2 }-> if_replace(eq(n2, m1), 1 + n2, m, 1 + (1 + m1) + x) :|: z = 1 + n2, z' = m, z'' = 1 + (1 + m1) + x, x >= 0, n2 >= 0, m1 >= 0, m >= 0 replace(z, z', z'') -{ 2 }-> if_replace(1, 0, m, 1 + 0 + x) :|: z' = m, x >= 0, z = 0, z'' = 1 + 0 + x, m >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 0, m, 1 + (1 + m'') + x) :|: z' = m, m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, m >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 1 + n1, m, 1 + 0 + x) :|: z = 1 + n1, z' = m, x >= 0, n1 >= 0, z'' = 1 + 0 + x, m >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, n >= 0, z = n, z' = m, m >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 1 }-> 1 + min(1 + n + x) + sort(replace(0, n, x)) :|: n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 2 }-> 1 + min(1 + n + (1 + m2 + x')) + sort(replace(if_min(le(n, m2), 1 + n + (1 + m2 + x')), n, 1 + m2 + x')) :|: n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 2 }-> 1 + min(1 + 0 + 0) + sort(replace(0, 0, 0)) :|: z = 1 + 0 + 0 sort(z) -{ 2 }-> 1 + min(1 + (1 + n3) + 0) + sort(replace(1 + n3, 1 + n3, 0)) :|: z = 1 + (1 + n3) + 0, n3 >= 0 ---------------------------------------- (11) SimplificationProof (BOTH BOUNDS(ID, ID)) Simplified the RNTS by moving equalities from the constraints into the right-hand sides. ---------------------------------------- (12) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 1 }-> eq(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 1 }-> min(1 + m + x) :|: n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 1 }-> min(1 + n + x) :|: n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + k + replace(z', z'', x) :|: z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 1 }-> le(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 2 }-> if_min(le(n'', m'), 1 + (1 + n'') + (1 + (1 + m') + x)) :|: x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 2 }-> if_min(1, 1 + 0 + (1 + m + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 2 }-> if_min(0, 1 + (1 + n') + (1 + 0 + x)) :|: x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 2 }-> if_replace(eq(z - 1, m1), 1 + (z - 1), z', 1 + (1 + m1) + x) :|: z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 0, z', 1 + (1 + m'') + x) :|: m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 1 }-> 1 + min(1 + n + x) + sort(replace(0, n, x)) :|: n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 2 }-> 1 + min(1 + n + (1 + m2 + x')) + sort(replace(if_min(le(n, m2), 1 + n + (1 + m2 + x')), n, 1 + m2 + x')) :|: n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 2 }-> 1 + min(1 + 0 + 0) + sort(replace(0, 0, 0)) :|: z = 1 + 0 + 0 sort(z) -{ 2 }-> 1 + min(1 + (1 + (z - 2)) + 0) + sort(replace(1 + (z - 2), 1 + (z - 2), 0)) :|: z - 2 >= 0 ---------------------------------------- (13) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID)) Found the following analysis order by SCC decomposition: { le } { eq } { min, if_min } { replace, if_replace } { sort } ---------------------------------------- (14) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 1 }-> eq(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 1 }-> min(1 + m + x) :|: n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 1 }-> min(1 + n + x) :|: n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + k + replace(z', z'', x) :|: z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 1 }-> le(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 2 }-> if_min(le(n'', m'), 1 + (1 + n'') + (1 + (1 + m') + x)) :|: x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 2 }-> if_min(1, 1 + 0 + (1 + m + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 2 }-> if_min(0, 1 + (1 + n') + (1 + 0 + x)) :|: x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 2 }-> if_replace(eq(z - 1, m1), 1 + (z - 1), z', 1 + (1 + m1) + x) :|: z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 0, z', 1 + (1 + m'') + x) :|: m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 1 }-> 1 + min(1 + n + x) + sort(replace(0, n, x)) :|: n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 2 }-> 1 + min(1 + n + (1 + m2 + x')) + sort(replace(if_min(le(n, m2), 1 + n + (1 + m2 + x')), n, 1 + m2 + x')) :|: n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 2 }-> 1 + min(1 + 0 + 0) + sort(replace(0, 0, 0)) :|: z = 1 + 0 + 0 sort(z) -{ 2 }-> 1 + min(1 + (1 + (z - 2)) + 0) + sort(replace(1 + (z - 2), 1 + (z - 2), 0)) :|: z - 2 >= 0 Function symbols to be analyzed: {le}, {eq}, {min,if_min}, {replace,if_replace}, {sort} ---------------------------------------- (15) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (16) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 1 }-> eq(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 1 }-> min(1 + m + x) :|: n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 1 }-> min(1 + n + x) :|: n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + k + replace(z', z'', x) :|: z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 1 }-> le(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 2 }-> if_min(le(n'', m'), 1 + (1 + n'') + (1 + (1 + m') + x)) :|: x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 2 }-> if_min(1, 1 + 0 + (1 + m + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 2 }-> if_min(0, 1 + (1 + n') + (1 + 0 + x)) :|: x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 2 }-> if_replace(eq(z - 1, m1), 1 + (z - 1), z', 1 + (1 + m1) + x) :|: z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 0, z', 1 + (1 + m'') + x) :|: m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 1 }-> 1 + min(1 + n + x) + sort(replace(0, n, x)) :|: n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 2 }-> 1 + min(1 + n + (1 + m2 + x')) + sort(replace(if_min(le(n, m2), 1 + n + (1 + m2 + x')), n, 1 + m2 + x')) :|: n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 2 }-> 1 + min(1 + 0 + 0) + sort(replace(0, 0, 0)) :|: z = 1 + 0 + 0 sort(z) -{ 2 }-> 1 + min(1 + (1 + (z - 2)) + 0) + sort(replace(1 + (z - 2), 1 + (z - 2), 0)) :|: z - 2 >= 0 Function symbols to be analyzed: {le}, {eq}, {min,if_min}, {replace,if_replace}, {sort} ---------------------------------------- (17) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: le after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 1 ---------------------------------------- (18) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 1 }-> eq(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 1 }-> min(1 + m + x) :|: n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 1 }-> min(1 + n + x) :|: n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + k + replace(z', z'', x) :|: z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 1 }-> le(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 2 }-> if_min(le(n'', m'), 1 + (1 + n'') + (1 + (1 + m') + x)) :|: x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 2 }-> if_min(1, 1 + 0 + (1 + m + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 2 }-> if_min(0, 1 + (1 + n') + (1 + 0 + x)) :|: x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 2 }-> if_replace(eq(z - 1, m1), 1 + (z - 1), z', 1 + (1 + m1) + x) :|: z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 0, z', 1 + (1 + m'') + x) :|: m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 1 }-> 1 + min(1 + n + x) + sort(replace(0, n, x)) :|: n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 2 }-> 1 + min(1 + n + (1 + m2 + x')) + sort(replace(if_min(le(n, m2), 1 + n + (1 + m2 + x')), n, 1 + m2 + x')) :|: n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 2 }-> 1 + min(1 + 0 + 0) + sort(replace(0, 0, 0)) :|: z = 1 + 0 + 0 sort(z) -{ 2 }-> 1 + min(1 + (1 + (z - 2)) + 0) + sort(replace(1 + (z - 2), 1 + (z - 2), 0)) :|: z - 2 >= 0 Function symbols to be analyzed: {le}, {eq}, {min,if_min}, {replace,if_replace}, {sort} Previous analysis results are: le: runtime: ?, size: O(1) [1] ---------------------------------------- (19) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using KoAT for: le after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 2 + z' ---------------------------------------- (20) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 1 }-> eq(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 1 }-> min(1 + m + x) :|: n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 1 }-> min(1 + n + x) :|: n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + k + replace(z', z'', x) :|: z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 1 }-> le(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 2 }-> if_min(le(n'', m'), 1 + (1 + n'') + (1 + (1 + m') + x)) :|: x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 2 }-> if_min(1, 1 + 0 + (1 + m + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 2 }-> if_min(0, 1 + (1 + n') + (1 + 0 + x)) :|: x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 2 }-> if_replace(eq(z - 1, m1), 1 + (z - 1), z', 1 + (1 + m1) + x) :|: z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 0, z', 1 + (1 + m'') + x) :|: m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 1 }-> 1 + min(1 + n + x) + sort(replace(0, n, x)) :|: n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 2 }-> 1 + min(1 + n + (1 + m2 + x')) + sort(replace(if_min(le(n, m2), 1 + n + (1 + m2 + x')), n, 1 + m2 + x')) :|: n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 2 }-> 1 + min(1 + 0 + 0) + sort(replace(0, 0, 0)) :|: z = 1 + 0 + 0 sort(z) -{ 2 }-> 1 + min(1 + (1 + (z - 2)) + 0) + sort(replace(1 + (z - 2), 1 + (z - 2), 0)) :|: z - 2 >= 0 Function symbols to be analyzed: {eq}, {min,if_min}, {replace,if_replace}, {sort} Previous analysis results are: le: runtime: O(n^1) [2 + z'], size: O(1) [1] ---------------------------------------- (21) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (22) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 1 }-> eq(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 1 }-> min(1 + m + x) :|: n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 1 }-> min(1 + n + x) :|: n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + k + replace(z', z'', x) :|: z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 2 + z' }-> s :|: s >= 0, s <= 1, z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 4 + m' }-> if_min(s', 1 + (1 + n'') + (1 + (1 + m') + x)) :|: s' >= 0, s' <= 1, x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 2 }-> if_min(1, 1 + 0 + (1 + m + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 2 }-> if_min(0, 1 + (1 + n') + (1 + 0 + x)) :|: x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 2 }-> if_replace(eq(z - 1, m1), 1 + (z - 1), z', 1 + (1 + m1) + x) :|: z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 0, z', 1 + (1 + m'') + x) :|: m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 1 }-> 1 + min(1 + n + x) + sort(replace(0, n, x)) :|: n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 4 + m2 }-> 1 + min(1 + n + (1 + m2 + x')) + sort(replace(if_min(s'', 1 + n + (1 + m2 + x')), n, 1 + m2 + x')) :|: s'' >= 0, s'' <= 1, n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 2 }-> 1 + min(1 + 0 + 0) + sort(replace(0, 0, 0)) :|: z = 1 + 0 + 0 sort(z) -{ 2 }-> 1 + min(1 + (1 + (z - 2)) + 0) + sort(replace(1 + (z - 2), 1 + (z - 2), 0)) :|: z - 2 >= 0 Function symbols to be analyzed: {eq}, {min,if_min}, {replace,if_replace}, {sort} Previous analysis results are: le: runtime: O(n^1) [2 + z'], size: O(1) [1] ---------------------------------------- (23) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: eq after applying outer abstraction to obtain an ITS, resulting in: O(1) with polynomial bound: 1 ---------------------------------------- (24) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 1 }-> eq(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 1 }-> min(1 + m + x) :|: n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 1 }-> min(1 + n + x) :|: n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + k + replace(z', z'', x) :|: z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 2 + z' }-> s :|: s >= 0, s <= 1, z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 4 + m' }-> if_min(s', 1 + (1 + n'') + (1 + (1 + m') + x)) :|: s' >= 0, s' <= 1, x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 2 }-> if_min(1, 1 + 0 + (1 + m + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 2 }-> if_min(0, 1 + (1 + n') + (1 + 0 + x)) :|: x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 2 }-> if_replace(eq(z - 1, m1), 1 + (z - 1), z', 1 + (1 + m1) + x) :|: z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 0, z', 1 + (1 + m'') + x) :|: m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 1 }-> 1 + min(1 + n + x) + sort(replace(0, n, x)) :|: n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 4 + m2 }-> 1 + min(1 + n + (1 + m2 + x')) + sort(replace(if_min(s'', 1 + n + (1 + m2 + x')), n, 1 + m2 + x')) :|: s'' >= 0, s'' <= 1, n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 2 }-> 1 + min(1 + 0 + 0) + sort(replace(0, 0, 0)) :|: z = 1 + 0 + 0 sort(z) -{ 2 }-> 1 + min(1 + (1 + (z - 2)) + 0) + sort(replace(1 + (z - 2), 1 + (z - 2), 0)) :|: z - 2 >= 0 Function symbols to be analyzed: {eq}, {min,if_min}, {replace,if_replace}, {sort} Previous analysis results are: le: runtime: O(n^1) [2 + z'], size: O(1) [1] eq: runtime: ?, size: O(1) [1] ---------------------------------------- (25) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using KoAT for: eq after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: 3 + z' ---------------------------------------- (26) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 1 }-> eq(z - 1, z' - 1) :|: z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 1 }-> min(1 + m + x) :|: n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 1 }-> min(1 + n + x) :|: n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + k + replace(z', z'', x) :|: z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 2 + z' }-> s :|: s >= 0, s <= 1, z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 4 + m' }-> if_min(s', 1 + (1 + n'') + (1 + (1 + m') + x)) :|: s' >= 0, s' <= 1, x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 2 }-> if_min(1, 1 + 0 + (1 + m + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 2 }-> if_min(0, 1 + (1 + n') + (1 + 0 + x)) :|: x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 2 }-> if_replace(eq(z - 1, m1), 1 + (z - 1), z', 1 + (1 + m1) + x) :|: z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 0, z', 1 + (1 + m'') + x) :|: m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 1 }-> 1 + min(1 + n + x) + sort(replace(0, n, x)) :|: n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 4 + m2 }-> 1 + min(1 + n + (1 + m2 + x')) + sort(replace(if_min(s'', 1 + n + (1 + m2 + x')), n, 1 + m2 + x')) :|: s'' >= 0, s'' <= 1, n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 2 }-> 1 + min(1 + 0 + 0) + sort(replace(0, 0, 0)) :|: z = 1 + 0 + 0 sort(z) -{ 2 }-> 1 + min(1 + (1 + (z - 2)) + 0) + sort(replace(1 + (z - 2), 1 + (z - 2), 0)) :|: z - 2 >= 0 Function symbols to be analyzed: {min,if_min}, {replace,if_replace}, {sort} Previous analysis results are: le: runtime: O(n^1) [2 + z'], size: O(1) [1] eq: runtime: O(n^1) [3 + z'], size: O(1) [1] ---------------------------------------- (27) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (28) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 3 + z' }-> s1 :|: s1 >= 0, s1 <= 1, z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 1 }-> min(1 + m + x) :|: n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 1 }-> min(1 + n + x) :|: n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + k + replace(z', z'', x) :|: z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 2 + z' }-> s :|: s >= 0, s <= 1, z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 4 + m' }-> if_min(s', 1 + (1 + n'') + (1 + (1 + m') + x)) :|: s' >= 0, s' <= 1, x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 2 }-> if_min(1, 1 + 0 + (1 + m + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 2 }-> if_min(0, 1 + (1 + n') + (1 + 0 + x)) :|: x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 5 + m1 }-> if_replace(s2, 1 + (z - 1), z', 1 + (1 + m1) + x) :|: s2 >= 0, s2 <= 1, z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 0, z', 1 + (1 + m'') + x) :|: m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 1 }-> 1 + min(1 + n + x) + sort(replace(0, n, x)) :|: n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 4 + m2 }-> 1 + min(1 + n + (1 + m2 + x')) + sort(replace(if_min(s'', 1 + n + (1 + m2 + x')), n, 1 + m2 + x')) :|: s'' >= 0, s'' <= 1, n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 2 }-> 1 + min(1 + 0 + 0) + sort(replace(0, 0, 0)) :|: z = 1 + 0 + 0 sort(z) -{ 2 }-> 1 + min(1 + (1 + (z - 2)) + 0) + sort(replace(1 + (z - 2), 1 + (z - 2), 0)) :|: z - 2 >= 0 Function symbols to be analyzed: {min,if_min}, {replace,if_replace}, {sort} Previous analysis results are: le: runtime: O(n^1) [2 + z'], size: O(1) [1] eq: runtime: O(n^1) [3 + z'], size: O(1) [1] ---------------------------------------- (29) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: min after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z Computed SIZE bound using KoAT for: if_min after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z' ---------------------------------------- (30) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 3 + z' }-> s1 :|: s1 >= 0, s1 <= 1, z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 1 }-> min(1 + m + x) :|: n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 1 }-> min(1 + n + x) :|: n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + k + replace(z', z'', x) :|: z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 2 + z' }-> s :|: s >= 0, s <= 1, z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 4 + m' }-> if_min(s', 1 + (1 + n'') + (1 + (1 + m') + x)) :|: s' >= 0, s' <= 1, x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 2 }-> if_min(1, 1 + 0 + (1 + m + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 2 }-> if_min(0, 1 + (1 + n') + (1 + 0 + x)) :|: x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 5 + m1 }-> if_replace(s2, 1 + (z - 1), z', 1 + (1 + m1) + x) :|: s2 >= 0, s2 <= 1, z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 0, z', 1 + (1 + m'') + x) :|: m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 1 }-> 1 + min(1 + n + x) + sort(replace(0, n, x)) :|: n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 4 + m2 }-> 1 + min(1 + n + (1 + m2 + x')) + sort(replace(if_min(s'', 1 + n + (1 + m2 + x')), n, 1 + m2 + x')) :|: s'' >= 0, s'' <= 1, n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 2 }-> 1 + min(1 + 0 + 0) + sort(replace(0, 0, 0)) :|: z = 1 + 0 + 0 sort(z) -{ 2 }-> 1 + min(1 + (1 + (z - 2)) + 0) + sort(replace(1 + (z - 2), 1 + (z - 2), 0)) :|: z - 2 >= 0 Function symbols to be analyzed: {min,if_min}, {replace,if_replace}, {sort} Previous analysis results are: le: runtime: O(n^1) [2 + z'], size: O(1) [1] eq: runtime: O(n^1) [3 + z'], size: O(1) [1] min: runtime: ?, size: O(n^1) [z] if_min: runtime: ?, size: O(n^1) [z'] ---------------------------------------- (31) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: min after applying outer abstraction to obtain an ITS, resulting in: O(n^2) with polynomial bound: 5 + 4*z + z^2 Computed RUNTIME bound using KoAT for: if_min after applying outer abstraction to obtain an ITS, resulting in: O(n^2) with polynomial bound: 22 + 24*z' + 8*z'^2 ---------------------------------------- (32) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 3 + z' }-> s1 :|: s1 >= 0, s1 <= 1, z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 1 }-> min(1 + m + x) :|: n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 1 }-> min(1 + n + x) :|: n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + k + replace(z', z'', x) :|: z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 2 + z' }-> s :|: s >= 0, s <= 1, z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 4 + m' }-> if_min(s', 1 + (1 + n'') + (1 + (1 + m') + x)) :|: s' >= 0, s' <= 1, x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 2 }-> if_min(1, 1 + 0 + (1 + m + x)) :|: x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 2 }-> if_min(0, 1 + (1 + n') + (1 + 0 + x)) :|: x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 5 + m1 }-> if_replace(s2, 1 + (z - 1), z', 1 + (1 + m1) + x) :|: s2 >= 0, s2 <= 1, z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 0, z', 1 + (1 + m'') + x) :|: m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 1 }-> 1 + min(1 + n + x) + sort(replace(0, n, x)) :|: n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 4 + m2 }-> 1 + min(1 + n + (1 + m2 + x')) + sort(replace(if_min(s'', 1 + n + (1 + m2 + x')), n, 1 + m2 + x')) :|: s'' >= 0, s'' <= 1, n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 2 }-> 1 + min(1 + 0 + 0) + sort(replace(0, 0, 0)) :|: z = 1 + 0 + 0 sort(z) -{ 2 }-> 1 + min(1 + (1 + (z - 2)) + 0) + sort(replace(1 + (z - 2), 1 + (z - 2), 0)) :|: z - 2 >= 0 Function symbols to be analyzed: {replace,if_replace}, {sort} Previous analysis results are: le: runtime: O(n^1) [2 + z'], size: O(1) [1] eq: runtime: O(n^1) [3 + z'], size: O(1) [1] min: runtime: O(n^2) [5 + 4*z + z^2], size: O(n^1) [z] if_min: runtime: O(n^2) [22 + 24*z' + 8*z'^2], size: O(n^1) [z'] ---------------------------------------- (33) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (34) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 3 + z' }-> s1 :|: s1 >= 0, s1 <= 1, z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 11 + 6*n + 2*n*x + n^2 + 6*x + x^2 }-> s6 :|: s6 >= 0, s6 <= 1 + n + x, n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 11 + 6*m + 2*m*x + m^2 + 6*x + x^2 }-> s7 :|: s7 >= 0, s7 <= 1 + m + x, n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + k + replace(z', z'', x) :|: z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 2 + z' }-> s :|: s >= 0, s <= 1, z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 104 + 56*m + 16*m*x + 8*m^2 + 56*x + 8*x^2 }-> s3 :|: s3 >= 0, s3 <= 1 + 0 + (1 + m + x), x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 168 + 72*n' + 16*n'*x + 8*n'^2 + 72*x + 8*x^2 }-> s4 :|: s4 >= 0, s4 <= 1 + (1 + n') + (1 + 0 + x), x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 250 + 89*m' + 16*m'*n'' + 16*m'*x + 8*m'^2 + 88*n'' + 16*n''*x + 8*n''^2 + 88*x + 8*x^2 }-> s5 :|: s5 >= 0, s5 <= 1 + (1 + n'') + (1 + (1 + m') + x), s' >= 0, s' <= 1, x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 5 + m1 }-> if_replace(s2, 1 + (z - 1), z', 1 + (1 + m1) + x) :|: s2 >= 0, s2 <= 1, z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 0, z', 1 + (1 + m'') + x) :|: m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 123 + 65*m2 + 18*m2*n + 18*m2*x' + 9*m2^2 + 64*n + 18*n*x' + 9*n^2 + 64*x' + 9*x'^2 }-> 1 + s10 + sort(replace(s11, n, 1 + m2 + x')) :|: s10 >= 0, s10 <= 1 + n + (1 + m2 + x'), s11 >= 0, s11 <= 1 + n + (1 + m2 + x'), s'' >= 0, s'' <= 1, n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 11 + 6*n + 2*n*x + n^2 + 6*x + x^2 }-> 1 + s12 + sort(replace(0, n, x)) :|: s12 >= 0, s12 <= 1 + n + x, n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 12 }-> 1 + s8 + sort(replace(0, 0, 0)) :|: s8 >= 0, s8 <= 1 + 0 + 0, z = 1 + 0 + 0 sort(z) -{ 7 + 4*z + z^2 }-> 1 + s9 + sort(replace(1 + (z - 2), 1 + (z - 2), 0)) :|: s9 >= 0, s9 <= 1 + (1 + (z - 2)) + 0, z - 2 >= 0 Function symbols to be analyzed: {replace,if_replace}, {sort} Previous analysis results are: le: runtime: O(n^1) [2 + z'], size: O(1) [1] eq: runtime: O(n^1) [3 + z'], size: O(1) [1] min: runtime: O(n^2) [5 + 4*z + z^2], size: O(n^1) [z] if_min: runtime: O(n^2) [22 + 24*z' + 8*z'^2], size: O(n^1) [z'] ---------------------------------------- (35) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using KoAT for: replace after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z' + z'' Computed SIZE bound using CoFloCo for: if_replace after applying outer abstraction to obtain an ITS, resulting in: O(n^1) with polynomial bound: z'' + z1 ---------------------------------------- (36) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 3 + z' }-> s1 :|: s1 >= 0, s1 <= 1, z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 11 + 6*n + 2*n*x + n^2 + 6*x + x^2 }-> s6 :|: s6 >= 0, s6 <= 1 + n + x, n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 11 + 6*m + 2*m*x + m^2 + 6*x + x^2 }-> s7 :|: s7 >= 0, s7 <= 1 + m + x, n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + k + replace(z', z'', x) :|: z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 2 + z' }-> s :|: s >= 0, s <= 1, z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 104 + 56*m + 16*m*x + 8*m^2 + 56*x + 8*x^2 }-> s3 :|: s3 >= 0, s3 <= 1 + 0 + (1 + m + x), x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 168 + 72*n' + 16*n'*x + 8*n'^2 + 72*x + 8*x^2 }-> s4 :|: s4 >= 0, s4 <= 1 + (1 + n') + (1 + 0 + x), x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 250 + 89*m' + 16*m'*n'' + 16*m'*x + 8*m'^2 + 88*n'' + 16*n''*x + 8*n''^2 + 88*x + 8*x^2 }-> s5 :|: s5 >= 0, s5 <= 1 + (1 + n'') + (1 + (1 + m') + x), s' >= 0, s' <= 1, x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 5 + m1 }-> if_replace(s2, 1 + (z - 1), z', 1 + (1 + m1) + x) :|: s2 >= 0, s2 <= 1, z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 0, z', 1 + (1 + m'') + x) :|: m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 123 + 65*m2 + 18*m2*n + 18*m2*x' + 9*m2^2 + 64*n + 18*n*x' + 9*n^2 + 64*x' + 9*x'^2 }-> 1 + s10 + sort(replace(s11, n, 1 + m2 + x')) :|: s10 >= 0, s10 <= 1 + n + (1 + m2 + x'), s11 >= 0, s11 <= 1 + n + (1 + m2 + x'), s'' >= 0, s'' <= 1, n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 11 + 6*n + 2*n*x + n^2 + 6*x + x^2 }-> 1 + s12 + sort(replace(0, n, x)) :|: s12 >= 0, s12 <= 1 + n + x, n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 12 }-> 1 + s8 + sort(replace(0, 0, 0)) :|: s8 >= 0, s8 <= 1 + 0 + 0, z = 1 + 0 + 0 sort(z) -{ 7 + 4*z + z^2 }-> 1 + s9 + sort(replace(1 + (z - 2), 1 + (z - 2), 0)) :|: s9 >= 0, s9 <= 1 + (1 + (z - 2)) + 0, z - 2 >= 0 Function symbols to be analyzed: {replace,if_replace}, {sort} Previous analysis results are: le: runtime: O(n^1) [2 + z'], size: O(1) [1] eq: runtime: O(n^1) [3 + z'], size: O(1) [1] min: runtime: O(n^2) [5 + 4*z + z^2], size: O(n^1) [z] if_min: runtime: O(n^2) [22 + 24*z' + 8*z'^2], size: O(n^1) [z'] replace: runtime: ?, size: O(n^1) [z' + z''] if_replace: runtime: ?, size: O(n^1) [z'' + z1] ---------------------------------------- (37) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using CoFloCo for: replace after applying outer abstraction to obtain an ITS, resulting in: O(n^2) with polynomial bound: 6 + 5*z'' + z''^2 Computed RUNTIME bound using KoAT for: if_replace after applying outer abstraction to obtain an ITS, resulting in: O(n^2) with polynomial bound: 8 + 5*z1 + z1^2 ---------------------------------------- (38) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 3 + z' }-> s1 :|: s1 >= 0, s1 <= 1, z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 11 + 6*n + 2*n*x + n^2 + 6*x + x^2 }-> s6 :|: s6 >= 0, s6 <= 1 + n + x, n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 11 + 6*m + 2*m*x + m^2 + 6*x + x^2 }-> s7 :|: s7 >= 0, s7 <= 1 + m + x, n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + k + replace(z', z'', x) :|: z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 2 + z' }-> s :|: s >= 0, s <= 1, z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 104 + 56*m + 16*m*x + 8*m^2 + 56*x + 8*x^2 }-> s3 :|: s3 >= 0, s3 <= 1 + 0 + (1 + m + x), x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 168 + 72*n' + 16*n'*x + 8*n'^2 + 72*x + 8*x^2 }-> s4 :|: s4 >= 0, s4 <= 1 + (1 + n') + (1 + 0 + x), x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 250 + 89*m' + 16*m'*n'' + 16*m'*x + 8*m'^2 + 88*n'' + 16*n''*x + 8*n''^2 + 88*x + 8*x^2 }-> s5 :|: s5 >= 0, s5 <= 1 + (1 + n'') + (1 + (1 + m') + x), s' >= 0, s' <= 1, x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 5 + m1 }-> if_replace(s2, 1 + (z - 1), z', 1 + (1 + m1) + x) :|: s2 >= 0, s2 <= 1, z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 0, z', 1 + (1 + m'') + x) :|: m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 2 }-> if_replace(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 123 + 65*m2 + 18*m2*n + 18*m2*x' + 9*m2^2 + 64*n + 18*n*x' + 9*n^2 + 64*x' + 9*x'^2 }-> 1 + s10 + sort(replace(s11, n, 1 + m2 + x')) :|: s10 >= 0, s10 <= 1 + n + (1 + m2 + x'), s11 >= 0, s11 <= 1 + n + (1 + m2 + x'), s'' >= 0, s'' <= 1, n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 11 + 6*n + 2*n*x + n^2 + 6*x + x^2 }-> 1 + s12 + sort(replace(0, n, x)) :|: s12 >= 0, s12 <= 1 + n + x, n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 12 }-> 1 + s8 + sort(replace(0, 0, 0)) :|: s8 >= 0, s8 <= 1 + 0 + 0, z = 1 + 0 + 0 sort(z) -{ 7 + 4*z + z^2 }-> 1 + s9 + sort(replace(1 + (z - 2), 1 + (z - 2), 0)) :|: s9 >= 0, s9 <= 1 + (1 + (z - 2)) + 0, z - 2 >= 0 Function symbols to be analyzed: {sort} Previous analysis results are: le: runtime: O(n^1) [2 + z'], size: O(1) [1] eq: runtime: O(n^1) [3 + z'], size: O(1) [1] min: runtime: O(n^2) [5 + 4*z + z^2], size: O(n^1) [z] if_min: runtime: O(n^2) [22 + 24*z' + 8*z'^2], size: O(n^1) [z'] replace: runtime: O(n^2) [6 + 5*z'' + z''^2], size: O(n^1) [z' + z''] if_replace: runtime: O(n^2) [8 + 5*z1 + z1^2], size: O(n^1) [z'' + z1] ---------------------------------------- (39) ResultPropagationProof (UPPER BOUND(ID)) Applied inner abstraction using the recently inferred runtime/size bounds where possible. ---------------------------------------- (40) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 3 + z' }-> s1 :|: s1 >= 0, s1 <= 1, z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 11 + 6*n + 2*n*x + n^2 + 6*x + x^2 }-> s6 :|: s6 >= 0, s6 <= 1 + n + x, n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 11 + 6*m + 2*m*x + m^2 + 6*x + x^2 }-> s7 :|: s7 >= 0, s7 <= 1 + m + x, n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 7 + 5*x + x^2 }-> 1 + k + s17 :|: s17 >= 0, s17 <= z'' + x, z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 2 + z' }-> s :|: s >= 0, s <= 1, z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 104 + 56*m + 16*m*x + 8*m^2 + 56*x + 8*x^2 }-> s3 :|: s3 >= 0, s3 <= 1 + 0 + (1 + m + x), x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 168 + 72*n' + 16*n'*x + 8*n'^2 + 72*x + 8*x^2 }-> s4 :|: s4 >= 0, s4 <= 1 + (1 + n') + (1 + 0 + x), x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 250 + 89*m' + 16*m'*n'' + 16*m'*x + 8*m'^2 + 88*n'' + 16*n''*x + 8*n''^2 + 88*x + 8*x^2 }-> s5 :|: s5 >= 0, s5 <= 1 + (1 + n'') + (1 + (1 + m') + x), s' >= 0, s' <= 1, x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 10 + 5*z'' + z''^2 }-> s13 :|: s13 >= 0, s13 <= z' + (1 + 0 + (z'' - 1)), z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 24 + 9*m'' + 2*m''*x + m''^2 + 9*x + x^2 }-> s14 :|: s14 >= 0, s14 <= z' + (1 + (1 + m'') + x), m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 10 + 5*z'' + z''^2 }-> s15 :|: s15 >= 0, s15 <= z' + (1 + 0 + (z'' - 1)), z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 27 + 10*m1 + 2*m1*x + m1^2 + 9*x + x^2 }-> s16 :|: s16 >= 0, s16 <= z' + (1 + (1 + m1) + x), s2 >= 0, s2 <= 1, z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 135 + 72*m2 + 18*m2*n + 20*m2*x' + 10*m2^2 + 64*n + 18*n*x' + 9*n^2 + 71*x' + 10*x'^2 }-> 1 + s10 + sort(s20) :|: s20 >= 0, s20 <= n + (1 + m2 + x'), s10 >= 0, s10 <= 1 + n + (1 + m2 + x'), s11 >= 0, s11 <= 1 + n + (1 + m2 + x'), s'' >= 0, s'' <= 1, n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 17 + 6*n + 2*n*x + n^2 + 11*x + 2*x^2 }-> 1 + s12 + sort(s21) :|: s21 >= 0, s21 <= n + x, s12 >= 0, s12 <= 1 + n + x, n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 18 }-> 1 + s8 + sort(s18) :|: s18 >= 0, s18 <= 0 + 0, s8 >= 0, s8 <= 1 + 0 + 0, z = 1 + 0 + 0 sort(z) -{ 13 + 4*z + z^2 }-> 1 + s9 + sort(s19) :|: s19 >= 0, s19 <= 1 + (z - 2) + 0, s9 >= 0, s9 <= 1 + (1 + (z - 2)) + 0, z - 2 >= 0 Function symbols to be analyzed: {sort} Previous analysis results are: le: runtime: O(n^1) [2 + z'], size: O(1) [1] eq: runtime: O(n^1) [3 + z'], size: O(1) [1] min: runtime: O(n^2) [5 + 4*z + z^2], size: O(n^1) [z] if_min: runtime: O(n^2) [22 + 24*z' + 8*z'^2], size: O(n^1) [z'] replace: runtime: O(n^2) [6 + 5*z'' + z''^2], size: O(n^1) [z' + z''] if_replace: runtime: O(n^2) [8 + 5*z1 + z1^2], size: O(n^1) [z'' + z1] ---------------------------------------- (41) IntTrsBoundProof (UPPER BOUND(ID)) Computed SIZE bound using CoFloCo for: sort after applying outer abstraction to obtain an ITS, resulting in: O(n^2) with polynomial bound: z + z^2 ---------------------------------------- (42) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 3 + z' }-> s1 :|: s1 >= 0, s1 <= 1, z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 11 + 6*n + 2*n*x + n^2 + 6*x + x^2 }-> s6 :|: s6 >= 0, s6 <= 1 + n + x, n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 11 + 6*m + 2*m*x + m^2 + 6*x + x^2 }-> s7 :|: s7 >= 0, s7 <= 1 + m + x, n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 7 + 5*x + x^2 }-> 1 + k + s17 :|: s17 >= 0, s17 <= z'' + x, z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 2 + z' }-> s :|: s >= 0, s <= 1, z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 104 + 56*m + 16*m*x + 8*m^2 + 56*x + 8*x^2 }-> s3 :|: s3 >= 0, s3 <= 1 + 0 + (1 + m + x), x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 168 + 72*n' + 16*n'*x + 8*n'^2 + 72*x + 8*x^2 }-> s4 :|: s4 >= 0, s4 <= 1 + (1 + n') + (1 + 0 + x), x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 250 + 89*m' + 16*m'*n'' + 16*m'*x + 8*m'^2 + 88*n'' + 16*n''*x + 8*n''^2 + 88*x + 8*x^2 }-> s5 :|: s5 >= 0, s5 <= 1 + (1 + n'') + (1 + (1 + m') + x), s' >= 0, s' <= 1, x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 10 + 5*z'' + z''^2 }-> s13 :|: s13 >= 0, s13 <= z' + (1 + 0 + (z'' - 1)), z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 24 + 9*m'' + 2*m''*x + m''^2 + 9*x + x^2 }-> s14 :|: s14 >= 0, s14 <= z' + (1 + (1 + m'') + x), m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 10 + 5*z'' + z''^2 }-> s15 :|: s15 >= 0, s15 <= z' + (1 + 0 + (z'' - 1)), z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 27 + 10*m1 + 2*m1*x + m1^2 + 9*x + x^2 }-> s16 :|: s16 >= 0, s16 <= z' + (1 + (1 + m1) + x), s2 >= 0, s2 <= 1, z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 135 + 72*m2 + 18*m2*n + 20*m2*x' + 10*m2^2 + 64*n + 18*n*x' + 9*n^2 + 71*x' + 10*x'^2 }-> 1 + s10 + sort(s20) :|: s20 >= 0, s20 <= n + (1 + m2 + x'), s10 >= 0, s10 <= 1 + n + (1 + m2 + x'), s11 >= 0, s11 <= 1 + n + (1 + m2 + x'), s'' >= 0, s'' <= 1, n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 17 + 6*n + 2*n*x + n^2 + 11*x + 2*x^2 }-> 1 + s12 + sort(s21) :|: s21 >= 0, s21 <= n + x, s12 >= 0, s12 <= 1 + n + x, n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 18 }-> 1 + s8 + sort(s18) :|: s18 >= 0, s18 <= 0 + 0, s8 >= 0, s8 <= 1 + 0 + 0, z = 1 + 0 + 0 sort(z) -{ 13 + 4*z + z^2 }-> 1 + s9 + sort(s19) :|: s19 >= 0, s19 <= 1 + (z - 2) + 0, s9 >= 0, s9 <= 1 + (1 + (z - 2)) + 0, z - 2 >= 0 Function symbols to be analyzed: {sort} Previous analysis results are: le: runtime: O(n^1) [2 + z'], size: O(1) [1] eq: runtime: O(n^1) [3 + z'], size: O(1) [1] min: runtime: O(n^2) [5 + 4*z + z^2], size: O(n^1) [z] if_min: runtime: O(n^2) [22 + 24*z' + 8*z'^2], size: O(n^1) [z'] replace: runtime: O(n^2) [6 + 5*z'' + z''^2], size: O(n^1) [z' + z''] if_replace: runtime: O(n^2) [8 + 5*z1 + z1^2], size: O(n^1) [z'' + z1] sort: runtime: ?, size: O(n^2) [z + z^2] ---------------------------------------- (43) IntTrsBoundProof (UPPER BOUND(ID)) Computed RUNTIME bound using KoAT for: sort after applying outer abstraction to obtain an ITS, resulting in: O(n^3) with polynomial bound: 1 + 183*z + 228*z^2 + 91*z^3 ---------------------------------------- (44) Obligation: Complexity RNTS consisting of the following rules: eq(z, z') -{ 3 + z' }-> s1 :|: s1 >= 0, s1 <= 1, z - 1 >= 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 1 :|: z = 0, z' = 0 eq(z, z') -{ 1 }-> 0 :|: z = 0, z' - 1 >= 0 eq(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 if_min(z, z') -{ 11 + 6*n + 2*n*x + n^2 + 6*x + x^2 }-> s6 :|: s6 >= 0, s6 <= 1 + n + x, n >= 0, z = 1, x >= 0, z' = 1 + n + (1 + m + x), m >= 0 if_min(z, z') -{ 11 + 6*m + 2*m*x + m^2 + 6*x + x^2 }-> s7 :|: s7 >= 0, s7 <= 1 + m + x, n >= 0, x >= 0, z' = 1 + n + (1 + m + x), z = 0, m >= 0 if_min(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0 if_replace(z, z', z'', z1) -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0 if_replace(z, z', z'', z1) -{ 7 + 5*x + x^2 }-> 1 + k + s17 :|: s17 >= 0, s17 <= z'' + x, z' >= 0, x >= 0, z1 = 1 + k + x, k >= 0, z = 0, z'' >= 0 if_replace(z, z', z'', z1) -{ 1 }-> 1 + z'' + x :|: z' >= 0, z = 1, x >= 0, z1 = 1 + k + x, k >= 0, z'' >= 0 le(z, z') -{ 2 + z' }-> s :|: s >= 0, s <= 1, z - 1 >= 0, z' - 1 >= 0 le(z, z') -{ 1 }-> 1 :|: z = 0, z' >= 0 le(z, z') -{ 1 }-> 0 :|: z - 1 >= 0, z' = 0 min(z) -{ 104 + 56*m + 16*m*x + 8*m^2 + 56*x + 8*x^2 }-> s3 :|: s3 >= 0, s3 <= 1 + 0 + (1 + m + x), x >= 0, z = 1 + 0 + (1 + m + x), m >= 0 min(z) -{ 168 + 72*n' + 16*n'*x + 8*n'^2 + 72*x + 8*x^2 }-> s4 :|: s4 >= 0, s4 <= 1 + (1 + n') + (1 + 0 + x), x >= 0, z = 1 + (1 + n') + (1 + 0 + x), n' >= 0 min(z) -{ 250 + 89*m' + 16*m'*n'' + 16*m'*x + 8*m'^2 + 88*n'' + 16*n''*x + 8*n''^2 + 88*x + 8*x^2 }-> s5 :|: s5 >= 0, s5 <= 1 + (1 + n'') + (1 + (1 + m') + x), s' >= 0, s' <= 1, x >= 0, z = 1 + (1 + n'') + (1 + (1 + m') + x), m' >= 0, n'' >= 0 min(z) -{ 1 }-> 0 :|: z = 1 + 0 + 0 min(z) -{ 0 }-> 0 :|: z >= 0 min(z) -{ 1 }-> 1 + (z - 2) :|: z - 2 >= 0 replace(z, z', z'') -{ 10 + 5*z'' + z''^2 }-> s13 :|: s13 >= 0, s13 <= z' + (1 + 0 + (z'' - 1)), z'' - 1 >= 0, z = 0, z' >= 0 replace(z, z', z'') -{ 24 + 9*m'' + 2*m''*x + m''^2 + 9*x + x^2 }-> s14 :|: s14 >= 0, s14 <= z' + (1 + (1 + m'') + x), m'' >= 0, x >= 0, z'' = 1 + (1 + m'') + x, z = 0, z' >= 0 replace(z, z', z'') -{ 10 + 5*z'' + z''^2 }-> s15 :|: s15 >= 0, s15 <= z' + (1 + 0 + (z'' - 1)), z'' - 1 >= 0, z - 1 >= 0, z' >= 0 replace(z, z', z'') -{ 27 + 10*m1 + 2*m1*x + m1^2 + 9*x + x^2 }-> s16 :|: s16 >= 0, s16 <= z' + (1 + (1 + m1) + x), s2 >= 0, s2 <= 1, z'' = 1 + (1 + m1) + x, x >= 0, z - 1 >= 0, m1 >= 0, z' >= 0 replace(z, z', z'') -{ 1 }-> 0 :|: z'' = 0, z >= 0, z' >= 0 sort(z) -{ 1 }-> 0 :|: z = 0 sort(z) -{ 135 + 72*m2 + 18*m2*n + 20*m2*x' + 10*m2^2 + 64*n + 18*n*x' + 9*n^2 + 71*x' + 10*x'^2 }-> 1 + s10 + sort(s20) :|: s20 >= 0, s20 <= n + (1 + m2 + x'), s10 >= 0, s10 <= 1 + n + (1 + m2 + x'), s11 >= 0, s11 <= 1 + n + (1 + m2 + x'), s'' >= 0, s'' <= 1, n >= 0, x' >= 0, z = 1 + n + (1 + m2 + x'), m2 >= 0 sort(z) -{ 17 + 6*n + 2*n*x + n^2 + 11*x + 2*x^2 }-> 1 + s12 + sort(s21) :|: s21 >= 0, s21 <= n + x, s12 >= 0, s12 <= 1 + n + x, n >= 0, x >= 0, z = 1 + n + x sort(z) -{ 18 }-> 1 + s8 + sort(s18) :|: s18 >= 0, s18 <= 0 + 0, s8 >= 0, s8 <= 1 + 0 + 0, z = 1 + 0 + 0 sort(z) -{ 13 + 4*z + z^2 }-> 1 + s9 + sort(s19) :|: s19 >= 0, s19 <= 1 + (z - 2) + 0, s9 >= 0, s9 <= 1 + (1 + (z - 2)) + 0, z - 2 >= 0 Function symbols to be analyzed: Previous analysis results are: le: runtime: O(n^1) [2 + z'], size: O(1) [1] eq: runtime: O(n^1) [3 + z'], size: O(1) [1] min: runtime: O(n^2) [5 + 4*z + z^2], size: O(n^1) [z] if_min: runtime: O(n^2) [22 + 24*z' + 8*z'^2], size: O(n^1) [z'] replace: runtime: O(n^2) [6 + 5*z'' + z''^2], size: O(n^1) [z' + z''] if_replace: runtime: O(n^2) [8 + 5*z1 + z1^2], size: O(n^1) [z'' + z1] sort: runtime: O(n^3) [1 + 183*z + 228*z^2 + 91*z^3], size: O(n^2) [z + z^2] ---------------------------------------- (45) FinalProof (FINISHED) Computed overall runtime complexity ---------------------------------------- (46) BOUNDS(1, n^3) ---------------------------------------- (47) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (48) Obligation: Complexity Dependency Tuples Problem Rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) le(0, z0) -> true le(s(z0), 0) -> false le(s(z0), s(z1)) -> le(z0, z1) min(cons(0, nil)) -> 0 min(cons(s(z0), nil)) -> s(z0) min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2))) if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2)) if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2)) replace(z0, z1, nil) -> nil replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3)) if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3) if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3)) sort(nil) -> nil sort(cons(z0, z1)) -> cons(min(cons(z0, z1)), sort(replace(min(cons(z0, z1)), z0, z1))) Tuples: EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) LE(0, z0) -> c4 LE(s(z0), 0) -> c5 LE(s(z0), s(z1)) -> c6(LE(z0, z1)) MIN(cons(0, nil)) -> c7 MIN(cons(s(z0), nil)) -> c8 MIN(cons(z0, cons(z1, z2))) -> c9(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1)) IF_MIN(true, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z0, z2))) IF_MIN(false, cons(z0, cons(z1, z2))) -> c11(MIN(cons(z1, z2))) REPLACE(z0, z1, nil) -> c12 REPLACE(z0, z1, cons(z2, z3)) -> c13(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2)) IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c14 IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c15(REPLACE(z0, z1, z3)) SORT(nil) -> c16 SORT(cons(z0, z1)) -> c17(MIN(cons(z0, z1))) SORT(cons(z0, z1)) -> c18(SORT(replace(min(cons(z0, z1)), z0, z1)), REPLACE(min(cons(z0, z1)), z0, z1), MIN(cons(z0, z1))) S tuples: EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) LE(0, z0) -> c4 LE(s(z0), 0) -> c5 LE(s(z0), s(z1)) -> c6(LE(z0, z1)) MIN(cons(0, nil)) -> c7 MIN(cons(s(z0), nil)) -> c8 MIN(cons(z0, cons(z1, z2))) -> c9(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1)) IF_MIN(true, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z0, z2))) IF_MIN(false, cons(z0, cons(z1, z2))) -> c11(MIN(cons(z1, z2))) REPLACE(z0, z1, nil) -> c12 REPLACE(z0, z1, cons(z2, z3)) -> c13(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2)) IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c14 IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c15(REPLACE(z0, z1, z3)) SORT(nil) -> c16 SORT(cons(z0, z1)) -> c17(MIN(cons(z0, z1))) SORT(cons(z0, z1)) -> c18(SORT(replace(min(cons(z0, z1)), z0, z1)), REPLACE(min(cons(z0, z1)), z0, z1), MIN(cons(z0, z1))) K tuples:none Defined Rule Symbols: eq_2, le_2, min_1, if_min_2, replace_3, if_replace_4, sort_1 Defined Pair Symbols: EQ_2, LE_2, MIN_1, IF_MIN_2, REPLACE_3, IF_REPLACE_4, SORT_1 Compound Symbols: c, c1, c2, c3_1, c4, c5, c6_1, c7, c8, c9_2, c10_1, c11_1, c12, c13_2, c14, c15_1, c16, c17_1, c18_3 ---------------------------------------- (49) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (50) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^2, INF). The TRS R consists of the following rules: EQ(0, 0) -> c EQ(0, s(z0)) -> c1 EQ(s(z0), 0) -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) LE(0, z0) -> c4 LE(s(z0), 0) -> c5 LE(s(z0), s(z1)) -> c6(LE(z0, z1)) MIN(cons(0, nil)) -> c7 MIN(cons(s(z0), nil)) -> c8 MIN(cons(z0, cons(z1, z2))) -> c9(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1)) IF_MIN(true, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z0, z2))) IF_MIN(false, cons(z0, cons(z1, z2))) -> c11(MIN(cons(z1, z2))) REPLACE(z0, z1, nil) -> c12 REPLACE(z0, z1, cons(z2, z3)) -> c13(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2)) IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c14 IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c15(REPLACE(z0, z1, z3)) SORT(nil) -> c16 SORT(cons(z0, z1)) -> c17(MIN(cons(z0, z1))) SORT(cons(z0, z1)) -> c18(SORT(replace(min(cons(z0, z1)), z0, z1)), REPLACE(min(cons(z0, z1)), z0, z1), MIN(cons(z0, z1))) The (relative) TRS S consists of the following rules: eq(0, 0) -> true eq(0, s(z0)) -> false eq(s(z0), 0) -> false eq(s(z0), s(z1)) -> eq(z0, z1) le(0, z0) -> true le(s(z0), 0) -> false le(s(z0), s(z1)) -> le(z0, z1) min(cons(0, nil)) -> 0 min(cons(s(z0), nil)) -> s(z0) min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2))) if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2)) if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2)) replace(z0, z1, nil) -> nil replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3)) if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3) if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3)) sort(nil) -> nil sort(cons(z0, z1)) -> cons(min(cons(z0, z1)), sort(replace(min(cons(z0, z1)), z0, z1))) Rewrite Strategy: INNERMOST ---------------------------------------- (51) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (52) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^2, INF). The TRS R consists of the following rules: EQ(0', 0') -> c EQ(0', s(z0)) -> c1 EQ(s(z0), 0') -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) LE(0', z0) -> c4 LE(s(z0), 0') -> c5 LE(s(z0), s(z1)) -> c6(LE(z0, z1)) MIN(cons(0', nil)) -> c7 MIN(cons(s(z0), nil)) -> c8 MIN(cons(z0, cons(z1, z2))) -> c9(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1)) IF_MIN(true, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z0, z2))) IF_MIN(false, cons(z0, cons(z1, z2))) -> c11(MIN(cons(z1, z2))) REPLACE(z0, z1, nil) -> c12 REPLACE(z0, z1, cons(z2, z3)) -> c13(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2)) IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c14 IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c15(REPLACE(z0, z1, z3)) SORT(nil) -> c16 SORT(cons(z0, z1)) -> c17(MIN(cons(z0, z1))) SORT(cons(z0, z1)) -> c18(SORT(replace(min(cons(z0, z1)), z0, z1)), REPLACE(min(cons(z0, z1)), z0, z1), MIN(cons(z0, z1))) The (relative) TRS S consists of the following rules: eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) min(cons(0', nil)) -> 0' min(cons(s(z0), nil)) -> s(z0) min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2))) if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2)) if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2)) replace(z0, z1, nil) -> nil replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3)) if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3) if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3)) sort(nil) -> nil sort(cons(z0, z1)) -> cons(min(cons(z0, z1)), sort(replace(min(cons(z0, z1)), z0, z1))) Rewrite Strategy: INNERMOST ---------------------------------------- (53) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (54) Obligation: Innermost TRS: Rules: EQ(0', 0') -> c EQ(0', s(z0)) -> c1 EQ(s(z0), 0') -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) LE(0', z0) -> c4 LE(s(z0), 0') -> c5 LE(s(z0), s(z1)) -> c6(LE(z0, z1)) MIN(cons(0', nil)) -> c7 MIN(cons(s(z0), nil)) -> c8 MIN(cons(z0, cons(z1, z2))) -> c9(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1)) IF_MIN(true, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z0, z2))) IF_MIN(false, cons(z0, cons(z1, z2))) -> c11(MIN(cons(z1, z2))) REPLACE(z0, z1, nil) -> c12 REPLACE(z0, z1, cons(z2, z3)) -> c13(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2)) IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c14 IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c15(REPLACE(z0, z1, z3)) SORT(nil) -> c16 SORT(cons(z0, z1)) -> c17(MIN(cons(z0, z1))) SORT(cons(z0, z1)) -> c18(SORT(replace(min(cons(z0, z1)), z0, z1)), REPLACE(min(cons(z0, z1)), z0, z1), MIN(cons(z0, z1))) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) min(cons(0', nil)) -> 0' min(cons(s(z0), nil)) -> s(z0) min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2))) if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2)) if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2)) replace(z0, z1, nil) -> nil replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3)) if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3) if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3)) sort(nil) -> nil sort(cons(z0, z1)) -> cons(min(cons(z0, z1)), sort(replace(min(cons(z0, z1)), z0, z1))) Types: EQ :: 0':s -> 0':s -> c:c1:c2:c3 0' :: 0':s c :: c:c1:c2:c3 s :: 0':s -> 0':s c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 -> c:c1:c2:c3 LE :: 0':s -> 0':s -> c4:c5:c6 c4 :: c4:c5:c6 c5 :: c4:c5:c6 c6 :: c4:c5:c6 -> c4:c5:c6 MIN :: nil:cons -> c7:c8:c9 cons :: 0':s -> nil:cons -> nil:cons nil :: nil:cons c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c10:c11 -> c4:c5:c6 -> c7:c8:c9 IF_MIN :: true:false -> nil:cons -> c10:c11 le :: 0':s -> 0':s -> true:false true :: true:false c10 :: c7:c8:c9 -> c10:c11 false :: true:false c11 :: c7:c8:c9 -> c10:c11 REPLACE :: 0':s -> 0':s -> nil:cons -> c12:c13 c12 :: c12:c13 c13 :: c14:c15 -> c:c1:c2:c3 -> c12:c13 IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons -> c14:c15 eq :: 0':s -> 0':s -> true:false c14 :: c14:c15 c15 :: c12:c13 -> c14:c15 SORT :: nil:cons -> c16:c17:c18 c16 :: c16:c17:c18 c17 :: c7:c8:c9 -> c16:c17:c18 c18 :: c16:c17:c18 -> c12:c13 -> c7:c8:c9 -> c16:c17:c18 replace :: 0':s -> 0':s -> nil:cons -> nil:cons min :: nil:cons -> 0':s if_min :: true:false -> nil:cons -> 0':s if_replace :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c2:c31_19 :: c:c1:c2:c3 hole_0':s2_19 :: 0':s hole_c4:c5:c63_19 :: c4:c5:c6 hole_c7:c8:c94_19 :: c7:c8:c9 hole_nil:cons5_19 :: nil:cons hole_c10:c116_19 :: c10:c11 hole_true:false7_19 :: true:false hole_c12:c138_19 :: c12:c13 hole_c14:c159_19 :: c14:c15 hole_c16:c17:c1810_19 :: c16:c17:c18 gen_c:c1:c2:c311_19 :: Nat -> c:c1:c2:c3 gen_0':s12_19 :: Nat -> 0':s gen_c4:c5:c613_19 :: Nat -> c4:c5:c6 gen_nil:cons14_19 :: Nat -> nil:cons gen_c16:c17:c1815_19 :: Nat -> c16:c17:c18 ---------------------------------------- (55) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: EQ, LE, MIN, le, REPLACE, eq, SORT, replace, min, sort They will be analysed ascendingly in the following order: EQ < REPLACE LE < MIN le < MIN MIN < SORT le < min eq < REPLACE REPLACE < SORT eq < replace replace < SORT min < SORT replace < sort min < sort ---------------------------------------- (56) Obligation: Innermost TRS: Rules: EQ(0', 0') -> c EQ(0', s(z0)) -> c1 EQ(s(z0), 0') -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) LE(0', z0) -> c4 LE(s(z0), 0') -> c5 LE(s(z0), s(z1)) -> c6(LE(z0, z1)) MIN(cons(0', nil)) -> c7 MIN(cons(s(z0), nil)) -> c8 MIN(cons(z0, cons(z1, z2))) -> c9(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1)) IF_MIN(true, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z0, z2))) IF_MIN(false, cons(z0, cons(z1, z2))) -> c11(MIN(cons(z1, z2))) REPLACE(z0, z1, nil) -> c12 REPLACE(z0, z1, cons(z2, z3)) -> c13(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2)) IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c14 IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c15(REPLACE(z0, z1, z3)) SORT(nil) -> c16 SORT(cons(z0, z1)) -> c17(MIN(cons(z0, z1))) SORT(cons(z0, z1)) -> c18(SORT(replace(min(cons(z0, z1)), z0, z1)), REPLACE(min(cons(z0, z1)), z0, z1), MIN(cons(z0, z1))) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) min(cons(0', nil)) -> 0' min(cons(s(z0), nil)) -> s(z0) min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2))) if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2)) if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2)) replace(z0, z1, nil) -> nil replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3)) if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3) if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3)) sort(nil) -> nil sort(cons(z0, z1)) -> cons(min(cons(z0, z1)), sort(replace(min(cons(z0, z1)), z0, z1))) Types: EQ :: 0':s -> 0':s -> c:c1:c2:c3 0' :: 0':s c :: c:c1:c2:c3 s :: 0':s -> 0':s c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 -> c:c1:c2:c3 LE :: 0':s -> 0':s -> c4:c5:c6 c4 :: c4:c5:c6 c5 :: c4:c5:c6 c6 :: c4:c5:c6 -> c4:c5:c6 MIN :: nil:cons -> c7:c8:c9 cons :: 0':s -> nil:cons -> nil:cons nil :: nil:cons c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c10:c11 -> c4:c5:c6 -> c7:c8:c9 IF_MIN :: true:false -> nil:cons -> c10:c11 le :: 0':s -> 0':s -> true:false true :: true:false c10 :: c7:c8:c9 -> c10:c11 false :: true:false c11 :: c7:c8:c9 -> c10:c11 REPLACE :: 0':s -> 0':s -> nil:cons -> c12:c13 c12 :: c12:c13 c13 :: c14:c15 -> c:c1:c2:c3 -> c12:c13 IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons -> c14:c15 eq :: 0':s -> 0':s -> true:false c14 :: c14:c15 c15 :: c12:c13 -> c14:c15 SORT :: nil:cons -> c16:c17:c18 c16 :: c16:c17:c18 c17 :: c7:c8:c9 -> c16:c17:c18 c18 :: c16:c17:c18 -> c12:c13 -> c7:c8:c9 -> c16:c17:c18 replace :: 0':s -> 0':s -> nil:cons -> nil:cons min :: nil:cons -> 0':s if_min :: true:false -> nil:cons -> 0':s if_replace :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c2:c31_19 :: c:c1:c2:c3 hole_0':s2_19 :: 0':s hole_c4:c5:c63_19 :: c4:c5:c6 hole_c7:c8:c94_19 :: c7:c8:c9 hole_nil:cons5_19 :: nil:cons hole_c10:c116_19 :: c10:c11 hole_true:false7_19 :: true:false hole_c12:c138_19 :: c12:c13 hole_c14:c159_19 :: c14:c15 hole_c16:c17:c1810_19 :: c16:c17:c18 gen_c:c1:c2:c311_19 :: Nat -> c:c1:c2:c3 gen_0':s12_19 :: Nat -> 0':s gen_c4:c5:c613_19 :: Nat -> c4:c5:c6 gen_nil:cons14_19 :: Nat -> nil:cons gen_c16:c17:c1815_19 :: Nat -> c16:c17:c18 Generator Equations: gen_c:c1:c2:c311_19(0) <=> c gen_c:c1:c2:c311_19(+(x, 1)) <=> c3(gen_c:c1:c2:c311_19(x)) gen_0':s12_19(0) <=> 0' gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x)) gen_c4:c5:c613_19(0) <=> c4 gen_c4:c5:c613_19(+(x, 1)) <=> c6(gen_c4:c5:c613_19(x)) gen_nil:cons14_19(0) <=> nil gen_nil:cons14_19(+(x, 1)) <=> cons(0', gen_nil:cons14_19(x)) gen_c16:c17:c1815_19(0) <=> c16 gen_c16:c17:c1815_19(+(x, 1)) <=> c18(gen_c16:c17:c1815_19(x), c12, c7) The following defined symbols remain to be analysed: EQ, LE, MIN, le, REPLACE, eq, SORT, replace, min, sort They will be analysed ascendingly in the following order: EQ < REPLACE LE < MIN le < MIN MIN < SORT le < min eq < REPLACE REPLACE < SORT eq < replace replace < SORT min < SORT replace < sort min < sort ---------------------------------------- (57) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: EQ(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c2:c311_19(n17_19), rt in Omega(1 + n17_19) Induction Base: EQ(gen_0':s12_19(0), gen_0':s12_19(0)) ->_R^Omega(1) c Induction Step: EQ(gen_0':s12_19(+(n17_19, 1)), gen_0':s12_19(+(n17_19, 1))) ->_R^Omega(1) c3(EQ(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19))) ->_IH c3(gen_c:c1:c2:c311_19(c18_19)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (58) Complex Obligation (BEST) ---------------------------------------- (59) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: EQ(0', 0') -> c EQ(0', s(z0)) -> c1 EQ(s(z0), 0') -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) LE(0', z0) -> c4 LE(s(z0), 0') -> c5 LE(s(z0), s(z1)) -> c6(LE(z0, z1)) MIN(cons(0', nil)) -> c7 MIN(cons(s(z0), nil)) -> c8 MIN(cons(z0, cons(z1, z2))) -> c9(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1)) IF_MIN(true, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z0, z2))) IF_MIN(false, cons(z0, cons(z1, z2))) -> c11(MIN(cons(z1, z2))) REPLACE(z0, z1, nil) -> c12 REPLACE(z0, z1, cons(z2, z3)) -> c13(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2)) IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c14 IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c15(REPLACE(z0, z1, z3)) SORT(nil) -> c16 SORT(cons(z0, z1)) -> c17(MIN(cons(z0, z1))) SORT(cons(z0, z1)) -> c18(SORT(replace(min(cons(z0, z1)), z0, z1)), REPLACE(min(cons(z0, z1)), z0, z1), MIN(cons(z0, z1))) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) min(cons(0', nil)) -> 0' min(cons(s(z0), nil)) -> s(z0) min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2))) if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2)) if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2)) replace(z0, z1, nil) -> nil replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3)) if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3) if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3)) sort(nil) -> nil sort(cons(z0, z1)) -> cons(min(cons(z0, z1)), sort(replace(min(cons(z0, z1)), z0, z1))) Types: EQ :: 0':s -> 0':s -> c:c1:c2:c3 0' :: 0':s c :: c:c1:c2:c3 s :: 0':s -> 0':s c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 -> c:c1:c2:c3 LE :: 0':s -> 0':s -> c4:c5:c6 c4 :: c4:c5:c6 c5 :: c4:c5:c6 c6 :: c4:c5:c6 -> c4:c5:c6 MIN :: nil:cons -> c7:c8:c9 cons :: 0':s -> nil:cons -> nil:cons nil :: nil:cons c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c10:c11 -> c4:c5:c6 -> c7:c8:c9 IF_MIN :: true:false -> nil:cons -> c10:c11 le :: 0':s -> 0':s -> true:false true :: true:false c10 :: c7:c8:c9 -> c10:c11 false :: true:false c11 :: c7:c8:c9 -> c10:c11 REPLACE :: 0':s -> 0':s -> nil:cons -> c12:c13 c12 :: c12:c13 c13 :: c14:c15 -> c:c1:c2:c3 -> c12:c13 IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons -> c14:c15 eq :: 0':s -> 0':s -> true:false c14 :: c14:c15 c15 :: c12:c13 -> c14:c15 SORT :: nil:cons -> c16:c17:c18 c16 :: c16:c17:c18 c17 :: c7:c8:c9 -> c16:c17:c18 c18 :: c16:c17:c18 -> c12:c13 -> c7:c8:c9 -> c16:c17:c18 replace :: 0':s -> 0':s -> nil:cons -> nil:cons min :: nil:cons -> 0':s if_min :: true:false -> nil:cons -> 0':s if_replace :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c2:c31_19 :: c:c1:c2:c3 hole_0':s2_19 :: 0':s hole_c4:c5:c63_19 :: c4:c5:c6 hole_c7:c8:c94_19 :: c7:c8:c9 hole_nil:cons5_19 :: nil:cons hole_c10:c116_19 :: c10:c11 hole_true:false7_19 :: true:false hole_c12:c138_19 :: c12:c13 hole_c14:c159_19 :: c14:c15 hole_c16:c17:c1810_19 :: c16:c17:c18 gen_c:c1:c2:c311_19 :: Nat -> c:c1:c2:c3 gen_0':s12_19 :: Nat -> 0':s gen_c4:c5:c613_19 :: Nat -> c4:c5:c6 gen_nil:cons14_19 :: Nat -> nil:cons gen_c16:c17:c1815_19 :: Nat -> c16:c17:c18 Generator Equations: gen_c:c1:c2:c311_19(0) <=> c gen_c:c1:c2:c311_19(+(x, 1)) <=> c3(gen_c:c1:c2:c311_19(x)) gen_0':s12_19(0) <=> 0' gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x)) gen_c4:c5:c613_19(0) <=> c4 gen_c4:c5:c613_19(+(x, 1)) <=> c6(gen_c4:c5:c613_19(x)) gen_nil:cons14_19(0) <=> nil gen_nil:cons14_19(+(x, 1)) <=> cons(0', gen_nil:cons14_19(x)) gen_c16:c17:c1815_19(0) <=> c16 gen_c16:c17:c1815_19(+(x, 1)) <=> c18(gen_c16:c17:c1815_19(x), c12, c7) The following defined symbols remain to be analysed: EQ, LE, MIN, le, REPLACE, eq, SORT, replace, min, sort They will be analysed ascendingly in the following order: EQ < REPLACE LE < MIN le < MIN MIN < SORT le < min eq < REPLACE REPLACE < SORT eq < replace replace < SORT min < SORT replace < sort min < sort ---------------------------------------- (60) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (61) BOUNDS(n^1, INF) ---------------------------------------- (62) Obligation: Innermost TRS: Rules: EQ(0', 0') -> c EQ(0', s(z0)) -> c1 EQ(s(z0), 0') -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) LE(0', z0) -> c4 LE(s(z0), 0') -> c5 LE(s(z0), s(z1)) -> c6(LE(z0, z1)) MIN(cons(0', nil)) -> c7 MIN(cons(s(z0), nil)) -> c8 MIN(cons(z0, cons(z1, z2))) -> c9(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1)) IF_MIN(true, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z0, z2))) IF_MIN(false, cons(z0, cons(z1, z2))) -> c11(MIN(cons(z1, z2))) REPLACE(z0, z1, nil) -> c12 REPLACE(z0, z1, cons(z2, z3)) -> c13(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2)) IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c14 IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c15(REPLACE(z0, z1, z3)) SORT(nil) -> c16 SORT(cons(z0, z1)) -> c17(MIN(cons(z0, z1))) SORT(cons(z0, z1)) -> c18(SORT(replace(min(cons(z0, z1)), z0, z1)), REPLACE(min(cons(z0, z1)), z0, z1), MIN(cons(z0, z1))) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) min(cons(0', nil)) -> 0' min(cons(s(z0), nil)) -> s(z0) min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2))) if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2)) if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2)) replace(z0, z1, nil) -> nil replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3)) if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3) if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3)) sort(nil) -> nil sort(cons(z0, z1)) -> cons(min(cons(z0, z1)), sort(replace(min(cons(z0, z1)), z0, z1))) Types: EQ :: 0':s -> 0':s -> c:c1:c2:c3 0' :: 0':s c :: c:c1:c2:c3 s :: 0':s -> 0':s c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 -> c:c1:c2:c3 LE :: 0':s -> 0':s -> c4:c5:c6 c4 :: c4:c5:c6 c5 :: c4:c5:c6 c6 :: c4:c5:c6 -> c4:c5:c6 MIN :: nil:cons -> c7:c8:c9 cons :: 0':s -> nil:cons -> nil:cons nil :: nil:cons c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c10:c11 -> c4:c5:c6 -> c7:c8:c9 IF_MIN :: true:false -> nil:cons -> c10:c11 le :: 0':s -> 0':s -> true:false true :: true:false c10 :: c7:c8:c9 -> c10:c11 false :: true:false c11 :: c7:c8:c9 -> c10:c11 REPLACE :: 0':s -> 0':s -> nil:cons -> c12:c13 c12 :: c12:c13 c13 :: c14:c15 -> c:c1:c2:c3 -> c12:c13 IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons -> c14:c15 eq :: 0':s -> 0':s -> true:false c14 :: c14:c15 c15 :: c12:c13 -> c14:c15 SORT :: nil:cons -> c16:c17:c18 c16 :: c16:c17:c18 c17 :: c7:c8:c9 -> c16:c17:c18 c18 :: c16:c17:c18 -> c12:c13 -> c7:c8:c9 -> c16:c17:c18 replace :: 0':s -> 0':s -> nil:cons -> nil:cons min :: nil:cons -> 0':s if_min :: true:false -> nil:cons -> 0':s if_replace :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c2:c31_19 :: c:c1:c2:c3 hole_0':s2_19 :: 0':s hole_c4:c5:c63_19 :: c4:c5:c6 hole_c7:c8:c94_19 :: c7:c8:c9 hole_nil:cons5_19 :: nil:cons hole_c10:c116_19 :: c10:c11 hole_true:false7_19 :: true:false hole_c12:c138_19 :: c12:c13 hole_c14:c159_19 :: c14:c15 hole_c16:c17:c1810_19 :: c16:c17:c18 gen_c:c1:c2:c311_19 :: Nat -> c:c1:c2:c3 gen_0':s12_19 :: Nat -> 0':s gen_c4:c5:c613_19 :: Nat -> c4:c5:c6 gen_nil:cons14_19 :: Nat -> nil:cons gen_c16:c17:c1815_19 :: Nat -> c16:c17:c18 Lemmas: EQ(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c2:c311_19(n17_19), rt in Omega(1 + n17_19) Generator Equations: gen_c:c1:c2:c311_19(0) <=> c gen_c:c1:c2:c311_19(+(x, 1)) <=> c3(gen_c:c1:c2:c311_19(x)) gen_0':s12_19(0) <=> 0' gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x)) gen_c4:c5:c613_19(0) <=> c4 gen_c4:c5:c613_19(+(x, 1)) <=> c6(gen_c4:c5:c613_19(x)) gen_nil:cons14_19(0) <=> nil gen_nil:cons14_19(+(x, 1)) <=> cons(0', gen_nil:cons14_19(x)) gen_c16:c17:c1815_19(0) <=> c16 gen_c16:c17:c1815_19(+(x, 1)) <=> c18(gen_c16:c17:c1815_19(x), c12, c7) The following defined symbols remain to be analysed: LE, MIN, le, REPLACE, eq, SORT, replace, min, sort They will be analysed ascendingly in the following order: LE < MIN le < MIN MIN < SORT le < min eq < REPLACE REPLACE < SORT eq < replace replace < SORT min < SORT replace < sort min < sort ---------------------------------------- (63) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: LE(gen_0':s12_19(n1023_19), gen_0':s12_19(n1023_19)) -> gen_c4:c5:c613_19(n1023_19), rt in Omega(1 + n1023_19) Induction Base: LE(gen_0':s12_19(0), gen_0':s12_19(0)) ->_R^Omega(1) c4 Induction Step: LE(gen_0':s12_19(+(n1023_19, 1)), gen_0':s12_19(+(n1023_19, 1))) ->_R^Omega(1) c6(LE(gen_0':s12_19(n1023_19), gen_0':s12_19(n1023_19))) ->_IH c6(gen_c4:c5:c613_19(c1024_19)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (64) Obligation: Innermost TRS: Rules: EQ(0', 0') -> c EQ(0', s(z0)) -> c1 EQ(s(z0), 0') -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) LE(0', z0) -> c4 LE(s(z0), 0') -> c5 LE(s(z0), s(z1)) -> c6(LE(z0, z1)) MIN(cons(0', nil)) -> c7 MIN(cons(s(z0), nil)) -> c8 MIN(cons(z0, cons(z1, z2))) -> c9(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1)) IF_MIN(true, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z0, z2))) IF_MIN(false, cons(z0, cons(z1, z2))) -> c11(MIN(cons(z1, z2))) REPLACE(z0, z1, nil) -> c12 REPLACE(z0, z1, cons(z2, z3)) -> c13(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2)) IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c14 IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c15(REPLACE(z0, z1, z3)) SORT(nil) -> c16 SORT(cons(z0, z1)) -> c17(MIN(cons(z0, z1))) SORT(cons(z0, z1)) -> c18(SORT(replace(min(cons(z0, z1)), z0, z1)), REPLACE(min(cons(z0, z1)), z0, z1), MIN(cons(z0, z1))) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) min(cons(0', nil)) -> 0' min(cons(s(z0), nil)) -> s(z0) min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2))) if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2)) if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2)) replace(z0, z1, nil) -> nil replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3)) if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3) if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3)) sort(nil) -> nil sort(cons(z0, z1)) -> cons(min(cons(z0, z1)), sort(replace(min(cons(z0, z1)), z0, z1))) Types: EQ :: 0':s -> 0':s -> c:c1:c2:c3 0' :: 0':s c :: c:c1:c2:c3 s :: 0':s -> 0':s c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 -> c:c1:c2:c3 LE :: 0':s -> 0':s -> c4:c5:c6 c4 :: c4:c5:c6 c5 :: c4:c5:c6 c6 :: c4:c5:c6 -> c4:c5:c6 MIN :: nil:cons -> c7:c8:c9 cons :: 0':s -> nil:cons -> nil:cons nil :: nil:cons c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c10:c11 -> c4:c5:c6 -> c7:c8:c9 IF_MIN :: true:false -> nil:cons -> c10:c11 le :: 0':s -> 0':s -> true:false true :: true:false c10 :: c7:c8:c9 -> c10:c11 false :: true:false c11 :: c7:c8:c9 -> c10:c11 REPLACE :: 0':s -> 0':s -> nil:cons -> c12:c13 c12 :: c12:c13 c13 :: c14:c15 -> c:c1:c2:c3 -> c12:c13 IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons -> c14:c15 eq :: 0':s -> 0':s -> true:false c14 :: c14:c15 c15 :: c12:c13 -> c14:c15 SORT :: nil:cons -> c16:c17:c18 c16 :: c16:c17:c18 c17 :: c7:c8:c9 -> c16:c17:c18 c18 :: c16:c17:c18 -> c12:c13 -> c7:c8:c9 -> c16:c17:c18 replace :: 0':s -> 0':s -> nil:cons -> nil:cons min :: nil:cons -> 0':s if_min :: true:false -> nil:cons -> 0':s if_replace :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c2:c31_19 :: c:c1:c2:c3 hole_0':s2_19 :: 0':s hole_c4:c5:c63_19 :: c4:c5:c6 hole_c7:c8:c94_19 :: c7:c8:c9 hole_nil:cons5_19 :: nil:cons hole_c10:c116_19 :: c10:c11 hole_true:false7_19 :: true:false hole_c12:c138_19 :: c12:c13 hole_c14:c159_19 :: c14:c15 hole_c16:c17:c1810_19 :: c16:c17:c18 gen_c:c1:c2:c311_19 :: Nat -> c:c1:c2:c3 gen_0':s12_19 :: Nat -> 0':s gen_c4:c5:c613_19 :: Nat -> c4:c5:c6 gen_nil:cons14_19 :: Nat -> nil:cons gen_c16:c17:c1815_19 :: Nat -> c16:c17:c18 Lemmas: EQ(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c2:c311_19(n17_19), rt in Omega(1 + n17_19) LE(gen_0':s12_19(n1023_19), gen_0':s12_19(n1023_19)) -> gen_c4:c5:c613_19(n1023_19), rt in Omega(1 + n1023_19) Generator Equations: gen_c:c1:c2:c311_19(0) <=> c gen_c:c1:c2:c311_19(+(x, 1)) <=> c3(gen_c:c1:c2:c311_19(x)) gen_0':s12_19(0) <=> 0' gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x)) gen_c4:c5:c613_19(0) <=> c4 gen_c4:c5:c613_19(+(x, 1)) <=> c6(gen_c4:c5:c613_19(x)) gen_nil:cons14_19(0) <=> nil gen_nil:cons14_19(+(x, 1)) <=> cons(0', gen_nil:cons14_19(x)) gen_c16:c17:c1815_19(0) <=> c16 gen_c16:c17:c1815_19(+(x, 1)) <=> c18(gen_c16:c17:c1815_19(x), c12, c7) The following defined symbols remain to be analysed: le, MIN, REPLACE, eq, SORT, replace, min, sort They will be analysed ascendingly in the following order: le < MIN MIN < SORT le < min eq < REPLACE REPLACE < SORT eq < replace replace < SORT min < SORT replace < sort min < sort ---------------------------------------- (65) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: le(gen_0':s12_19(n1803_19), gen_0':s12_19(n1803_19)) -> true, rt in Omega(0) Induction Base: le(gen_0':s12_19(0), gen_0':s12_19(0)) ->_R^Omega(0) true Induction Step: le(gen_0':s12_19(+(n1803_19, 1)), gen_0':s12_19(+(n1803_19, 1))) ->_R^Omega(0) le(gen_0':s12_19(n1803_19), gen_0':s12_19(n1803_19)) ->_IH true We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (66) Obligation: Innermost TRS: Rules: EQ(0', 0') -> c EQ(0', s(z0)) -> c1 EQ(s(z0), 0') -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) LE(0', z0) -> c4 LE(s(z0), 0') -> c5 LE(s(z0), s(z1)) -> c6(LE(z0, z1)) MIN(cons(0', nil)) -> c7 MIN(cons(s(z0), nil)) -> c8 MIN(cons(z0, cons(z1, z2))) -> c9(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1)) IF_MIN(true, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z0, z2))) IF_MIN(false, cons(z0, cons(z1, z2))) -> c11(MIN(cons(z1, z2))) REPLACE(z0, z1, nil) -> c12 REPLACE(z0, z1, cons(z2, z3)) -> c13(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2)) IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c14 IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c15(REPLACE(z0, z1, z3)) SORT(nil) -> c16 SORT(cons(z0, z1)) -> c17(MIN(cons(z0, z1))) SORT(cons(z0, z1)) -> c18(SORT(replace(min(cons(z0, z1)), z0, z1)), REPLACE(min(cons(z0, z1)), z0, z1), MIN(cons(z0, z1))) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) min(cons(0', nil)) -> 0' min(cons(s(z0), nil)) -> s(z0) min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2))) if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2)) if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2)) replace(z0, z1, nil) -> nil replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3)) if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3) if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3)) sort(nil) -> nil sort(cons(z0, z1)) -> cons(min(cons(z0, z1)), sort(replace(min(cons(z0, z1)), z0, z1))) Types: EQ :: 0':s -> 0':s -> c:c1:c2:c3 0' :: 0':s c :: c:c1:c2:c3 s :: 0':s -> 0':s c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 -> c:c1:c2:c3 LE :: 0':s -> 0':s -> c4:c5:c6 c4 :: c4:c5:c6 c5 :: c4:c5:c6 c6 :: c4:c5:c6 -> c4:c5:c6 MIN :: nil:cons -> c7:c8:c9 cons :: 0':s -> nil:cons -> nil:cons nil :: nil:cons c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c10:c11 -> c4:c5:c6 -> c7:c8:c9 IF_MIN :: true:false -> nil:cons -> c10:c11 le :: 0':s -> 0':s -> true:false true :: true:false c10 :: c7:c8:c9 -> c10:c11 false :: true:false c11 :: c7:c8:c9 -> c10:c11 REPLACE :: 0':s -> 0':s -> nil:cons -> c12:c13 c12 :: c12:c13 c13 :: c14:c15 -> c:c1:c2:c3 -> c12:c13 IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons -> c14:c15 eq :: 0':s -> 0':s -> true:false c14 :: c14:c15 c15 :: c12:c13 -> c14:c15 SORT :: nil:cons -> c16:c17:c18 c16 :: c16:c17:c18 c17 :: c7:c8:c9 -> c16:c17:c18 c18 :: c16:c17:c18 -> c12:c13 -> c7:c8:c9 -> c16:c17:c18 replace :: 0':s -> 0':s -> nil:cons -> nil:cons min :: nil:cons -> 0':s if_min :: true:false -> nil:cons -> 0':s if_replace :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c2:c31_19 :: c:c1:c2:c3 hole_0':s2_19 :: 0':s hole_c4:c5:c63_19 :: c4:c5:c6 hole_c7:c8:c94_19 :: c7:c8:c9 hole_nil:cons5_19 :: nil:cons hole_c10:c116_19 :: c10:c11 hole_true:false7_19 :: true:false hole_c12:c138_19 :: c12:c13 hole_c14:c159_19 :: c14:c15 hole_c16:c17:c1810_19 :: c16:c17:c18 gen_c:c1:c2:c311_19 :: Nat -> c:c1:c2:c3 gen_0':s12_19 :: Nat -> 0':s gen_c4:c5:c613_19 :: Nat -> c4:c5:c6 gen_nil:cons14_19 :: Nat -> nil:cons gen_c16:c17:c1815_19 :: Nat -> c16:c17:c18 Lemmas: EQ(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c2:c311_19(n17_19), rt in Omega(1 + n17_19) LE(gen_0':s12_19(n1023_19), gen_0':s12_19(n1023_19)) -> gen_c4:c5:c613_19(n1023_19), rt in Omega(1 + n1023_19) le(gen_0':s12_19(n1803_19), gen_0':s12_19(n1803_19)) -> true, rt in Omega(0) Generator Equations: gen_c:c1:c2:c311_19(0) <=> c gen_c:c1:c2:c311_19(+(x, 1)) <=> c3(gen_c:c1:c2:c311_19(x)) gen_0':s12_19(0) <=> 0' gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x)) gen_c4:c5:c613_19(0) <=> c4 gen_c4:c5:c613_19(+(x, 1)) <=> c6(gen_c4:c5:c613_19(x)) gen_nil:cons14_19(0) <=> nil gen_nil:cons14_19(+(x, 1)) <=> cons(0', gen_nil:cons14_19(x)) gen_c16:c17:c1815_19(0) <=> c16 gen_c16:c17:c1815_19(+(x, 1)) <=> c18(gen_c16:c17:c1815_19(x), c12, c7) The following defined symbols remain to be analysed: MIN, REPLACE, eq, SORT, replace, min, sort They will be analysed ascendingly in the following order: MIN < SORT eq < REPLACE REPLACE < SORT eq < replace replace < SORT min < SORT replace < sort min < sort ---------------------------------------- (67) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: MIN(gen_nil:cons14_19(+(1, n2270_19))) -> *16_19, rt in Omega(n2270_19) Induction Base: MIN(gen_nil:cons14_19(+(1, 0))) Induction Step: MIN(gen_nil:cons14_19(+(1, +(n2270_19, 1)))) ->_R^Omega(1) c9(IF_MIN(le(0', 0'), cons(0', cons(0', gen_nil:cons14_19(n2270_19)))), LE(0', 0')) ->_L^Omega(0) c9(IF_MIN(true, cons(0', cons(0', gen_nil:cons14_19(n2270_19)))), LE(0', 0')) ->_R^Omega(1) c9(c10(MIN(cons(0', gen_nil:cons14_19(n2270_19)))), LE(0', 0')) ->_IH c9(c10(*16_19), LE(0', 0')) ->_L^Omega(1) c9(c10(*16_19), gen_c4:c5:c613_19(0)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (68) Obligation: Innermost TRS: Rules: EQ(0', 0') -> c EQ(0', s(z0)) -> c1 EQ(s(z0), 0') -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) LE(0', z0) -> c4 LE(s(z0), 0') -> c5 LE(s(z0), s(z1)) -> c6(LE(z0, z1)) MIN(cons(0', nil)) -> c7 MIN(cons(s(z0), nil)) -> c8 MIN(cons(z0, cons(z1, z2))) -> c9(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1)) IF_MIN(true, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z0, z2))) IF_MIN(false, cons(z0, cons(z1, z2))) -> c11(MIN(cons(z1, z2))) REPLACE(z0, z1, nil) -> c12 REPLACE(z0, z1, cons(z2, z3)) -> c13(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2)) IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c14 IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c15(REPLACE(z0, z1, z3)) SORT(nil) -> c16 SORT(cons(z0, z1)) -> c17(MIN(cons(z0, z1))) SORT(cons(z0, z1)) -> c18(SORT(replace(min(cons(z0, z1)), z0, z1)), REPLACE(min(cons(z0, z1)), z0, z1), MIN(cons(z0, z1))) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) min(cons(0', nil)) -> 0' min(cons(s(z0), nil)) -> s(z0) min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2))) if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2)) if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2)) replace(z0, z1, nil) -> nil replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3)) if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3) if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3)) sort(nil) -> nil sort(cons(z0, z1)) -> cons(min(cons(z0, z1)), sort(replace(min(cons(z0, z1)), z0, z1))) Types: EQ :: 0':s -> 0':s -> c:c1:c2:c3 0' :: 0':s c :: c:c1:c2:c3 s :: 0':s -> 0':s c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 -> c:c1:c2:c3 LE :: 0':s -> 0':s -> c4:c5:c6 c4 :: c4:c5:c6 c5 :: c4:c5:c6 c6 :: c4:c5:c6 -> c4:c5:c6 MIN :: nil:cons -> c7:c8:c9 cons :: 0':s -> nil:cons -> nil:cons nil :: nil:cons c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c10:c11 -> c4:c5:c6 -> c7:c8:c9 IF_MIN :: true:false -> nil:cons -> c10:c11 le :: 0':s -> 0':s -> true:false true :: true:false c10 :: c7:c8:c9 -> c10:c11 false :: true:false c11 :: c7:c8:c9 -> c10:c11 REPLACE :: 0':s -> 0':s -> nil:cons -> c12:c13 c12 :: c12:c13 c13 :: c14:c15 -> c:c1:c2:c3 -> c12:c13 IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons -> c14:c15 eq :: 0':s -> 0':s -> true:false c14 :: c14:c15 c15 :: c12:c13 -> c14:c15 SORT :: nil:cons -> c16:c17:c18 c16 :: c16:c17:c18 c17 :: c7:c8:c9 -> c16:c17:c18 c18 :: c16:c17:c18 -> c12:c13 -> c7:c8:c9 -> c16:c17:c18 replace :: 0':s -> 0':s -> nil:cons -> nil:cons min :: nil:cons -> 0':s if_min :: true:false -> nil:cons -> 0':s if_replace :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c2:c31_19 :: c:c1:c2:c3 hole_0':s2_19 :: 0':s hole_c4:c5:c63_19 :: c4:c5:c6 hole_c7:c8:c94_19 :: c7:c8:c9 hole_nil:cons5_19 :: nil:cons hole_c10:c116_19 :: c10:c11 hole_true:false7_19 :: true:false hole_c12:c138_19 :: c12:c13 hole_c14:c159_19 :: c14:c15 hole_c16:c17:c1810_19 :: c16:c17:c18 gen_c:c1:c2:c311_19 :: Nat -> c:c1:c2:c3 gen_0':s12_19 :: Nat -> 0':s gen_c4:c5:c613_19 :: Nat -> c4:c5:c6 gen_nil:cons14_19 :: Nat -> nil:cons gen_c16:c17:c1815_19 :: Nat -> c16:c17:c18 Lemmas: EQ(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c2:c311_19(n17_19), rt in Omega(1 + n17_19) LE(gen_0':s12_19(n1023_19), gen_0':s12_19(n1023_19)) -> gen_c4:c5:c613_19(n1023_19), rt in Omega(1 + n1023_19) le(gen_0':s12_19(n1803_19), gen_0':s12_19(n1803_19)) -> true, rt in Omega(0) MIN(gen_nil:cons14_19(+(1, n2270_19))) -> *16_19, rt in Omega(n2270_19) Generator Equations: gen_c:c1:c2:c311_19(0) <=> c gen_c:c1:c2:c311_19(+(x, 1)) <=> c3(gen_c:c1:c2:c311_19(x)) gen_0':s12_19(0) <=> 0' gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x)) gen_c4:c5:c613_19(0) <=> c4 gen_c4:c5:c613_19(+(x, 1)) <=> c6(gen_c4:c5:c613_19(x)) gen_nil:cons14_19(0) <=> nil gen_nil:cons14_19(+(x, 1)) <=> cons(0', gen_nil:cons14_19(x)) gen_c16:c17:c1815_19(0) <=> c16 gen_c16:c17:c1815_19(+(x, 1)) <=> c18(gen_c16:c17:c1815_19(x), c12, c7) The following defined symbols remain to be analysed: eq, REPLACE, SORT, replace, min, sort They will be analysed ascendingly in the following order: eq < REPLACE REPLACE < SORT eq < replace replace < SORT min < SORT replace < sort min < sort ---------------------------------------- (69) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: eq(gen_0':s12_19(n7487_19), gen_0':s12_19(n7487_19)) -> true, rt in Omega(0) Induction Base: eq(gen_0':s12_19(0), gen_0':s12_19(0)) ->_R^Omega(0) true Induction Step: eq(gen_0':s12_19(+(n7487_19, 1)), gen_0':s12_19(+(n7487_19, 1))) ->_R^Omega(0) eq(gen_0':s12_19(n7487_19), gen_0':s12_19(n7487_19)) ->_IH true We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (70) Obligation: Innermost TRS: Rules: EQ(0', 0') -> c EQ(0', s(z0)) -> c1 EQ(s(z0), 0') -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) LE(0', z0) -> c4 LE(s(z0), 0') -> c5 LE(s(z0), s(z1)) -> c6(LE(z0, z1)) MIN(cons(0', nil)) -> c7 MIN(cons(s(z0), nil)) -> c8 MIN(cons(z0, cons(z1, z2))) -> c9(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1)) IF_MIN(true, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z0, z2))) IF_MIN(false, cons(z0, cons(z1, z2))) -> c11(MIN(cons(z1, z2))) REPLACE(z0, z1, nil) -> c12 REPLACE(z0, z1, cons(z2, z3)) -> c13(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2)) IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c14 IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c15(REPLACE(z0, z1, z3)) SORT(nil) -> c16 SORT(cons(z0, z1)) -> c17(MIN(cons(z0, z1))) SORT(cons(z0, z1)) -> c18(SORT(replace(min(cons(z0, z1)), z0, z1)), REPLACE(min(cons(z0, z1)), z0, z1), MIN(cons(z0, z1))) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) min(cons(0', nil)) -> 0' min(cons(s(z0), nil)) -> s(z0) min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2))) if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2)) if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2)) replace(z0, z1, nil) -> nil replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3)) if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3) if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3)) sort(nil) -> nil sort(cons(z0, z1)) -> cons(min(cons(z0, z1)), sort(replace(min(cons(z0, z1)), z0, z1))) Types: EQ :: 0':s -> 0':s -> c:c1:c2:c3 0' :: 0':s c :: c:c1:c2:c3 s :: 0':s -> 0':s c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 -> c:c1:c2:c3 LE :: 0':s -> 0':s -> c4:c5:c6 c4 :: c4:c5:c6 c5 :: c4:c5:c6 c6 :: c4:c5:c6 -> c4:c5:c6 MIN :: nil:cons -> c7:c8:c9 cons :: 0':s -> nil:cons -> nil:cons nil :: nil:cons c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c10:c11 -> c4:c5:c6 -> c7:c8:c9 IF_MIN :: true:false -> nil:cons -> c10:c11 le :: 0':s -> 0':s -> true:false true :: true:false c10 :: c7:c8:c9 -> c10:c11 false :: true:false c11 :: c7:c8:c9 -> c10:c11 REPLACE :: 0':s -> 0':s -> nil:cons -> c12:c13 c12 :: c12:c13 c13 :: c14:c15 -> c:c1:c2:c3 -> c12:c13 IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons -> c14:c15 eq :: 0':s -> 0':s -> true:false c14 :: c14:c15 c15 :: c12:c13 -> c14:c15 SORT :: nil:cons -> c16:c17:c18 c16 :: c16:c17:c18 c17 :: c7:c8:c9 -> c16:c17:c18 c18 :: c16:c17:c18 -> c12:c13 -> c7:c8:c9 -> c16:c17:c18 replace :: 0':s -> 0':s -> nil:cons -> nil:cons min :: nil:cons -> 0':s if_min :: true:false -> nil:cons -> 0':s if_replace :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c2:c31_19 :: c:c1:c2:c3 hole_0':s2_19 :: 0':s hole_c4:c5:c63_19 :: c4:c5:c6 hole_c7:c8:c94_19 :: c7:c8:c9 hole_nil:cons5_19 :: nil:cons hole_c10:c116_19 :: c10:c11 hole_true:false7_19 :: true:false hole_c12:c138_19 :: c12:c13 hole_c14:c159_19 :: c14:c15 hole_c16:c17:c1810_19 :: c16:c17:c18 gen_c:c1:c2:c311_19 :: Nat -> c:c1:c2:c3 gen_0':s12_19 :: Nat -> 0':s gen_c4:c5:c613_19 :: Nat -> c4:c5:c6 gen_nil:cons14_19 :: Nat -> nil:cons gen_c16:c17:c1815_19 :: Nat -> c16:c17:c18 Lemmas: EQ(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c2:c311_19(n17_19), rt in Omega(1 + n17_19) LE(gen_0':s12_19(n1023_19), gen_0':s12_19(n1023_19)) -> gen_c4:c5:c613_19(n1023_19), rt in Omega(1 + n1023_19) le(gen_0':s12_19(n1803_19), gen_0':s12_19(n1803_19)) -> true, rt in Omega(0) MIN(gen_nil:cons14_19(+(1, n2270_19))) -> *16_19, rt in Omega(n2270_19) eq(gen_0':s12_19(n7487_19), gen_0':s12_19(n7487_19)) -> true, rt in Omega(0) Generator Equations: gen_c:c1:c2:c311_19(0) <=> c gen_c:c1:c2:c311_19(+(x, 1)) <=> c3(gen_c:c1:c2:c311_19(x)) gen_0':s12_19(0) <=> 0' gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x)) gen_c4:c5:c613_19(0) <=> c4 gen_c4:c5:c613_19(+(x, 1)) <=> c6(gen_c4:c5:c613_19(x)) gen_nil:cons14_19(0) <=> nil gen_nil:cons14_19(+(x, 1)) <=> cons(0', gen_nil:cons14_19(x)) gen_c16:c17:c1815_19(0) <=> c16 gen_c16:c17:c1815_19(+(x, 1)) <=> c18(gen_c16:c17:c1815_19(x), c12, c7) The following defined symbols remain to be analysed: REPLACE, SORT, replace, min, sort They will be analysed ascendingly in the following order: REPLACE < SORT replace < SORT min < SORT replace < sort min < sort ---------------------------------------- (71) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: min(gen_nil:cons14_19(+(1, n9513_19))) -> gen_0':s12_19(0), rt in Omega(0) Induction Base: min(gen_nil:cons14_19(+(1, 0))) ->_R^Omega(0) 0' Induction Step: min(gen_nil:cons14_19(+(1, +(n9513_19, 1)))) ->_R^Omega(0) if_min(le(0', 0'), cons(0', cons(0', gen_nil:cons14_19(n9513_19)))) ->_L^Omega(0) if_min(true, cons(0', cons(0', gen_nil:cons14_19(n9513_19)))) ->_R^Omega(0) min(cons(0', gen_nil:cons14_19(n9513_19))) ->_IH gen_0':s12_19(0) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (72) Obligation: Innermost TRS: Rules: EQ(0', 0') -> c EQ(0', s(z0)) -> c1 EQ(s(z0), 0') -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) LE(0', z0) -> c4 LE(s(z0), 0') -> c5 LE(s(z0), s(z1)) -> c6(LE(z0, z1)) MIN(cons(0', nil)) -> c7 MIN(cons(s(z0), nil)) -> c8 MIN(cons(z0, cons(z1, z2))) -> c9(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1)) IF_MIN(true, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z0, z2))) IF_MIN(false, cons(z0, cons(z1, z2))) -> c11(MIN(cons(z1, z2))) REPLACE(z0, z1, nil) -> c12 REPLACE(z0, z1, cons(z2, z3)) -> c13(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2)) IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c14 IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c15(REPLACE(z0, z1, z3)) SORT(nil) -> c16 SORT(cons(z0, z1)) -> c17(MIN(cons(z0, z1))) SORT(cons(z0, z1)) -> c18(SORT(replace(min(cons(z0, z1)), z0, z1)), REPLACE(min(cons(z0, z1)), z0, z1), MIN(cons(z0, z1))) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) min(cons(0', nil)) -> 0' min(cons(s(z0), nil)) -> s(z0) min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2))) if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2)) if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2)) replace(z0, z1, nil) -> nil replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3)) if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3) if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3)) sort(nil) -> nil sort(cons(z0, z1)) -> cons(min(cons(z0, z1)), sort(replace(min(cons(z0, z1)), z0, z1))) Types: EQ :: 0':s -> 0':s -> c:c1:c2:c3 0' :: 0':s c :: c:c1:c2:c3 s :: 0':s -> 0':s c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 -> c:c1:c2:c3 LE :: 0':s -> 0':s -> c4:c5:c6 c4 :: c4:c5:c6 c5 :: c4:c5:c6 c6 :: c4:c5:c6 -> c4:c5:c6 MIN :: nil:cons -> c7:c8:c9 cons :: 0':s -> nil:cons -> nil:cons nil :: nil:cons c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c10:c11 -> c4:c5:c6 -> c7:c8:c9 IF_MIN :: true:false -> nil:cons -> c10:c11 le :: 0':s -> 0':s -> true:false true :: true:false c10 :: c7:c8:c9 -> c10:c11 false :: true:false c11 :: c7:c8:c9 -> c10:c11 REPLACE :: 0':s -> 0':s -> nil:cons -> c12:c13 c12 :: c12:c13 c13 :: c14:c15 -> c:c1:c2:c3 -> c12:c13 IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons -> c14:c15 eq :: 0':s -> 0':s -> true:false c14 :: c14:c15 c15 :: c12:c13 -> c14:c15 SORT :: nil:cons -> c16:c17:c18 c16 :: c16:c17:c18 c17 :: c7:c8:c9 -> c16:c17:c18 c18 :: c16:c17:c18 -> c12:c13 -> c7:c8:c9 -> c16:c17:c18 replace :: 0':s -> 0':s -> nil:cons -> nil:cons min :: nil:cons -> 0':s if_min :: true:false -> nil:cons -> 0':s if_replace :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c2:c31_19 :: c:c1:c2:c3 hole_0':s2_19 :: 0':s hole_c4:c5:c63_19 :: c4:c5:c6 hole_c7:c8:c94_19 :: c7:c8:c9 hole_nil:cons5_19 :: nil:cons hole_c10:c116_19 :: c10:c11 hole_true:false7_19 :: true:false hole_c12:c138_19 :: c12:c13 hole_c14:c159_19 :: c14:c15 hole_c16:c17:c1810_19 :: c16:c17:c18 gen_c:c1:c2:c311_19 :: Nat -> c:c1:c2:c3 gen_0':s12_19 :: Nat -> 0':s gen_c4:c5:c613_19 :: Nat -> c4:c5:c6 gen_nil:cons14_19 :: Nat -> nil:cons gen_c16:c17:c1815_19 :: Nat -> c16:c17:c18 Lemmas: EQ(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c2:c311_19(n17_19), rt in Omega(1 + n17_19) LE(gen_0':s12_19(n1023_19), gen_0':s12_19(n1023_19)) -> gen_c4:c5:c613_19(n1023_19), rt in Omega(1 + n1023_19) le(gen_0':s12_19(n1803_19), gen_0':s12_19(n1803_19)) -> true, rt in Omega(0) MIN(gen_nil:cons14_19(+(1, n2270_19))) -> *16_19, rt in Omega(n2270_19) eq(gen_0':s12_19(n7487_19), gen_0':s12_19(n7487_19)) -> true, rt in Omega(0) min(gen_nil:cons14_19(+(1, n9513_19))) -> gen_0':s12_19(0), rt in Omega(0) Generator Equations: gen_c:c1:c2:c311_19(0) <=> c gen_c:c1:c2:c311_19(+(x, 1)) <=> c3(gen_c:c1:c2:c311_19(x)) gen_0':s12_19(0) <=> 0' gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x)) gen_c4:c5:c613_19(0) <=> c4 gen_c4:c5:c613_19(+(x, 1)) <=> c6(gen_c4:c5:c613_19(x)) gen_nil:cons14_19(0) <=> nil gen_nil:cons14_19(+(x, 1)) <=> cons(0', gen_nil:cons14_19(x)) gen_c16:c17:c1815_19(0) <=> c16 gen_c16:c17:c1815_19(+(x, 1)) <=> c18(gen_c16:c17:c1815_19(x), c12, c7) The following defined symbols remain to be analysed: SORT, sort ---------------------------------------- (73) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: SORT(gen_nil:cons14_19(+(1, n10367_19))) -> *16_19, rt in Omega(n10367_19 + n10367_19^2) Induction Base: SORT(gen_nil:cons14_19(+(1, 0))) Induction Step: SORT(gen_nil:cons14_19(+(1, +(n10367_19, 1)))) ->_R^Omega(1) c18(SORT(replace(min(cons(0', gen_nil:cons14_19(+(1, n10367_19)))), 0', gen_nil:cons14_19(+(1, n10367_19)))), REPLACE(min(cons(0', gen_nil:cons14_19(+(1, n10367_19)))), 0', gen_nil:cons14_19(+(1, n10367_19))), MIN(cons(0', gen_nil:cons14_19(+(1, n10367_19))))) ->_L^Omega(0) c18(SORT(replace(gen_0':s12_19(0), 0', gen_nil:cons14_19(+(1, n10367_19)))), REPLACE(min(cons(0', gen_nil:cons14_19(+(1, n10367_19)))), 0', gen_nil:cons14_19(+(1, n10367_19))), MIN(cons(0', gen_nil:cons14_19(+(1, n10367_19))))) ->_R^Omega(0) c18(SORT(if_replace(eq(gen_0':s12_19(0), 0'), gen_0':s12_19(0), 0', cons(0', gen_nil:cons14_19(n10367_19)))), REPLACE(min(cons(0', gen_nil:cons14_19(+(1, n10367_19)))), 0', gen_nil:cons14_19(+(1, n10367_19))), MIN(cons(0', gen_nil:cons14_19(+(1, n10367_19))))) ->_L^Omega(0) c18(SORT(if_replace(true, gen_0':s12_19(0), 0', cons(0', gen_nil:cons14_19(n10367_19)))), REPLACE(min(cons(0', gen_nil:cons14_19(+(1, n10367_19)))), 0', gen_nil:cons14_19(+(1, n10367_19))), MIN(cons(0', gen_nil:cons14_19(+(1, n10367_19))))) ->_R^Omega(0) c18(SORT(cons(0', gen_nil:cons14_19(n10367_19))), REPLACE(min(cons(0', gen_nil:cons14_19(+(1, n10367_19)))), 0', gen_nil:cons14_19(+(1, n10367_19))), MIN(cons(0', gen_nil:cons14_19(+(1, n10367_19))))) ->_IH c18(*16_19, REPLACE(min(cons(0', gen_nil:cons14_19(+(1, n10367_19)))), 0', gen_nil:cons14_19(+(1, n10367_19))), MIN(cons(0', gen_nil:cons14_19(+(1, n10367_19))))) ->_L^Omega(0) c18(*16_19, REPLACE(gen_0':s12_19(0), 0', gen_nil:cons14_19(+(1, n10367_19))), MIN(cons(0', gen_nil:cons14_19(+(1, n10367_19))))) ->_R^Omega(1) c18(*16_19, c13(IF_REPLACE(eq(gen_0':s12_19(0), 0'), gen_0':s12_19(0), 0', cons(0', gen_nil:cons14_19(n10367_19))), EQ(gen_0':s12_19(0), 0')), MIN(cons(0', gen_nil:cons14_19(+(1, n10367_19))))) ->_L^Omega(0) c18(*16_19, c13(IF_REPLACE(true, gen_0':s12_19(0), 0', cons(0', gen_nil:cons14_19(n10367_19))), EQ(gen_0':s12_19(0), 0')), MIN(cons(0', gen_nil:cons14_19(+(1, n10367_19))))) ->_R^Omega(1) c18(*16_19, c13(c14, EQ(gen_0':s12_19(0), 0')), MIN(cons(0', gen_nil:cons14_19(+(1, n10367_19))))) ->_L^Omega(1) c18(*16_19, c13(c14, gen_c:c1:c2:c311_19(0)), MIN(cons(0', gen_nil:cons14_19(+(1, n10367_19))))) ->_R^Omega(1) c18(*16_19, c13(c14, gen_c:c1:c2:c311_19(0)), c9(IF_MIN(le(0', 0'), cons(0', cons(0', gen_nil:cons14_19(n10367_19)))), LE(0', 0'))) ->_L^Omega(0) c18(*16_19, c13(c14, gen_c:c1:c2:c311_19(0)), c9(IF_MIN(true, cons(0', cons(0', gen_nil:cons14_19(n10367_19)))), LE(0', 0'))) ->_R^Omega(1) c18(*16_19, c13(c14, gen_c:c1:c2:c311_19(0)), c9(c10(MIN(cons(0', gen_nil:cons14_19(n10367_19)))), LE(0', 0'))) ->_L^Omega(n10367_19) c18(*16_19, c13(c14, gen_c:c1:c2:c311_19(0)), c9(c10(*16_19), LE(0', 0'))) ->_L^Omega(1) c18(*16_19, c13(c14, gen_c:c1:c2:c311_19(0)), c9(c10(*16_19), gen_c4:c5:c613_19(0))) We have rt in Omega(n^2) and sz in O(n). Thus, we have irc_R in Omega(n^2). ---------------------------------------- (74) Complex Obligation (BEST) ---------------------------------------- (75) Obligation: Proved the lower bound n^2 for the following obligation: Innermost TRS: Rules: EQ(0', 0') -> c EQ(0', s(z0)) -> c1 EQ(s(z0), 0') -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) LE(0', z0) -> c4 LE(s(z0), 0') -> c5 LE(s(z0), s(z1)) -> c6(LE(z0, z1)) MIN(cons(0', nil)) -> c7 MIN(cons(s(z0), nil)) -> c8 MIN(cons(z0, cons(z1, z2))) -> c9(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1)) IF_MIN(true, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z0, z2))) IF_MIN(false, cons(z0, cons(z1, z2))) -> c11(MIN(cons(z1, z2))) REPLACE(z0, z1, nil) -> c12 REPLACE(z0, z1, cons(z2, z3)) -> c13(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2)) IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c14 IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c15(REPLACE(z0, z1, z3)) SORT(nil) -> c16 SORT(cons(z0, z1)) -> c17(MIN(cons(z0, z1))) SORT(cons(z0, z1)) -> c18(SORT(replace(min(cons(z0, z1)), z0, z1)), REPLACE(min(cons(z0, z1)), z0, z1), MIN(cons(z0, z1))) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) min(cons(0', nil)) -> 0' min(cons(s(z0), nil)) -> s(z0) min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2))) if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2)) if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2)) replace(z0, z1, nil) -> nil replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3)) if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3) if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3)) sort(nil) -> nil sort(cons(z0, z1)) -> cons(min(cons(z0, z1)), sort(replace(min(cons(z0, z1)), z0, z1))) Types: EQ :: 0':s -> 0':s -> c:c1:c2:c3 0' :: 0':s c :: c:c1:c2:c3 s :: 0':s -> 0':s c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 -> c:c1:c2:c3 LE :: 0':s -> 0':s -> c4:c5:c6 c4 :: c4:c5:c6 c5 :: c4:c5:c6 c6 :: c4:c5:c6 -> c4:c5:c6 MIN :: nil:cons -> c7:c8:c9 cons :: 0':s -> nil:cons -> nil:cons nil :: nil:cons c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c10:c11 -> c4:c5:c6 -> c7:c8:c9 IF_MIN :: true:false -> nil:cons -> c10:c11 le :: 0':s -> 0':s -> true:false true :: true:false c10 :: c7:c8:c9 -> c10:c11 false :: true:false c11 :: c7:c8:c9 -> c10:c11 REPLACE :: 0':s -> 0':s -> nil:cons -> c12:c13 c12 :: c12:c13 c13 :: c14:c15 -> c:c1:c2:c3 -> c12:c13 IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons -> c14:c15 eq :: 0':s -> 0':s -> true:false c14 :: c14:c15 c15 :: c12:c13 -> c14:c15 SORT :: nil:cons -> c16:c17:c18 c16 :: c16:c17:c18 c17 :: c7:c8:c9 -> c16:c17:c18 c18 :: c16:c17:c18 -> c12:c13 -> c7:c8:c9 -> c16:c17:c18 replace :: 0':s -> 0':s -> nil:cons -> nil:cons min :: nil:cons -> 0':s if_min :: true:false -> nil:cons -> 0':s if_replace :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c2:c31_19 :: c:c1:c2:c3 hole_0':s2_19 :: 0':s hole_c4:c5:c63_19 :: c4:c5:c6 hole_c7:c8:c94_19 :: c7:c8:c9 hole_nil:cons5_19 :: nil:cons hole_c10:c116_19 :: c10:c11 hole_true:false7_19 :: true:false hole_c12:c138_19 :: c12:c13 hole_c14:c159_19 :: c14:c15 hole_c16:c17:c1810_19 :: c16:c17:c18 gen_c:c1:c2:c311_19 :: Nat -> c:c1:c2:c3 gen_0':s12_19 :: Nat -> 0':s gen_c4:c5:c613_19 :: Nat -> c4:c5:c6 gen_nil:cons14_19 :: Nat -> nil:cons gen_c16:c17:c1815_19 :: Nat -> c16:c17:c18 Lemmas: EQ(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c2:c311_19(n17_19), rt in Omega(1 + n17_19) LE(gen_0':s12_19(n1023_19), gen_0':s12_19(n1023_19)) -> gen_c4:c5:c613_19(n1023_19), rt in Omega(1 + n1023_19) le(gen_0':s12_19(n1803_19), gen_0':s12_19(n1803_19)) -> true, rt in Omega(0) MIN(gen_nil:cons14_19(+(1, n2270_19))) -> *16_19, rt in Omega(n2270_19) eq(gen_0':s12_19(n7487_19), gen_0':s12_19(n7487_19)) -> true, rt in Omega(0) min(gen_nil:cons14_19(+(1, n9513_19))) -> gen_0':s12_19(0), rt in Omega(0) Generator Equations: gen_c:c1:c2:c311_19(0) <=> c gen_c:c1:c2:c311_19(+(x, 1)) <=> c3(gen_c:c1:c2:c311_19(x)) gen_0':s12_19(0) <=> 0' gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x)) gen_c4:c5:c613_19(0) <=> c4 gen_c4:c5:c613_19(+(x, 1)) <=> c6(gen_c4:c5:c613_19(x)) gen_nil:cons14_19(0) <=> nil gen_nil:cons14_19(+(x, 1)) <=> cons(0', gen_nil:cons14_19(x)) gen_c16:c17:c1815_19(0) <=> c16 gen_c16:c17:c1815_19(+(x, 1)) <=> c18(gen_c16:c17:c1815_19(x), c12, c7) The following defined symbols remain to be analysed: SORT, sort ---------------------------------------- (76) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (77) BOUNDS(n^2, INF) ---------------------------------------- (78) Obligation: Innermost TRS: Rules: EQ(0', 0') -> c EQ(0', s(z0)) -> c1 EQ(s(z0), 0') -> c2 EQ(s(z0), s(z1)) -> c3(EQ(z0, z1)) LE(0', z0) -> c4 LE(s(z0), 0') -> c5 LE(s(z0), s(z1)) -> c6(LE(z0, z1)) MIN(cons(0', nil)) -> c7 MIN(cons(s(z0), nil)) -> c8 MIN(cons(z0, cons(z1, z2))) -> c9(IF_MIN(le(z0, z1), cons(z0, cons(z1, z2))), LE(z0, z1)) IF_MIN(true, cons(z0, cons(z1, z2))) -> c10(MIN(cons(z0, z2))) IF_MIN(false, cons(z0, cons(z1, z2))) -> c11(MIN(cons(z1, z2))) REPLACE(z0, z1, nil) -> c12 REPLACE(z0, z1, cons(z2, z3)) -> c13(IF_REPLACE(eq(z0, z2), z0, z1, cons(z2, z3)), EQ(z0, z2)) IF_REPLACE(true, z0, z1, cons(z2, z3)) -> c14 IF_REPLACE(false, z0, z1, cons(z2, z3)) -> c15(REPLACE(z0, z1, z3)) SORT(nil) -> c16 SORT(cons(z0, z1)) -> c17(MIN(cons(z0, z1))) SORT(cons(z0, z1)) -> c18(SORT(replace(min(cons(z0, z1)), z0, z1)), REPLACE(min(cons(z0, z1)), z0, z1), MIN(cons(z0, z1))) eq(0', 0') -> true eq(0', s(z0)) -> false eq(s(z0), 0') -> false eq(s(z0), s(z1)) -> eq(z0, z1) le(0', z0) -> true le(s(z0), 0') -> false le(s(z0), s(z1)) -> le(z0, z1) min(cons(0', nil)) -> 0' min(cons(s(z0), nil)) -> s(z0) min(cons(z0, cons(z1, z2))) -> if_min(le(z0, z1), cons(z0, cons(z1, z2))) if_min(true, cons(z0, cons(z1, z2))) -> min(cons(z0, z2)) if_min(false, cons(z0, cons(z1, z2))) -> min(cons(z1, z2)) replace(z0, z1, nil) -> nil replace(z0, z1, cons(z2, z3)) -> if_replace(eq(z0, z2), z0, z1, cons(z2, z3)) if_replace(true, z0, z1, cons(z2, z3)) -> cons(z1, z3) if_replace(false, z0, z1, cons(z2, z3)) -> cons(z2, replace(z0, z1, z3)) sort(nil) -> nil sort(cons(z0, z1)) -> cons(min(cons(z0, z1)), sort(replace(min(cons(z0, z1)), z0, z1))) Types: EQ :: 0':s -> 0':s -> c:c1:c2:c3 0' :: 0':s c :: c:c1:c2:c3 s :: 0':s -> 0':s c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 -> c:c1:c2:c3 LE :: 0':s -> 0':s -> c4:c5:c6 c4 :: c4:c5:c6 c5 :: c4:c5:c6 c6 :: c4:c5:c6 -> c4:c5:c6 MIN :: nil:cons -> c7:c8:c9 cons :: 0':s -> nil:cons -> nil:cons nil :: nil:cons c7 :: c7:c8:c9 c8 :: c7:c8:c9 c9 :: c10:c11 -> c4:c5:c6 -> c7:c8:c9 IF_MIN :: true:false -> nil:cons -> c10:c11 le :: 0':s -> 0':s -> true:false true :: true:false c10 :: c7:c8:c9 -> c10:c11 false :: true:false c11 :: c7:c8:c9 -> c10:c11 REPLACE :: 0':s -> 0':s -> nil:cons -> c12:c13 c12 :: c12:c13 c13 :: c14:c15 -> c:c1:c2:c3 -> c12:c13 IF_REPLACE :: true:false -> 0':s -> 0':s -> nil:cons -> c14:c15 eq :: 0':s -> 0':s -> true:false c14 :: c14:c15 c15 :: c12:c13 -> c14:c15 SORT :: nil:cons -> c16:c17:c18 c16 :: c16:c17:c18 c17 :: c7:c8:c9 -> c16:c17:c18 c18 :: c16:c17:c18 -> c12:c13 -> c7:c8:c9 -> c16:c17:c18 replace :: 0':s -> 0':s -> nil:cons -> nil:cons min :: nil:cons -> 0':s if_min :: true:false -> nil:cons -> 0':s if_replace :: true:false -> 0':s -> 0':s -> nil:cons -> nil:cons sort :: nil:cons -> nil:cons hole_c:c1:c2:c31_19 :: c:c1:c2:c3 hole_0':s2_19 :: 0':s hole_c4:c5:c63_19 :: c4:c5:c6 hole_c7:c8:c94_19 :: c7:c8:c9 hole_nil:cons5_19 :: nil:cons hole_c10:c116_19 :: c10:c11 hole_true:false7_19 :: true:false hole_c12:c138_19 :: c12:c13 hole_c14:c159_19 :: c14:c15 hole_c16:c17:c1810_19 :: c16:c17:c18 gen_c:c1:c2:c311_19 :: Nat -> c:c1:c2:c3 gen_0':s12_19 :: Nat -> 0':s gen_c4:c5:c613_19 :: Nat -> c4:c5:c6 gen_nil:cons14_19 :: Nat -> nil:cons gen_c16:c17:c1815_19 :: Nat -> c16:c17:c18 Lemmas: EQ(gen_0':s12_19(n17_19), gen_0':s12_19(n17_19)) -> gen_c:c1:c2:c311_19(n17_19), rt in Omega(1 + n17_19) LE(gen_0':s12_19(n1023_19), gen_0':s12_19(n1023_19)) -> gen_c4:c5:c613_19(n1023_19), rt in Omega(1 + n1023_19) le(gen_0':s12_19(n1803_19), gen_0':s12_19(n1803_19)) -> true, rt in Omega(0) MIN(gen_nil:cons14_19(+(1, n2270_19))) -> *16_19, rt in Omega(n2270_19) eq(gen_0':s12_19(n7487_19), gen_0':s12_19(n7487_19)) -> true, rt in Omega(0) min(gen_nil:cons14_19(+(1, n9513_19))) -> gen_0':s12_19(0), rt in Omega(0) SORT(gen_nil:cons14_19(+(1, n10367_19))) -> *16_19, rt in Omega(n10367_19 + n10367_19^2) Generator Equations: gen_c:c1:c2:c311_19(0) <=> c gen_c:c1:c2:c311_19(+(x, 1)) <=> c3(gen_c:c1:c2:c311_19(x)) gen_0':s12_19(0) <=> 0' gen_0':s12_19(+(x, 1)) <=> s(gen_0':s12_19(x)) gen_c4:c5:c613_19(0) <=> c4 gen_c4:c5:c613_19(+(x, 1)) <=> c6(gen_c4:c5:c613_19(x)) gen_nil:cons14_19(0) <=> nil gen_nil:cons14_19(+(x, 1)) <=> cons(0', gen_nil:cons14_19(x)) gen_c16:c17:c1815_19(0) <=> c16 gen_c16:c17:c1815_19(+(x, 1)) <=> c18(gen_c16:c17:c1815_19(x), c12, c7) The following defined symbols remain to be analysed: sort ---------------------------------------- (79) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: sort(gen_nil:cons14_19(+(1, n401090_19))) -> *16_19, rt in Omega(0) Induction Base: sort(gen_nil:cons14_19(+(1, 0))) Induction Step: sort(gen_nil:cons14_19(+(1, +(n401090_19, 1)))) ->_R^Omega(0) cons(min(cons(0', gen_nil:cons14_19(+(1, n401090_19)))), sort(replace(min(cons(0', gen_nil:cons14_19(+(1, n401090_19)))), 0', gen_nil:cons14_19(+(1, n401090_19))))) ->_L^Omega(0) cons(gen_0':s12_19(0), sort(replace(min(cons(0', gen_nil:cons14_19(+(1, n401090_19)))), 0', gen_nil:cons14_19(+(1, n401090_19))))) ->_L^Omega(0) cons(gen_0':s12_19(0), sort(replace(gen_0':s12_19(0), 0', gen_nil:cons14_19(+(1, n401090_19))))) ->_R^Omega(0) cons(gen_0':s12_19(0), sort(if_replace(eq(gen_0':s12_19(0), 0'), gen_0':s12_19(0), 0', cons(0', gen_nil:cons14_19(n401090_19))))) ->_L^Omega(0) cons(gen_0':s12_19(0), sort(if_replace(true, gen_0':s12_19(0), 0', cons(0', gen_nil:cons14_19(n401090_19))))) ->_R^Omega(0) cons(gen_0':s12_19(0), sort(cons(0', gen_nil:cons14_19(n401090_19)))) ->_IH cons(gen_0':s12_19(0), *16_19) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (80) BOUNDS(1, INF)