WORST_CASE(?,O(n^1)) proof of input_fz7C6urvmU.trs # AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1). (0) CpxTRS (1) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (2) CdtProblem (3) CdtLeafRemovalProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CdtProblem (5) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (6) CdtProblem (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CpxRelTRS (9) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CpxWeightedTrs (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CpxTypedWeightedTrs (13) CompletionProof [UPPER BOUND(ID), 0 ms] (14) CpxTypedWeightedCompleteTrs (15) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (16) CpxRNTS (17) CompleteCoflocoProof [FINISHED, 665 ms] (18) BOUNDS(1, n^1) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: a__and(true, X) -> mark(X) a__and(false, Y) -> false a__if(true, X, Y) -> mark(X) a__if(false, X, Y) -> mark(Y) a__add(0, X) -> mark(X) a__add(s(X), Y) -> s(add(X, Y)) a__first(0, X) -> nil a__first(s(X), cons(Y, Z)) -> cons(Y, first(X, Z)) a__from(X) -> cons(X, from(s(X))) mark(and(X1, X2)) -> a__and(mark(X1), X2) mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) mark(add(X1, X2)) -> a__add(mark(X1), X2) mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)) mark(from(X)) -> a__from(X) mark(true) -> true mark(false) -> false mark(0) -> 0 mark(s(X)) -> s(X) mark(nil) -> nil mark(cons(X1, X2)) -> cons(X1, X2) a__and(X1, X2) -> and(X1, X2) a__if(X1, X2, X3) -> if(X1, X2, X3) a__add(X1, X2) -> add(X1, X2) a__first(X1, X2) -> first(X1, X2) a__from(X) -> from(X) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (2) Obligation: Complexity Dependency Tuples Problem Rules: a__and(true, z0) -> mark(z0) a__and(false, z0) -> false a__and(z0, z1) -> and(z0, z1) a__if(true, z0, z1) -> mark(z0) a__if(false, z0, z1) -> mark(z1) a__if(z0, z1, z2) -> if(z0, z1, z2) a__add(0, z0) -> mark(z0) a__add(s(z0), z1) -> s(add(z0, z1)) a__add(z0, z1) -> add(z0, z1) a__first(0, z0) -> nil a__first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2)) a__first(z0, z1) -> first(z0, z1) a__from(z0) -> cons(z0, from(s(z0))) a__from(z0) -> from(z0) mark(and(z0, z1)) -> a__and(mark(z0), z1) mark(if(z0, z1, z2)) -> a__if(mark(z0), z1, z2) mark(add(z0, z1)) -> a__add(mark(z0), z1) mark(first(z0, z1)) -> a__first(mark(z0), mark(z1)) mark(from(z0)) -> a__from(z0) mark(true) -> true mark(false) -> false mark(0) -> 0 mark(s(z0)) -> s(z0) mark(nil) -> nil mark(cons(z0, z1)) -> cons(z0, z1) Tuples: A__AND(true, z0) -> c(MARK(z0)) A__AND(false, z0) -> c1 A__AND(z0, z1) -> c2 A__IF(true, z0, z1) -> c3(MARK(z0)) A__IF(false, z0, z1) -> c4(MARK(z1)) A__IF(z0, z1, z2) -> c5 A__ADD(0, z0) -> c6(MARK(z0)) A__ADD(s(z0), z1) -> c7 A__ADD(z0, z1) -> c8 A__FIRST(0, z0) -> c9 A__FIRST(s(z0), cons(z1, z2)) -> c10 A__FIRST(z0, z1) -> c11 A__FROM(z0) -> c12 A__FROM(z0) -> c13 MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0)) MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0)) MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0)) MARK(first(z0, z1)) -> c17(A__FIRST(mark(z0), mark(z1)), MARK(z0)) MARK(first(z0, z1)) -> c18(A__FIRST(mark(z0), mark(z1)), MARK(z1)) MARK(from(z0)) -> c19(A__FROM(z0)) MARK(true) -> c20 MARK(false) -> c21 MARK(0) -> c22 MARK(s(z0)) -> c23 MARK(nil) -> c24 MARK(cons(z0, z1)) -> c25 S tuples: A__AND(true, z0) -> c(MARK(z0)) A__AND(false, z0) -> c1 A__AND(z0, z1) -> c2 A__IF(true, z0, z1) -> c3(MARK(z0)) A__IF(false, z0, z1) -> c4(MARK(z1)) A__IF(z0, z1, z2) -> c5 A__ADD(0, z0) -> c6(MARK(z0)) A__ADD(s(z0), z1) -> c7 A__ADD(z0, z1) -> c8 A__FIRST(0, z0) -> c9 A__FIRST(s(z0), cons(z1, z2)) -> c10 A__FIRST(z0, z1) -> c11 A__FROM(z0) -> c12 A__FROM(z0) -> c13 MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0)) MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0)) MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0)) MARK(first(z0, z1)) -> c17(A__FIRST(mark(z0), mark(z1)), MARK(z0)) MARK(first(z0, z1)) -> c18(A__FIRST(mark(z0), mark(z1)), MARK(z1)) MARK(from(z0)) -> c19(A__FROM(z0)) MARK(true) -> c20 MARK(false) -> c21 MARK(0) -> c22 MARK(s(z0)) -> c23 MARK(nil) -> c24 MARK(cons(z0, z1)) -> c25 K tuples:none Defined Rule Symbols: a__and_2, a__if_3, a__add_2, a__first_2, a__from_1, mark_1 Defined Pair Symbols: A__AND_2, A__IF_3, A__ADD_2, A__FIRST_2, A__FROM_1, MARK_1 Compound Symbols: c_1, c1, c2, c3_1, c4_1, c5, c6_1, c7, c8, c9, c10, c11, c12, c13, c14_2, c15_2, c16_2, c17_2, c18_2, c19_1, c20, c21, c22, c23, c24, c25 ---------------------------------------- (3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID)) Removed 17 trailing nodes: MARK(true) -> c20 MARK(cons(z0, z1)) -> c25 A__FIRST(z0, z1) -> c11 A__AND(false, z0) -> c1 MARK(s(z0)) -> c23 MARK(0) -> c22 MARK(false) -> c21 A__FIRST(s(z0), cons(z1, z2)) -> c10 MARK(nil) -> c24 MARK(from(z0)) -> c19(A__FROM(z0)) A__FROM(z0) -> c12 A__FROM(z0) -> c13 A__ADD(s(z0), z1) -> c7 A__FIRST(0, z0) -> c9 A__AND(z0, z1) -> c2 A__IF(z0, z1, z2) -> c5 A__ADD(z0, z1) -> c8 ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: a__and(true, z0) -> mark(z0) a__and(false, z0) -> false a__and(z0, z1) -> and(z0, z1) a__if(true, z0, z1) -> mark(z0) a__if(false, z0, z1) -> mark(z1) a__if(z0, z1, z2) -> if(z0, z1, z2) a__add(0, z0) -> mark(z0) a__add(s(z0), z1) -> s(add(z0, z1)) a__add(z0, z1) -> add(z0, z1) a__first(0, z0) -> nil a__first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2)) a__first(z0, z1) -> first(z0, z1) a__from(z0) -> cons(z0, from(s(z0))) a__from(z0) -> from(z0) mark(and(z0, z1)) -> a__and(mark(z0), z1) mark(if(z0, z1, z2)) -> a__if(mark(z0), z1, z2) mark(add(z0, z1)) -> a__add(mark(z0), z1) mark(first(z0, z1)) -> a__first(mark(z0), mark(z1)) mark(from(z0)) -> a__from(z0) mark(true) -> true mark(false) -> false mark(0) -> 0 mark(s(z0)) -> s(z0) mark(nil) -> nil mark(cons(z0, z1)) -> cons(z0, z1) Tuples: A__AND(true, z0) -> c(MARK(z0)) A__IF(true, z0, z1) -> c3(MARK(z0)) A__IF(false, z0, z1) -> c4(MARK(z1)) A__ADD(0, z0) -> c6(MARK(z0)) MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0)) MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0)) MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0)) MARK(first(z0, z1)) -> c17(A__FIRST(mark(z0), mark(z1)), MARK(z0)) MARK(first(z0, z1)) -> c18(A__FIRST(mark(z0), mark(z1)), MARK(z1)) S tuples: A__AND(true, z0) -> c(MARK(z0)) A__IF(true, z0, z1) -> c3(MARK(z0)) A__IF(false, z0, z1) -> c4(MARK(z1)) A__ADD(0, z0) -> c6(MARK(z0)) MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0)) MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0)) MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0)) MARK(first(z0, z1)) -> c17(A__FIRST(mark(z0), mark(z1)), MARK(z0)) MARK(first(z0, z1)) -> c18(A__FIRST(mark(z0), mark(z1)), MARK(z1)) K tuples:none Defined Rule Symbols: a__and_2, a__if_3, a__add_2, a__first_2, a__from_1, mark_1 Defined Pair Symbols: A__AND_2, A__IF_3, A__ADD_2, MARK_1 Compound Symbols: c_1, c3_1, c4_1, c6_1, c14_2, c15_2, c16_2, c17_2, c18_2 ---------------------------------------- (5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing tuple parts ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: a__and(true, z0) -> mark(z0) a__and(false, z0) -> false a__and(z0, z1) -> and(z0, z1) a__if(true, z0, z1) -> mark(z0) a__if(false, z0, z1) -> mark(z1) a__if(z0, z1, z2) -> if(z0, z1, z2) a__add(0, z0) -> mark(z0) a__add(s(z0), z1) -> s(add(z0, z1)) a__add(z0, z1) -> add(z0, z1) a__first(0, z0) -> nil a__first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2)) a__first(z0, z1) -> first(z0, z1) a__from(z0) -> cons(z0, from(s(z0))) a__from(z0) -> from(z0) mark(and(z0, z1)) -> a__and(mark(z0), z1) mark(if(z0, z1, z2)) -> a__if(mark(z0), z1, z2) mark(add(z0, z1)) -> a__add(mark(z0), z1) mark(first(z0, z1)) -> a__first(mark(z0), mark(z1)) mark(from(z0)) -> a__from(z0) mark(true) -> true mark(false) -> false mark(0) -> 0 mark(s(z0)) -> s(z0) mark(nil) -> nil mark(cons(z0, z1)) -> cons(z0, z1) Tuples: A__AND(true, z0) -> c(MARK(z0)) A__IF(true, z0, z1) -> c3(MARK(z0)) A__IF(false, z0, z1) -> c4(MARK(z1)) A__ADD(0, z0) -> c6(MARK(z0)) MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0)) MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0)) MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0)) MARK(first(z0, z1)) -> c17(MARK(z0)) MARK(first(z0, z1)) -> c18(MARK(z1)) S tuples: A__AND(true, z0) -> c(MARK(z0)) A__IF(true, z0, z1) -> c3(MARK(z0)) A__IF(false, z0, z1) -> c4(MARK(z1)) A__ADD(0, z0) -> c6(MARK(z0)) MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0)) MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0)) MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0)) MARK(first(z0, z1)) -> c17(MARK(z0)) MARK(first(z0, z1)) -> c18(MARK(z1)) K tuples:none Defined Rule Symbols: a__and_2, a__if_3, a__add_2, a__first_2, a__from_1, mark_1 Defined Pair Symbols: A__AND_2, A__IF_3, A__ADD_2, MARK_1 Compound Symbols: c_1, c3_1, c4_1, c6_1, c14_2, c15_2, c16_2, c17_1, c18_1 ---------------------------------------- (7) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (8) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: A__AND(true, z0) -> c(MARK(z0)) A__IF(true, z0, z1) -> c3(MARK(z0)) A__IF(false, z0, z1) -> c4(MARK(z1)) A__ADD(0, z0) -> c6(MARK(z0)) MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0)) MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0)) MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0)) MARK(first(z0, z1)) -> c17(MARK(z0)) MARK(first(z0, z1)) -> c18(MARK(z1)) The (relative) TRS S consists of the following rules: a__and(true, z0) -> mark(z0) a__and(false, z0) -> false a__and(z0, z1) -> and(z0, z1) a__if(true, z0, z1) -> mark(z0) a__if(false, z0, z1) -> mark(z1) a__if(z0, z1, z2) -> if(z0, z1, z2) a__add(0, z0) -> mark(z0) a__add(s(z0), z1) -> s(add(z0, z1)) a__add(z0, z1) -> add(z0, z1) a__first(0, z0) -> nil a__first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2)) a__first(z0, z1) -> first(z0, z1) a__from(z0) -> cons(z0, from(s(z0))) a__from(z0) -> from(z0) mark(and(z0, z1)) -> a__and(mark(z0), z1) mark(if(z0, z1, z2)) -> a__if(mark(z0), z1, z2) mark(add(z0, z1)) -> a__add(mark(z0), z1) mark(first(z0, z1)) -> a__first(mark(z0), mark(z1)) mark(from(z0)) -> a__from(z0) mark(true) -> true mark(false) -> false mark(0) -> 0 mark(s(z0)) -> s(z0) mark(nil) -> nil mark(cons(z0, z1)) -> cons(z0, z1) Rewrite Strategy: INNERMOST ---------------------------------------- (9) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (10) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1). The TRS R consists of the following rules: A__AND(true, z0) -> c(MARK(z0)) [1] A__IF(true, z0, z1) -> c3(MARK(z0)) [1] A__IF(false, z0, z1) -> c4(MARK(z1)) [1] A__ADD(0, z0) -> c6(MARK(z0)) [1] MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0)) [1] MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0)) [1] MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0)) [1] MARK(first(z0, z1)) -> c17(MARK(z0)) [1] MARK(first(z0, z1)) -> c18(MARK(z1)) [1] a__and(true, z0) -> mark(z0) [0] a__and(false, z0) -> false [0] a__and(z0, z1) -> and(z0, z1) [0] a__if(true, z0, z1) -> mark(z0) [0] a__if(false, z0, z1) -> mark(z1) [0] a__if(z0, z1, z2) -> if(z0, z1, z2) [0] a__add(0, z0) -> mark(z0) [0] a__add(s(z0), z1) -> s(add(z0, z1)) [0] a__add(z0, z1) -> add(z0, z1) [0] a__first(0, z0) -> nil [0] a__first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2)) [0] a__first(z0, z1) -> first(z0, z1) [0] a__from(z0) -> cons(z0, from(s(z0))) [0] a__from(z0) -> from(z0) [0] mark(and(z0, z1)) -> a__and(mark(z0), z1) [0] mark(if(z0, z1, z2)) -> a__if(mark(z0), z1, z2) [0] mark(add(z0, z1)) -> a__add(mark(z0), z1) [0] mark(first(z0, z1)) -> a__first(mark(z0), mark(z1)) [0] mark(from(z0)) -> a__from(z0) [0] mark(true) -> true [0] mark(false) -> false [0] mark(0) -> 0 [0] mark(s(z0)) -> s(z0) [0] mark(nil) -> nil [0] mark(cons(z0, z1)) -> cons(z0, z1) [0] Rewrite Strategy: INNERMOST ---------------------------------------- (11) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (12) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: A__AND(true, z0) -> c(MARK(z0)) [1] A__IF(true, z0, z1) -> c3(MARK(z0)) [1] A__IF(false, z0, z1) -> c4(MARK(z1)) [1] A__ADD(0, z0) -> c6(MARK(z0)) [1] MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0)) [1] MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0)) [1] MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0)) [1] MARK(first(z0, z1)) -> c17(MARK(z0)) [1] MARK(first(z0, z1)) -> c18(MARK(z1)) [1] a__and(true, z0) -> mark(z0) [0] a__and(false, z0) -> false [0] a__and(z0, z1) -> and(z0, z1) [0] a__if(true, z0, z1) -> mark(z0) [0] a__if(false, z0, z1) -> mark(z1) [0] a__if(z0, z1, z2) -> if(z0, z1, z2) [0] a__add(0, z0) -> mark(z0) [0] a__add(s(z0), z1) -> s(add(z0, z1)) [0] a__add(z0, z1) -> add(z0, z1) [0] a__first(0, z0) -> nil [0] a__first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2)) [0] a__first(z0, z1) -> first(z0, z1) [0] a__from(z0) -> cons(z0, from(s(z0))) [0] a__from(z0) -> from(z0) [0] mark(and(z0, z1)) -> a__and(mark(z0), z1) [0] mark(if(z0, z1, z2)) -> a__if(mark(z0), z1, z2) [0] mark(add(z0, z1)) -> a__add(mark(z0), z1) [0] mark(first(z0, z1)) -> a__first(mark(z0), mark(z1)) [0] mark(from(z0)) -> a__from(z0) [0] mark(true) -> true [0] mark(false) -> false [0] mark(0) -> 0 [0] mark(s(z0)) -> s(z0) [0] mark(nil) -> nil [0] mark(cons(z0, z1)) -> cons(z0, z1) [0] The TRS has the following type information: A__AND :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from -> c true :: true:false:0:and:if:add:first:s:nil:cons:from c :: c14:c15:c16:c17:c18 -> c MARK :: true:false:0:and:if:add:first:s:nil:cons:from -> c14:c15:c16:c17:c18 A__IF :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from -> c3:c4 c3 :: c14:c15:c16:c17:c18 -> c3:c4 false :: true:false:0:and:if:add:first:s:nil:cons:from c4 :: c14:c15:c16:c17:c18 -> c3:c4 A__ADD :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from -> c6 0 :: true:false:0:and:if:add:first:s:nil:cons:from c6 :: c14:c15:c16:c17:c18 -> c6 and :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from c14 :: c -> c14:c15:c16:c17:c18 -> c14:c15:c16:c17:c18 mark :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from if :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from c15 :: c3:c4 -> c14:c15:c16:c17:c18 -> c14:c15:c16:c17:c18 add :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from c16 :: c6 -> c14:c15:c16:c17:c18 -> c14:c15:c16:c17:c18 first :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from c17 :: c14:c15:c16:c17:c18 -> c14:c15:c16:c17:c18 c18 :: c14:c15:c16:c17:c18 -> c14:c15:c16:c17:c18 a__and :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from a__if :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from a__add :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from s :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from a__first :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from nil :: true:false:0:and:if:add:first:s:nil:cons:from cons :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from a__from :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from from :: true:false:0:and:if:add:first:s:nil:cons:from -> true:false:0:and:if:add:first:s:nil:cons:from Rewrite Strategy: INNERMOST ---------------------------------------- (13) CompletionProof (UPPER BOUND(ID)) The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added: a__and(v0, v1) -> null_a__and [0] a__if(v0, v1, v2) -> null_a__if [0] a__add(v0, v1) -> null_a__add [0] a__first(v0, v1) -> null_a__first [0] a__from(v0) -> null_a__from [0] mark(v0) -> null_mark [0] A__AND(v0, v1) -> null_A__AND [0] A__IF(v0, v1, v2) -> null_A__IF [0] A__ADD(v0, v1) -> null_A__ADD [0] MARK(v0) -> null_MARK [0] And the following fresh constants: null_a__and, null_a__if, null_a__add, null_a__first, null_a__from, null_mark, null_A__AND, null_A__IF, null_A__ADD, null_MARK ---------------------------------------- (14) Obligation: Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: A__AND(true, z0) -> c(MARK(z0)) [1] A__IF(true, z0, z1) -> c3(MARK(z0)) [1] A__IF(false, z0, z1) -> c4(MARK(z1)) [1] A__ADD(0, z0) -> c6(MARK(z0)) [1] MARK(and(z0, z1)) -> c14(A__AND(mark(z0), z1), MARK(z0)) [1] MARK(if(z0, z1, z2)) -> c15(A__IF(mark(z0), z1, z2), MARK(z0)) [1] MARK(add(z0, z1)) -> c16(A__ADD(mark(z0), z1), MARK(z0)) [1] MARK(first(z0, z1)) -> c17(MARK(z0)) [1] MARK(first(z0, z1)) -> c18(MARK(z1)) [1] a__and(true, z0) -> mark(z0) [0] a__and(false, z0) -> false [0] a__and(z0, z1) -> and(z0, z1) [0] a__if(true, z0, z1) -> mark(z0) [0] a__if(false, z0, z1) -> mark(z1) [0] a__if(z0, z1, z2) -> if(z0, z1, z2) [0] a__add(0, z0) -> mark(z0) [0] a__add(s(z0), z1) -> s(add(z0, z1)) [0] a__add(z0, z1) -> add(z0, z1) [0] a__first(0, z0) -> nil [0] a__first(s(z0), cons(z1, z2)) -> cons(z1, first(z0, z2)) [0] a__first(z0, z1) -> first(z0, z1) [0] a__from(z0) -> cons(z0, from(s(z0))) [0] a__from(z0) -> from(z0) [0] mark(and(z0, z1)) -> a__and(mark(z0), z1) [0] mark(if(z0, z1, z2)) -> a__if(mark(z0), z1, z2) [0] mark(add(z0, z1)) -> a__add(mark(z0), z1) [0] mark(first(z0, z1)) -> a__first(mark(z0), mark(z1)) [0] mark(from(z0)) -> a__from(z0) [0] mark(true) -> true [0] mark(false) -> false [0] mark(0) -> 0 [0] mark(s(z0)) -> s(z0) [0] mark(nil) -> nil [0] mark(cons(z0, z1)) -> cons(z0, z1) [0] a__and(v0, v1) -> null_a__and [0] a__if(v0, v1, v2) -> null_a__if [0] a__add(v0, v1) -> null_a__add [0] a__first(v0, v1) -> null_a__first [0] a__from(v0) -> null_a__from [0] mark(v0) -> null_mark [0] A__AND(v0, v1) -> null_A__AND [0] A__IF(v0, v1, v2) -> null_A__IF [0] A__ADD(v0, v1) -> null_A__ADD [0] MARK(v0) -> null_MARK [0] The TRS has the following type information: A__AND :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> c:null_A__AND true :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark c :: c14:c15:c16:c17:c18:null_MARK -> c:null_A__AND MARK :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> c14:c15:c16:c17:c18:null_MARK A__IF :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> c3:c4:null_A__IF c3 :: c14:c15:c16:c17:c18:null_MARK -> c3:c4:null_A__IF false :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark c4 :: c14:c15:c16:c17:c18:null_MARK -> c3:c4:null_A__IF A__ADD :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> c6:null_A__ADD 0 :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark c6 :: c14:c15:c16:c17:c18:null_MARK -> c6:null_A__ADD and :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark c14 :: c:null_A__AND -> c14:c15:c16:c17:c18:null_MARK -> c14:c15:c16:c17:c18:null_MARK mark :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark if :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark c15 :: c3:c4:null_A__IF -> c14:c15:c16:c17:c18:null_MARK -> c14:c15:c16:c17:c18:null_MARK add :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark c16 :: c6:null_A__ADD -> c14:c15:c16:c17:c18:null_MARK -> c14:c15:c16:c17:c18:null_MARK first :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark c17 :: c14:c15:c16:c17:c18:null_MARK -> c14:c15:c16:c17:c18:null_MARK c18 :: c14:c15:c16:c17:c18:null_MARK -> c14:c15:c16:c17:c18:null_MARK a__and :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark a__if :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark a__add :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark s :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark a__first :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark nil :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark cons :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark a__from :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark from :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark -> true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark null_a__and :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark null_a__if :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark null_a__add :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark null_a__first :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark null_a__from :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark null_mark :: true:false:0:and:if:add:first:s:nil:cons:from:null_a__and:null_a__if:null_a__add:null_a__first:null_a__from:null_mark null_A__AND :: c:null_A__AND null_A__IF :: c3:c4:null_A__IF null_A__ADD :: c6:null_A__ADD null_MARK :: c14:c15:c16:c17:c18:null_MARK Rewrite Strategy: INNERMOST ---------------------------------------- (15) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: true => 3 false => 1 0 => 0 nil => 2 null_a__and => 0 null_a__if => 0 null_a__add => 0 null_a__first => 0 null_a__from => 0 null_mark => 0 null_A__AND => 0 null_A__IF => 0 null_A__ADD => 0 null_MARK => 0 ---------------------------------------- (16) Obligation: Complexity RNTS consisting of the following rules: A__ADD(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 A__ADD(z, z') -{ 1 }-> 1 + MARK(z0) :|: z0 >= 0, z = 0, z' = z0 A__AND(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 A__AND(z, z') -{ 1 }-> 1 + MARK(z0) :|: z = 3, z0 >= 0, z' = z0 A__IF(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 A__IF(z, z', z'') -{ 1 }-> 1 + MARK(z0) :|: z = 3, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 A__IF(z, z', z'') -{ 1 }-> 1 + MARK(z1) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1 MARK(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 MARK(z) -{ 1 }-> 1 + MARK(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 MARK(z) -{ 1 }-> 1 + MARK(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 MARK(z) -{ 1 }-> 1 + A__IF(mark(z0), z1, z2) + MARK(z0) :|: z1 >= 0, z = 1 + z0 + z1 + z2, z0 >= 0, z2 >= 0 MARK(z) -{ 1 }-> 1 + A__AND(mark(z0), z1) + MARK(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 MARK(z) -{ 1 }-> 1 + A__ADD(mark(z0), z1) + MARK(z0) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 a__add(z, z') -{ 0 }-> mark(z0) :|: z0 >= 0, z = 0, z' = z0 a__add(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 a__add(z, z') -{ 0 }-> 1 + (1 + z0 + z1) :|: z1 >= 0, z = 1 + z0, z' = z1, z0 >= 0 a__add(z, z') -{ 0 }-> 1 + z0 + z1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 a__and(z, z') -{ 0 }-> mark(z0) :|: z = 3, z0 >= 0, z' = z0 a__and(z, z') -{ 0 }-> 1 :|: z = 1, z0 >= 0, z' = z0 a__and(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 a__and(z, z') -{ 0 }-> 1 + z0 + z1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 a__first(z, z') -{ 0 }-> 2 :|: z0 >= 0, z = 0, z' = z0 a__first(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 a__first(z, z') -{ 0 }-> 1 + z0 + z1 :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 a__first(z, z') -{ 0 }-> 1 + z1 + (1 + z0 + z2) :|: z1 >= 0, z' = 1 + z1 + z2, z = 1 + z0, z0 >= 0, z2 >= 0 a__from(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 a__from(z) -{ 0 }-> 1 + z0 :|: z = z0, z0 >= 0 a__from(z) -{ 0 }-> 1 + z0 + (1 + (1 + z0)) :|: z = z0, z0 >= 0 a__if(z, z', z'') -{ 0 }-> mark(z0) :|: z = 3, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 a__if(z, z', z'') -{ 0 }-> mark(z1) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1 a__if(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 a__if(z, z', z'') -{ 0 }-> 1 + z0 + z1 + z2 :|: z'' = z2, z = z0, z1 >= 0, z' = z1, z0 >= 0, z2 >= 0 mark(z) -{ 0 }-> a__if(mark(z0), z1, z2) :|: z1 >= 0, z = 1 + z0 + z1 + z2, z0 >= 0, z2 >= 0 mark(z) -{ 0 }-> a__from(z0) :|: z = 1 + z0, z0 >= 0 mark(z) -{ 0 }-> a__first(mark(z0), mark(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 mark(z) -{ 0 }-> a__and(mark(z0), z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 mark(z) -{ 0 }-> a__add(mark(z0), z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 mark(z) -{ 0 }-> 3 :|: z = 3 mark(z) -{ 0 }-> 2 :|: z = 2 mark(z) -{ 0 }-> 1 :|: z = 1 mark(z) -{ 0 }-> 0 :|: z = 0 mark(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 mark(z) -{ 0 }-> 1 + z0 :|: z = 1 + z0, z0 >= 0 mark(z) -{ 0 }-> 1 + z0 + z1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (17) CompleteCoflocoProof (FINISHED) Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo: eq(start(V1, V, V3),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V3),0,[fun2(V1, V, V3, Out)],[V1 >= 0,V >= 0,V3 >= 0]). eq(start(V1, V, V3),0,[fun3(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V3),0,[fun1(V1, Out)],[V1 >= 0]). eq(start(V1, V, V3),0,[fun4(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V3),0,[fun5(V1, V, V3, Out)],[V1 >= 0,V >= 0,V3 >= 0]). eq(start(V1, V, V3),0,[fun6(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V3),0,[fun7(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V3),0,[fun8(V1, Out)],[V1 >= 0]). eq(start(V1, V, V3),0,[mark(V1, Out)],[V1 >= 0]). eq(fun(V1, V, Out),1,[fun1(V2, Ret1)],[Out = 1 + Ret1,V1 = 3,V2 >= 0,V = V2]). eq(fun2(V1, V, V3, Out),1,[fun1(V5, Ret11)],[Out = 1 + Ret11,V1 = 3,V4 >= 0,V5 >= 0,V = V5,V3 = V4]). eq(fun2(V1, V, V3, Out),1,[fun1(V6, Ret12)],[Out = 1 + Ret12,V6 >= 0,V1 = 1,V7 >= 0,V = V7,V3 = V6]). eq(fun3(V1, V, Out),1,[fun1(V8, Ret13)],[Out = 1 + Ret13,V8 >= 0,V1 = 0,V = V8]). eq(fun1(V1, Out),1,[mark(V9, Ret010),fun(Ret010, V10, Ret01),fun1(V9, Ret14)],[Out = 1 + Ret01 + Ret14,V10 >= 0,V9 >= 0,V1 = 1 + V10 + V9]). eq(fun1(V1, Out),1,[mark(V11, Ret0101),fun2(Ret0101, V12, V13, Ret011),fun1(V11, Ret15)],[Out = 1 + Ret011 + Ret15,V12 >= 0,V1 = 1 + V11 + V12 + V13,V11 >= 0,V13 >= 0]). eq(fun1(V1, Out),1,[mark(V15, Ret0102),fun3(Ret0102, V14, Ret012),fun1(V15, Ret16)],[Out = 1 + Ret012 + Ret16,V14 >= 0,V15 >= 0,V1 = 1 + V14 + V15]). eq(fun1(V1, Out),1,[fun1(V17, Ret17)],[Out = 1 + Ret17,V16 >= 0,V17 >= 0,V1 = 1 + V16 + V17]). eq(fun1(V1, Out),1,[fun1(V18, Ret18)],[Out = 1 + Ret18,V18 >= 0,V19 >= 0,V1 = 1 + V18 + V19]). eq(fun4(V1, V, Out),0,[mark(V20, Ret)],[Out = Ret,V1 = 3,V20 >= 0,V = V20]). eq(fun4(V1, V, Out),0,[],[Out = 1,V1 = 1,V21 >= 0,V = V21]). eq(fun4(V1, V, Out),0,[],[Out = 1 + V22 + V23,V1 = V23,V22 >= 0,V = V22,V23 >= 0]). eq(fun5(V1, V, V3, Out),0,[mark(V24, Ret2)],[Out = Ret2,V1 = 3,V25 >= 0,V24 >= 0,V = V24,V3 = V25]). eq(fun5(V1, V, V3, Out),0,[mark(V27, Ret3)],[Out = Ret3,V27 >= 0,V1 = 1,V26 >= 0,V = V26,V3 = V27]). eq(fun5(V1, V, V3, Out),0,[],[Out = 1 + V28 + V29 + V30,V3 = V28,V1 = V30,V29 >= 0,V = V29,V30 >= 0,V28 >= 0]). eq(fun6(V1, V, Out),0,[mark(V31, Ret4)],[Out = Ret4,V31 >= 0,V1 = 0,V = V31]). eq(fun6(V1, V, Out),0,[],[Out = 2 + V32 + V33,V32 >= 0,V1 = 1 + V33,V = V32,V33 >= 0]). eq(fun6(V1, V, Out),0,[],[Out = 1 + V34 + V35,V1 = V35,V34 >= 0,V = V34,V35 >= 0]). eq(fun7(V1, V, Out),0,[],[Out = 2,V36 >= 0,V1 = 0,V = V36]). eq(fun7(V1, V, Out),0,[],[Out = 2 + V37 + V38 + V39,V39 >= 0,V = 1 + V38 + V39,V1 = 1 + V37,V37 >= 0,V38 >= 0]). eq(fun7(V1, V, Out),0,[],[Out = 1 + V40 + V41,V1 = V40,V41 >= 0,V = V41,V40 >= 0]). eq(fun8(V1, Out),0,[],[Out = 3 + 2*V42,V1 = V42,V42 >= 0]). eq(fun8(V1, Out),0,[],[Out = 1 + V43,V1 = V43,V43 >= 0]). eq(mark(V1, Out),0,[mark(V44, Ret0),fun4(Ret0, V45, Ret5)],[Out = Ret5,V45 >= 0,V44 >= 0,V1 = 1 + V44 + V45]). eq(mark(V1, Out),0,[mark(V46, Ret02),fun5(Ret02, V48, V47, Ret6)],[Out = Ret6,V48 >= 0,V1 = 1 + V46 + V47 + V48,V46 >= 0,V47 >= 0]). eq(mark(V1, Out),0,[mark(V49, Ret03),fun6(Ret03, V50, Ret7)],[Out = Ret7,V50 >= 0,V49 >= 0,V1 = 1 + V49 + V50]). eq(mark(V1, Out),0,[mark(V51, Ret04),mark(V52, Ret19),fun7(Ret04, Ret19, Ret8)],[Out = Ret8,V52 >= 0,V51 >= 0,V1 = 1 + V51 + V52]). eq(mark(V1, Out),0,[fun8(V53, Ret9)],[Out = Ret9,V1 = 1 + V53,V53 >= 0]). eq(mark(V1, Out),0,[],[Out = 3,V1 = 3]). eq(mark(V1, Out),0,[],[Out = 1,V1 = 1]). eq(mark(V1, Out),0,[],[Out = 0,V1 = 0]). eq(mark(V1, Out),0,[],[Out = 1 + V54,V1 = 1 + V54,V54 >= 0]). eq(mark(V1, Out),0,[],[Out = 2,V1 = 2]). eq(mark(V1, Out),0,[],[Out = 1 + V55 + V56,V55 >= 0,V56 >= 0,V1 = 1 + V55 + V56]). eq(fun4(V1, V, Out),0,[],[Out = 0,V58 >= 0,V57 >= 0,V1 = V58,V = V57]). eq(fun5(V1, V, V3, Out),0,[],[Out = 0,V60 >= 0,V3 = V61,V59 >= 0,V1 = V60,V = V59,V61 >= 0]). eq(fun6(V1, V, Out),0,[],[Out = 0,V63 >= 0,V62 >= 0,V1 = V63,V = V62]). eq(fun7(V1, V, Out),0,[],[Out = 0,V64 >= 0,V65 >= 0,V1 = V64,V = V65]). eq(fun8(V1, Out),0,[],[Out = 0,V66 >= 0,V1 = V66]). eq(mark(V1, Out),0,[],[Out = 0,V67 >= 0,V1 = V67]). eq(fun(V1, V, Out),0,[],[Out = 0,V69 >= 0,V68 >= 0,V1 = V69,V = V68]). eq(fun2(V1, V, V3, Out),0,[],[Out = 0,V70 >= 0,V3 = V72,V71 >= 0,V1 = V70,V = V71,V72 >= 0]). eq(fun3(V1, V, Out),0,[],[Out = 0,V73 >= 0,V74 >= 0,V1 = V73,V = V74]). eq(fun1(V1, Out),0,[],[Out = 0,V75 >= 0,V1 = V75]). input_output_vars(fun(V1,V,Out),[V1,V],[Out]). input_output_vars(fun2(V1,V,V3,Out),[V1,V,V3],[Out]). input_output_vars(fun3(V1,V,Out),[V1,V],[Out]). input_output_vars(fun1(V1,Out),[V1],[Out]). input_output_vars(fun4(V1,V,Out),[V1,V],[Out]). input_output_vars(fun5(V1,V,V3,Out),[V1,V,V3],[Out]). input_output_vars(fun6(V1,V,Out),[V1,V],[Out]). input_output_vars(fun7(V1,V,Out),[V1,V],[Out]). input_output_vars(fun8(V1,Out),[V1],[Out]). input_output_vars(mark(V1,Out),[V1],[Out]). CoFloCo proof output: Preprocessing Cost Relations ===================================== #### Computed strongly connected components 0. non_recursive : [fun7/3] 1. non_recursive : [fun8/2] 2. recursive [non_tail,multiple] : [fun4/3,fun5/4,fun6/3,mark/2] 3. recursive [multiple] : [fun/3,fun1/2,fun2/4,fun3/3] 4. non_recursive : [start/3] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into fun7/3 1. SCC is partially evaluated into fun8/2 2. SCC is partially evaluated into mark/2 3. SCC is partially evaluated into fun1/2 4. SCC is partially evaluated into start/3 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations fun7/3 * CE 30 is refined into CE [36] * CE 31 is refined into CE [37] * CE 32 is refined into CE [38] * CE 29 is refined into CE [39] ### Cost equations --> "Loop" of fun7/3 * CEs [36] --> Loop 22 * CEs [37] --> Loop 23 * CEs [38] --> Loop 24 * CEs [39] --> Loop 25 ### Ranking functions of CR fun7(V1,V,Out) #### Partial ranking functions of CR fun7(V1,V,Out) ### Specialization of cost equations fun8/2 * CE 33 is refined into CE [40] * CE 34 is refined into CE [41] * CE 35 is refined into CE [42] ### Cost equations --> "Loop" of fun8/2 * CEs [40] --> Loop 26 * CEs [41] --> Loop 27 * CEs [42] --> Loop 28 ### Ranking functions of CR fun8(V1,Out) #### Partial ranking functions of CR fun8(V1,Out) ### Specialization of cost equations mark/2 * CE 25 is refined into CE [43,44,45] * CE 26 is refined into CE [46] * CE 27 is refined into CE [47] * CE 28 is refined into CE [48] * CE 21 is refined into CE [49] * CE 22 is refined into CE [50] * CE 23 is refined into CE [51] * CE 24 is refined into CE [52,53,54,55] * CE 19 is refined into CE [56] * CE 20 is refined into CE [57] * CE 18 is refined into CE [58] ### Cost equations --> "Loop" of mark/2 * CEs [56] --> Loop 29 * CEs [57] --> Loop 30 * CEs [58] --> Loop 31 * CEs [55] --> Loop 32 * CEs [54] --> Loop 33 * CEs [49] --> Loop 34 * CEs [50] --> Loop 35 * CEs [51] --> Loop 36 * CEs [52] --> Loop 37 * CEs [53] --> Loop 38 * CEs [45] --> Loop 39 * CEs [44,46,47] --> Loop 40 * CEs [43,48] --> Loop 41 ### Ranking functions of CR mark(V1,Out) * RF of phase [29,30,31,32,33,34,35,36,37,38]: [V1] #### Partial ranking functions of CR mark(V1,Out) * Partial RF of phase [29,30,31,32,33,34,35,36,37,38]: - RF of loop [29:1,30:1,31:1,32:1,32:2,33:1,33:2,34:1,34:2,35:1,35:2,36:1,36:2,37:1,37:2,38:1,38:2]: V1 ### Specialization of cost equations fun1/2 * CE 17 is refined into CE [59] * CE 12 is refined into CE [60,61,62] * CE 16 is refined into CE [63] * CE 13 is refined into CE [64] * CE 14 is refined into CE [65,66] * CE 15 is refined into CE [67,68] ### Cost equations --> "Loop" of fun1/2 * CEs [67,68] --> Loop 42 * CEs [64,65,66] --> Loop 43 * CEs [60,61,62,63] --> Loop 44 * CEs [59] --> Loop 45 ### Ranking functions of CR fun1(V1,Out) * RF of phase [42,43,44]: [V1] #### Partial ranking functions of CR fun1(V1,Out) * Partial RF of phase [42,43,44]: - RF of loop [42:1,42:2,44:1]: V1 - RF of loop [43:1,43:2]: V1-1 ### Specialization of cost equations start/3 * CE 3 is refined into CE [69,70] * CE 5 is refined into CE [71,72,73] * CE 2 is refined into CE [74,75] * CE 6 is refined into CE [76,77,78] * CE 1 is refined into CE [79] * CE 4 is refined into CE [80,81] * CE 7 is refined into CE [82,83,84] * CE 8 is refined into CE [85,86] * CE 9 is refined into CE [87,88,89,90] * CE 10 is refined into CE [91,92,93] * CE 11 is refined into CE [94,95,96] ### Cost equations --> "Loop" of start/3 * CEs [69,70,71,72,73] --> Loop 46 * CEs [74,75,76,77,78] --> Loop 47 * CEs [79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96] --> Loop 48 ### Ranking functions of CR start(V1,V,V3) #### Partial ranking functions of CR start(V1,V,V3) Computing Bounds ===================================== #### Cost of chains of fun7(V1,V,Out): * Chain [25]: 0 with precondition: [V1=0,Out=2,V>=0] * Chain [24]: 0 with precondition: [Out=0,V1>=0,V>=0] * Chain [23]: 0 with precondition: [V+V1+1=Out,V1>=0,V>=0] * Chain [22]: 0 with precondition: [V+V1=Out,V1>=1,V>=1] #### Cost of chains of fun8(V1,Out): * Chain [28]: 0 with precondition: [Out=0,V1>=0] * Chain [27]: 0 with precondition: [V1+1=Out,V1>=0] * Chain [26]: 0 with precondition: [2*V1+3=Out,V1>=0] #### Cost of chains of mark(V1,Out): * Chain [41]: 0 with precondition: [Out=0,V1>=0] * Chain [40]: 0 with precondition: [V1=Out,V1>=1] * Chain [39]: 0 with precondition: [2*V1+1=Out,V1>=1] * Chain [multiple([29,30,31,32,33,34,35,36,37,38],[[41],[40],[39]])]: 0 with precondition: [V1>=1,Out>=0,5*V1>=2*Out+1,2*V1+1>=Out] #### Cost of chains of fun1(V1,Out): * Chain [45]: 0 with precondition: [Out=0,V1>=0] * Chain [multiple([42,43,44],[[45]])]: 5*it(42)+0 Such that:aux(15) =< V1 it(42) =< aux(15) with precondition: [V1>=1,Out>=1,2*V1>=Out] #### Cost of chains of start(V1,V,V3): * Chain [48]: 5*s(2)+5*s(4)+1 Such that:s(3) =< V1 s(1) =< V s(4) =< s(3) s(2) =< s(1) with precondition: [V1>=0] * Chain [47]: 5*s(6)+1 Such that:s(5) =< V3 s(6) =< s(5) with precondition: [V1=1,V>=0,V3>=0] * Chain [46]: 5*s(8)+1 Such that:s(7) =< V s(8) =< s(7) with precondition: [V1=3,V>=0] Closed-form bounds of start(V1,V,V3): ------------------------------------- * Chain [48] with precondition: [V1>=0] - Upper bound: 5*V1+1+nat(V)*5 - Complexity: n * Chain [47] with precondition: [V1=1,V>=0,V3>=0] - Upper bound: 5*V3+1 - Complexity: n * Chain [46] with precondition: [V1=3,V>=0] - Upper bound: 5*V+1 - Complexity: n ### Maximum cost of start(V1,V,V3): max([nat(V3)*5,nat(V)*5+5*V1])+1 Asymptotic class: n * Total analysis performed in 552 ms. ---------------------------------------- (18) BOUNDS(1, n^1)