WORST_CASE(Omega(n^1),O(n^3)) proof of input_0sjpewTi9Q.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^3). (0) CpxRelTRS (1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 281 ms] (2) CpxRelTRS (3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms] (4) CdtProblem (5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms] (6) CdtProblem (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms] (8) CdtProblem (9) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms] (10) CdtProblem (11) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (12) CpxRelTRS (13) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (14) CpxWeightedTrs (15) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (16) CpxTypedWeightedTrs (17) CompletionProof [UPPER BOUND(ID), 0 ms] (18) CpxTypedWeightedCompleteTrs (19) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (20) CpxRNTS (21) CompleteCoflocoProof [FINISHED, 66.4 s] (22) BOUNDS(1, n^3) (23) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 3 ms] (24) CdtProblem (25) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms] (26) CpxRelTRS (27) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms] (28) CpxRelTRS (29) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (30) typed CpxTrs (31) OrderProof [LOWER BOUND(ID), 5 ms] (32) typed CpxTrs (33) RewriteLemmaProof [LOWER BOUND(ID), 274 ms] (34) BEST (35) proven lower bound (36) LowerBoundPropagationProof [FINISHED, 0 ms] (37) BOUNDS(n^1, INF) (38) typed CpxTrs (39) RewriteLemmaProof [LOWER BOUND(ID), 171 ms] (40) typed CpxTrs (41) RewriteLemmaProof [LOWER BOUND(ID), 62 ms] (42) typed CpxTrs (43) RewriteLemmaProof [LOWER BOUND(ID), 87 ms] (44) typed CpxTrs (45) RewriteLemmaProof [LOWER BOUND(ID), 64 ms] (46) typed CpxTrs (47) RewriteLemmaProof [LOWER BOUND(ID), 61 ms] (48) typed CpxTrs (49) RewriteLemmaProof [LOWER BOUND(ID), 1331 ms] (50) typed CpxTrs ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^3). The TRS R consists of the following rules: @(Cons(x, xs), ys) -> Cons(x, @(xs, ys)) @(Nil, ys) -> ys gt0(Cons(x, xs), Nil) -> True gt0(Cons(x', xs'), Cons(x, xs)) -> gt0(xs', xs) gcd(Nil, Nil) -> Nil gcd(Nil, Cons(x, xs)) -> Nil gcd(Cons(x, xs), Nil) -> Nil gcd(Cons(x', xs'), Cons(x, xs)) -> gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs)) lgth(Cons(x, xs)) -> @(Cons(Nil, Nil), lgth(xs)) eqList(Cons(x, xs), Cons(y, ys)) -> and(eqList(x, y), eqList(xs, ys)) eqList(Cons(x, xs), Nil) -> False eqList(Nil, Cons(y, ys)) -> False eqList(Nil, Nil) -> True lgth(Nil) -> Nil gt0(Nil, y) -> False monus(x, y) -> monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y) goal(x, y) -> gcd(x, y) The (relative) TRS S consists of the following rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(x', xs'), Cons(x, xs)) -> monus(xs', xs) monus[Ite](True, Cons(x, xs), y) -> xs gcd[Ite](False, x, y) -> gcd[False][Ite](gt0(x, y), x, y) gcd[Ite](True, x, y) -> x gcd[False][Ite](False, x, y) -> gcd(x, monus(y, x)) gcd[False][Ite](True, x, y) -> gcd(monus(x, y), y) Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID)) proved innermost termination of relative rules ---------------------------------------- (2) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, n^3). The TRS R consists of the following rules: @(Cons(x, xs), ys) -> Cons(x, @(xs, ys)) @(Nil, ys) -> ys gt0(Cons(x, xs), Nil) -> True gt0(Cons(x', xs'), Cons(x, xs)) -> gt0(xs', xs) gcd(Nil, Nil) -> Nil gcd(Nil, Cons(x, xs)) -> Nil gcd(Cons(x, xs), Nil) -> Nil gcd(Cons(x', xs'), Cons(x, xs)) -> gcd[Ite](eqList(Cons(x', xs'), Cons(x, xs)), Cons(x', xs'), Cons(x, xs)) lgth(Cons(x, xs)) -> @(Cons(Nil, Nil), lgth(xs)) eqList(Cons(x, xs), Cons(y, ys)) -> and(eqList(x, y), eqList(xs, ys)) eqList(Cons(x, xs), Nil) -> False eqList(Nil, Cons(y, ys)) -> False eqList(Nil, Nil) -> True lgth(Nil) -> Nil gt0(Nil, y) -> False monus(x, y) -> monus[Ite](eqList(lgth(y), Cons(Nil, Nil)), x, y) goal(x, y) -> gcd(x, y) The (relative) TRS S consists of the following rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(x', xs'), Cons(x, xs)) -> monus(xs', xs) monus[Ite](True, Cons(x, xs), y) -> xs gcd[Ite](False, x, y) -> gcd[False][Ite](gt0(x, y), x, y) gcd[Ite](True, x, y) -> x gcd[False][Ite](False, x, y) -> gcd(x, monus(y, x)) gcd[False][Ite](True, x, y) -> gcd(monus(x, y), y) Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (3) CpxTrsToCdtProof (UPPER BOUND(ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (4) Obligation: Complexity Dependency Tuples Problem Rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Tuples: AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) MONUS[ITE](True, Cons(z0, z1), z2) -> c5 GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[ITE](True, z0, z1) -> c7 GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) S tuples: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) K tuples:none Defined Rule Symbols: @_2, gt0_2, gcd_2, lgth_1, eqList_2, monus_2, goal_2, and_2, monus[Ite]_3, gcd[Ite]_3, gcd[False][Ite]_3 Defined Pair Symbols: AND_2, MONUS[ITE]_3, GCD[ITE]_3, GCD[FALSE][ITE]_3, @'_2, GT0_2, GCD_2, LGTH_1, EQLIST_2, MONUS_2, GOAL_2 Compound Symbols: c, c1, c2, c3, c4_1, c5, c6_2, c7, c8_2, c9_2, c10_1, c11, c12, c13_1, c14, c15, c16, c17, c18_2, c19_2, c20, c21_2, c22_2, c23, c24, c25, c26_3, c27_1 ---------------------------------------- (5) CdtLeafRemovalProof (ComplexityIfPolyImplication) Removed 1 leading nodes: GOAL(z0, z1) -> c27(GCD(z0, z1)) Removed 11 trailing nodes: EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Nil) -> c25 EQLIST(Nil, Cons(z0, z1)) -> c24 @'(Nil, z0) -> c11 GCD[ITE](True, z0, z1) -> c7 AND(True, False) -> c1 AND(False, False) -> c LGTH(Nil) -> c20 AND(True, True) -> c3 MONUS[ITE](True, Cons(z0, z1), z2) -> c5 AND(False, True) -> c2 ---------------------------------------- (6) Obligation: Complexity Dependency Tuples Problem Rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Tuples: MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) S tuples: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) K tuples:none Defined Rule Symbols: @_2, gt0_2, gcd_2, lgth_1, eqList_2, monus_2, goal_2, and_2, monus[Ite]_3, gcd[Ite]_3, gcd[False][Ite]_3 Defined Pair Symbols: MONUS[ITE]_3, GCD[ITE]_3, GCD[FALSE][ITE]_3, @'_2, GT0_2, GCD_2, LGTH_1, EQLIST_2, MONUS_2 Compound Symbols: c4_1, c6_2, c8_2, c9_2, c10_1, c12, c13_1, c14, c15, c16, c17, c18_2, c19_2, c21_2, c22_2, c26_3 ---------------------------------------- (7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID)) Removed 2 trailing tuple parts ---------------------------------------- (8) Obligation: Complexity Dependency Tuples Problem Rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Tuples: MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(EQLIST(z1, z3)) S tuples: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(EQLIST(z1, z3)) K tuples:none Defined Rule Symbols: @_2, gt0_2, gcd_2, lgth_1, eqList_2, monus_2, goal_2, and_2, monus[Ite]_3, gcd[Ite]_3, gcd[False][Ite]_3 Defined Pair Symbols: MONUS[ITE]_3, GCD[ITE]_3, GCD[FALSE][ITE]_3, @'_2, GT0_2, GCD_2, LGTH_1, MONUS_2, EQLIST_2 Compound Symbols: c4_1, c6_2, c8_2, c9_2, c10_1, c12, c13_1, c14, c15, c16, c17, c18_2, c19_2, c26_3, c21_1, c22_1 ---------------------------------------- (9) CdtUsableRulesProof (BOTH BOUNDS(ID, ID)) The following rules are not usable and were removed: gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) goal(z0, z1) -> gcd(z0, z1) ---------------------------------------- (10) Obligation: Complexity Dependency Tuples Problem Rules: gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Nil, Cons(z0, z1)) -> False eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Nil) -> True lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True Tuples: MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(EQLIST(z1, z3)) S tuples: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(EQLIST(z1, z3)) K tuples:none Defined Rule Symbols: gt0_2, monus_2, monus[Ite]_3, eqList_2, lgth_1, @_2, and_2 Defined Pair Symbols: MONUS[ITE]_3, GCD[ITE]_3, GCD[FALSE][ITE]_3, @'_2, GT0_2, GCD_2, LGTH_1, MONUS_2, EQLIST_2 Compound Symbols: c4_1, c6_2, c8_2, c9_2, c10_1, c12, c13_1, c14, c15, c16, c17, c18_2, c19_2, c26_3, c21_1, c22_1 ---------------------------------------- (11) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (12) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^3). The TRS R consists of the following rules: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(EQLIST(z1, z3)) The (relative) TRS S consists of the following rules: MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Nil, Cons(z0, z1)) -> False eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Nil) -> True lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True Rewrite Strategy: INNERMOST ---------------------------------------- (13) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (14) 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: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) [1] GT0(Cons(z0, z1), Nil) -> c12 [1] GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) [1] GT0(Nil, z0) -> c14 [1] GCD(Nil, Nil) -> c15 [1] GCD(Nil, Cons(z0, z1)) -> c16 [1] GCD(Cons(z0, z1), Nil) -> c17 [1] GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) [1] LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) [1] MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) [1] EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(EQLIST(z0, z2)) [1] EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(EQLIST(z1, z3)) [1] MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) [0] GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) [0] GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) [0] GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) [0] gt0(Cons(z0, z1), Nil) -> True [0] gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) [0] gt0(Nil, z0) -> False [0] monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) [0] monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) [0] monus[Ite](True, Cons(z0, z1), z2) -> z1 [0] eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) [0] eqList(Nil, Cons(z0, z1)) -> False [0] eqList(Cons(z0, z1), Nil) -> False [0] eqList(Nil, Nil) -> True [0] lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) [0] lgth(Nil) -> Nil [0] @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) [0] @(Nil, z0) -> z0 [0] and(False, False) -> False [0] and(True, False) -> False [0] and(False, True) -> False [0] and(True, True) -> True [0] Rewrite Strategy: INNERMOST ---------------------------------------- (15) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (16) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) [1] GT0(Cons(z0, z1), Nil) -> c12 [1] GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) [1] GT0(Nil, z0) -> c14 [1] GCD(Nil, Nil) -> c15 [1] GCD(Nil, Cons(z0, z1)) -> c16 [1] GCD(Cons(z0, z1), Nil) -> c17 [1] GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) [1] LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) [1] MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) [1] EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(EQLIST(z0, z2)) [1] EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(EQLIST(z1, z3)) [1] MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) [0] GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) [0] GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) [0] GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) [0] gt0(Cons(z0, z1), Nil) -> True [0] gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) [0] gt0(Nil, z0) -> False [0] monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) [0] monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) [0] monus[Ite](True, Cons(z0, z1), z2) -> z1 [0] eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) [0] eqList(Nil, Cons(z0, z1)) -> False [0] eqList(Cons(z0, z1), Nil) -> False [0] eqList(Nil, Nil) -> True [0] lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) [0] lgth(Nil) -> Nil [0] @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) [0] @(Nil, z0) -> z0 [0] and(False, False) -> False [0] and(True, False) -> False [0] and(False, True) -> False [0] and(True, True) -> True [0] The TRS has the following type information: @' :: Cons:Nil -> Cons:Nil -> c10 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c10 :: c10 -> c10 GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14 Nil :: Cons:Nil c12 :: c12:c13:c14 c13 :: c12:c13:c14 -> c12:c13:c14 c14 :: c12:c13:c14 GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18 c15 :: c15:c16:c17:c18 c16 :: c15:c16:c17:c18 c17 :: c15:c16:c17:c18 c18 :: c6 -> c21:c22 -> c15:c16:c17:c18 GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6 eqList :: Cons:Nil -> Cons:Nil -> False:True EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22 LGTH :: Cons:Nil -> c19 c19 :: c10 -> c19 -> c19 lgth :: Cons:Nil -> Cons:Nil MONUS :: Cons:Nil -> Cons:Nil -> c26 c26 :: c4 -> c21:c22 -> c19 -> c26 MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4 c21 :: c21:c22 -> c21:c22 c22 :: c21:c22 -> c21:c22 False :: False:True c4 :: c26 -> c4 c6 :: c8:c9 -> c12:c13:c14 -> c6 GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9 gt0 :: Cons:Nil -> Cons:Nil -> False:True c8 :: c15:c16:c17:c18 -> c26 -> c8:c9 monus :: Cons:Nil -> Cons:Nil -> Cons:Nil True :: False:True c9 :: c15:c16:c17:c18 -> c26 -> c8:c9 monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil and :: False:True -> False:True -> False:True @ :: Cons:Nil -> Cons:Nil -> Cons:Nil Rewrite Strategy: INNERMOST ---------------------------------------- (17) 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: MONUS[ITE](v0, v1, v2) -> null_MONUS[ITE] [0] GCD[ITE](v0, v1, v2) -> null_GCD[ITE] [0] GCD[FALSE][ITE](v0, v1, v2) -> null_GCD[FALSE][ITE] [0] gt0(v0, v1) -> null_gt0 [0] monus(v0, v1) -> null_monus [0] monus[Ite](v0, v1, v2) -> null_monus[Ite] [0] eqList(v0, v1) -> null_eqList [0] lgth(v0) -> null_lgth [0] @(v0, v1) -> null_@ [0] and(v0, v1) -> null_and [0] @'(v0, v1) -> null_@' [0] GT0(v0, v1) -> null_GT0 [0] GCD(v0, v1) -> null_GCD [0] LGTH(v0) -> null_LGTH [0] EQLIST(v0, v1) -> null_EQLIST [0] And the following fresh constants: null_MONUS[ITE], null_GCD[ITE], null_GCD[FALSE][ITE], null_gt0, null_monus, null_monus[Ite], null_eqList, null_lgth, null_@, null_and, null_@', null_GT0, null_GCD, null_LGTH, null_EQLIST, const ---------------------------------------- (18) 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: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) [1] GT0(Cons(z0, z1), Nil) -> c12 [1] GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) [1] GT0(Nil, z0) -> c14 [1] GCD(Nil, Nil) -> c15 [1] GCD(Nil, Cons(z0, z1)) -> c16 [1] GCD(Cons(z0, z1), Nil) -> c17 [1] GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) [1] LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) [1] MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) [1] EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(EQLIST(z0, z2)) [1] EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(EQLIST(z1, z3)) [1] MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) [0] GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) [0] GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) [0] GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) [0] gt0(Cons(z0, z1), Nil) -> True [0] gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) [0] gt0(Nil, z0) -> False [0] monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) [0] monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) [0] monus[Ite](True, Cons(z0, z1), z2) -> z1 [0] eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) [0] eqList(Nil, Cons(z0, z1)) -> False [0] eqList(Cons(z0, z1), Nil) -> False [0] eqList(Nil, Nil) -> True [0] lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) [0] lgth(Nil) -> Nil [0] @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) [0] @(Nil, z0) -> z0 [0] and(False, False) -> False [0] and(True, False) -> False [0] and(False, True) -> False [0] and(True, True) -> True [0] MONUS[ITE](v0, v1, v2) -> null_MONUS[ITE] [0] GCD[ITE](v0, v1, v2) -> null_GCD[ITE] [0] GCD[FALSE][ITE](v0, v1, v2) -> null_GCD[FALSE][ITE] [0] gt0(v0, v1) -> null_gt0 [0] monus(v0, v1) -> null_monus [0] monus[Ite](v0, v1, v2) -> null_monus[Ite] [0] eqList(v0, v1) -> null_eqList [0] lgth(v0) -> null_lgth [0] @(v0, v1) -> null_@ [0] and(v0, v1) -> null_and [0] @'(v0, v1) -> null_@' [0] GT0(v0, v1) -> null_GT0 [0] GCD(v0, v1) -> null_GCD [0] LGTH(v0) -> null_LGTH [0] EQLIST(v0, v1) -> null_EQLIST [0] The TRS has the following type information: @' :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> c10:null_@' Cons :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ c10 :: c10:null_@' -> c10:null_@' GT0 :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> c12:c13:c14:null_GT0 Nil :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ c12 :: c12:c13:c14:null_GT0 c13 :: c12:c13:c14:null_GT0 -> c12:c13:c14:null_GT0 c14 :: c12:c13:c14:null_GT0 GCD :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> c15:c16:c17:c18:null_GCD c15 :: c15:c16:c17:c18:null_GCD c16 :: c15:c16:c17:c18:null_GCD c17 :: c15:c16:c17:c18:null_GCD c18 :: c6:null_GCD[ITE] -> c21:c22:null_EQLIST -> c15:c16:c17:c18:null_GCD GCD[ITE] :: False:True:null_gt0:null_eqList:null_and -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> c6:null_GCD[ITE] eqList :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> False:True:null_gt0:null_eqList:null_and EQLIST :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> c21:c22:null_EQLIST LGTH :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> c19:null_LGTH c19 :: c10:null_@' -> c19:null_LGTH -> c19:null_LGTH lgth :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ MONUS :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> c26 c26 :: c4:null_MONUS[ITE] -> c21:c22:null_EQLIST -> c19:null_LGTH -> c26 MONUS[ITE] :: False:True:null_gt0:null_eqList:null_and -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> c4:null_MONUS[ITE] c21 :: c21:c22:null_EQLIST -> c21:c22:null_EQLIST c22 :: c21:c22:null_EQLIST -> c21:c22:null_EQLIST False :: False:True:null_gt0:null_eqList:null_and c4 :: c26 -> c4:null_MONUS[ITE] c6 :: c8:c9:null_GCD[FALSE][ITE] -> c12:c13:c14:null_GT0 -> c6:null_GCD[ITE] GCD[FALSE][ITE] :: False:True:null_gt0:null_eqList:null_and -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> c8:c9:null_GCD[FALSE][ITE] gt0 :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> False:True:null_gt0:null_eqList:null_and c8 :: c15:c16:c17:c18:null_GCD -> c26 -> c8:c9:null_GCD[FALSE][ITE] monus :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ True :: False:True:null_gt0:null_eqList:null_and c9 :: c15:c16:c17:c18:null_GCD -> c26 -> c8:c9:null_GCD[FALSE][ITE] monus[Ite] :: False:True:null_gt0:null_eqList:null_and -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ and :: False:True:null_gt0:null_eqList:null_and -> False:True:null_gt0:null_eqList:null_and -> False:True:null_gt0:null_eqList:null_and @ :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ -> Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ null_MONUS[ITE] :: c4:null_MONUS[ITE] null_GCD[ITE] :: c6:null_GCD[ITE] null_GCD[FALSE][ITE] :: c8:c9:null_GCD[FALSE][ITE] null_gt0 :: False:True:null_gt0:null_eqList:null_and null_monus :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ null_monus[Ite] :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ null_eqList :: False:True:null_gt0:null_eqList:null_and null_lgth :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ null_@ :: Cons:Nil:null_monus:null_monus[Ite]:null_lgth:null_@ null_and :: False:True:null_gt0:null_eqList:null_and null_@' :: c10:null_@' null_GT0 :: c12:c13:c14:null_GT0 null_GCD :: c15:c16:c17:c18:null_GCD null_LGTH :: c19:null_LGTH null_EQLIST :: c21:c22:null_EQLIST const :: c26 Rewrite Strategy: INNERMOST ---------------------------------------- (19) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: Nil => 0 c12 => 0 c14 => 1 c15 => 0 c16 => 1 c17 => 2 False => 1 True => 2 null_MONUS[ITE] => 0 null_GCD[ITE] => 0 null_GCD[FALSE][ITE] => 0 null_gt0 => 0 null_monus => 0 null_monus[Ite] => 0 null_eqList => 0 null_lgth => 0 null_@ => 0 null_and => 0 null_@' => 0 null_GT0 => 0 null_GCD => 0 null_LGTH => 0 null_EQLIST => 0 const => 0 ---------------------------------------- (20) Obligation: Complexity RNTS consisting of the following rules: @(z, z') -{ 0 }-> z0 :|: z0 >= 0, z = 0, z' = z0 @(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 @(z, z') -{ 0 }-> 1 + z0 + @(z1, z2) :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + z0 + z1, z2 >= 0 @'(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 @'(z, z') -{ 1 }-> 1 + @'(z1, z2) :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + z0 + z1, z2 >= 0 EQLIST(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 EQLIST(z, z') -{ 1 }-> 1 + EQLIST(z0, z2) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0 EQLIST(z, z') -{ 1 }-> 1 + EQLIST(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0 GCD(z, z') -{ 1 }-> 2 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' = 0 GCD(z, z') -{ 1 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0 GCD(z, z') -{ 1 }-> 0 :|: z = 0, z' = 0 GCD(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 GCD(z, z') -{ 1 }-> 1 + GCD[ITE](eqList(1 + z0 + z1, 1 + z2 + z3), 1 + z0 + z1, 1 + z2 + z3) + EQLIST(1 + z0 + z1, 1 + z2 + z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0 GCD[FALSE][ITE](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 GCD[FALSE][ITE](z, z', z'') -{ 0 }-> 1 + GCD(z0, monus(z1, z0)) + MONUS(z1, z0) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1 GCD[FALSE][ITE](z, z', z'') -{ 0 }-> 1 + GCD(monus(z0, z1), z1) + MONUS(z0, z1) :|: z = 2, z1 >= 0, z0 >= 0, z' = z0, z'' = z1 GCD[ITE](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 GCD[ITE](z, z', z'') -{ 0 }-> 1 + GCD[FALSE][ITE](gt0(z0, z1), z0, z1) + GT0(z0, z1) :|: z1 >= 0, z = 1, z0 >= 0, z' = z0, z'' = z1 GT0(z, z') -{ 1 }-> 1 :|: z0 >= 0, z = 0, z' = z0 GT0(z, z') -{ 1 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' = 0 GT0(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 GT0(z, z') -{ 1 }-> 1 + GT0(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0 LGTH(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 LGTH(z) -{ 1 }-> 1 + @'(1 + 0 + 0, lgth(z1)) + LGTH(z1) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 MONUS(z, z') -{ 1 }-> 1 + MONUS[ITE](eqList(lgth(z1), 1 + 0 + 0), z0, z1) + EQLIST(lgth(z1), 1 + 0 + 0) + LGTH(z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 MONUS[ITE](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 MONUS[ITE](z, z', z'') -{ 0 }-> 1 + MONUS(z1, z3) :|: z' = 1 + z0 + z1, z1 >= 0, z = 1, z0 >= 0, z'' = 1 + z2 + z3, z2 >= 0, z3 >= 0 and(z, z') -{ 0 }-> 2 :|: z = 2, z' = 2 and(z, z') -{ 0 }-> 1 :|: z = 1, z' = 1 and(z, z') -{ 0 }-> 1 :|: z = 2, z' = 1 and(z, z') -{ 0 }-> 1 :|: z' = 2, z = 1 and(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 eqList(z, z') -{ 0 }-> and(eqList(z0, z2), eqList(z1, z3)) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0 eqList(z, z') -{ 0 }-> 2 :|: z = 0, z' = 0 eqList(z, z') -{ 0 }-> 1 :|: z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z = 0 eqList(z, z') -{ 0 }-> 1 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' = 0 eqList(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 gt0(z, z') -{ 0 }-> gt0(z1, z3) :|: z1 >= 0, z' = 1 + z2 + z3, z0 >= 0, z = 1 + z0 + z1, z2 >= 0, z3 >= 0 gt0(z, z') -{ 0 }-> 2 :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1, z' = 0 gt0(z, z') -{ 0 }-> 1 :|: z0 >= 0, z = 0, z' = z0 gt0(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 lgth(z) -{ 0 }-> @(1 + 0 + 0, lgth(z1)) :|: z1 >= 0, z0 >= 0, z = 1 + z0 + z1 lgth(z) -{ 0 }-> 0 :|: z = 0 lgth(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 monus(z, z') -{ 0 }-> monus[Ite](eqList(lgth(z1), 1 + 0 + 0), z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0 monus(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 monus[Ite](z, z', z'') -{ 0 }-> z1 :|: z = 2, z'' = z2, z' = 1 + z0 + z1, z1 >= 0, z0 >= 0, z2 >= 0 monus[Ite](z, z', z'') -{ 0 }-> monus(z1, z3) :|: z' = 1 + z0 + z1, z1 >= 0, z = 1, z0 >= 0, z'' = 1 + z2 + z3, z2 >= 0, z3 >= 0 monus[Ite](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (21) CompleteCoflocoProof (FINISHED) Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo: eq(start(V1, V, V33),0,[fun(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V33),0,[fun1(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V33),0,[fun2(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V33),0,[fun5(V1, Out)],[V1 >= 0]). eq(start(V1, V, V33),0,[fun6(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V33),0,[fun4(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V33),0,[fun7(V1, V, V33, Out)],[V1 >= 0,V >= 0,V33 >= 0]). eq(start(V1, V, V33),0,[fun3(V1, V, V33, Out)],[V1 >= 0,V >= 0,V33 >= 0]). eq(start(V1, V, V33),0,[fun8(V1, V, V33, Out)],[V1 >= 0,V >= 0,V33 >= 0]). eq(start(V1, V, V33),0,[gt0(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V33),0,[monus(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V33),0,[fun9(V1, V, V33, Out)],[V1 >= 0,V >= 0,V33 >= 0]). eq(start(V1, V, V33),0,[eqList(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V33),0,[lgth(V1, Out)],[V1 >= 0]). eq(start(V1, V, V33),0,[fun10(V1, V, Out)],[V1 >= 0,V >= 0]). eq(start(V1, V, V33),0,[and(V1, V, Out)],[V1 >= 0,V >= 0]). eq(fun(V1, V, Out),1,[fun(V2, V4, Ret1)],[Out = 1 + Ret1,V2 >= 0,V = V4,V3 >= 0,V1 = 1 + V2 + V3,V4 >= 0]). eq(fun1(V1, V, Out),1,[],[Out = 0,V5 >= 0,V6 >= 0,V1 = 1 + V5 + V6,V = 0]). eq(fun1(V1, V, Out),1,[fun1(V8, V10, Ret11)],[Out = 1 + Ret11,V8 >= 0,V = 1 + V10 + V7,V9 >= 0,V1 = 1 + V8 + V9,V7 >= 0,V10 >= 0]). eq(fun1(V1, V, Out),1,[],[Out = 1,V11 >= 0,V1 = 0,V = V11]). eq(fun2(V1, V, Out),1,[],[Out = 0,V1 = 0,V = 0]). eq(fun2(V1, V, Out),1,[],[Out = 1,V = 1 + V12 + V13,V13 >= 0,V12 >= 0,V1 = 0]). eq(fun2(V1, V, Out),1,[],[Out = 2,V14 >= 0,V15 >= 0,V1 = 1 + V14 + V15,V = 0]). eq(fun2(V1, V, Out),1,[eqList(1 + V17 + V16, 1 + V18 + V19, Ret010),fun3(Ret010, 1 + V17 + V16, 1 + V18 + V19, Ret01),fun4(1 + V17 + V16, 1 + V18 + V19, Ret12)],[Out = 1 + Ret01 + Ret12,V16 >= 0,V = 1 + V18 + V19,V17 >= 0,V1 = 1 + V16 + V17,V18 >= 0,V19 >= 0]). eq(fun5(V1, Out),1,[lgth(V20, Ret011),fun(1 + 0 + 0, Ret011, Ret012),fun5(V20, Ret13)],[Out = 1 + Ret012 + Ret13,V20 >= 0,V21 >= 0,V1 = 1 + V20 + V21]). eq(fun6(V1, V, Out),1,[lgth(V22, Ret00100),eqList(Ret00100, 1 + 0 + 0, Ret0010),fun7(Ret0010, V23, V22, Ret001),lgth(V22, Ret0101),fun4(Ret0101, 1 + 0 + 0, Ret013),fun5(V22, Ret14)],[Out = 1 + Ret001 + Ret013 + Ret14,V1 = V23,V22 >= 0,V = V22,V23 >= 0]). eq(fun4(V1, V, Out),1,[fun4(V24, V26, Ret15)],[Out = 1 + Ret15,V27 >= 0,V = 1 + V25 + V26,V24 >= 0,V1 = 1 + V24 + V27,V26 >= 0,V25 >= 0]). eq(fun4(V1, V, Out),1,[fun4(V29, V28, Ret16)],[Out = 1 + Ret16,V29 >= 0,V = 1 + V28 + V31,V30 >= 0,V1 = 1 + V29 + V30,V31 >= 0,V28 >= 0]). eq(fun7(V1, V, V33, Out),0,[fun6(V35, V34, Ret17)],[Out = 1 + Ret17,V = 1 + V35 + V36,V35 >= 0,V1 = 1,V36 >= 0,V33 = 1 + V32 + V34,V32 >= 0,V34 >= 0]). eq(fun3(V1, V, V33, Out),0,[gt0(V37, V38, Ret0102),fun8(Ret0102, V37, V38, Ret014),fun1(V37, V38, Ret18)],[Out = 1 + Ret014 + Ret18,V38 >= 0,V1 = 1,V37 >= 0,V = V37,V33 = V38]). eq(fun8(V1, V, V33, Out),0,[monus(V40, V39, Ret0111),fun2(V39, Ret0111, Ret015),fun6(V40, V39, Ret19)],[Out = 1 + Ret015 + Ret19,V40 >= 0,V1 = 1,V39 >= 0,V = V39,V33 = V40]). eq(fun8(V1, V, V33, Out),0,[monus(V41, V42, Ret0103),fun2(Ret0103, V42, Ret016),fun6(V41, V42, Ret110)],[Out = 1 + Ret016 + Ret110,V1 = 2,V42 >= 0,V41 >= 0,V = V41,V33 = V42]). eq(gt0(V1, V, Out),0,[],[Out = 2,V43 >= 0,V44 >= 0,V1 = 1 + V43 + V44,V = 0]). eq(gt0(V1, V, Out),0,[gt0(V47, V46, Ret)],[Out = Ret,V47 >= 0,V = 1 + V45 + V46,V48 >= 0,V1 = 1 + V47 + V48,V45 >= 0,V46 >= 0]). eq(gt0(V1, V, Out),0,[],[Out = 1,V49 >= 0,V1 = 0,V = V49]). eq(monus(V1, V, Out),0,[lgth(V50, Ret00),eqList(Ret00, 1 + 0 + 0, Ret0),fun9(Ret0, V51, V50, Ret2)],[Out = Ret2,V1 = V51,V50 >= 0,V = V50,V51 >= 0]). eq(fun9(V1, V, V33, Out),0,[monus(V55, V52, Ret3)],[Out = Ret3,V = 1 + V53 + V55,V55 >= 0,V1 = 1,V53 >= 0,V33 = 1 + V52 + V54,V54 >= 0,V52 >= 0]). eq(fun9(V1, V, V33, Out),0,[],[Out = V58,V1 = 2,V33 = V57,V = 1 + V56 + V58,V58 >= 0,V56 >= 0,V57 >= 0]). eq(eqList(V1, V, Out),0,[eqList(V61, V62, Ret02),eqList(V59, V60, Ret111),and(Ret02, Ret111, Ret4)],[Out = Ret4,V59 >= 0,V = 1 + V60 + V62,V61 >= 0,V1 = 1 + V59 + V61,V62 >= 0,V60 >= 0]). eq(eqList(V1, V, Out),0,[],[Out = 1,V = 1 + V63 + V64,V63 >= 0,V64 >= 0,V1 = 0]). eq(eqList(V1, V, Out),0,[],[Out = 1,V66 >= 0,V65 >= 0,V1 = 1 + V65 + V66,V = 0]). eq(eqList(V1, V, Out),0,[],[Out = 2,V1 = 0,V = 0]). eq(lgth(V1, Out),0,[lgth(V67, Ret112),fun10(1 + 0 + 0, Ret112, Ret5)],[Out = Ret5,V67 >= 0,V68 >= 0,V1 = 1 + V67 + V68]). eq(lgth(V1, Out),0,[],[Out = 0,V1 = 0]). eq(fun10(V1, V, Out),0,[fun10(V70, V69, Ret113)],[Out = 1 + Ret113 + V71,V70 >= 0,V = V69,V71 >= 0,V1 = 1 + V70 + V71,V69 >= 0]). eq(fun10(V1, V, Out),0,[],[Out = V72,V72 >= 0,V1 = 0,V = V72]). eq(and(V1, V, Out),0,[],[Out = 1,V1 = 1,V = 1]). eq(and(V1, V, Out),0,[],[Out = 1,V1 = 2,V = 1]). eq(and(V1, V, Out),0,[],[Out = 1,V = 2,V1 = 1]). eq(and(V1, V, Out),0,[],[Out = 2,V1 = 2,V = 2]). eq(fun7(V1, V, V33, Out),0,[],[Out = 0,V74 >= 0,V33 = V75,V73 >= 0,V1 = V74,V = V73,V75 >= 0]). eq(fun3(V1, V, V33, Out),0,[],[Out = 0,V78 >= 0,V33 = V76,V77 >= 0,V1 = V78,V = V77,V76 >= 0]). eq(fun8(V1, V, V33, Out),0,[],[Out = 0,V81 >= 0,V33 = V79,V80 >= 0,V1 = V81,V = V80,V79 >= 0]). eq(gt0(V1, V, Out),0,[],[Out = 0,V82 >= 0,V83 >= 0,V1 = V82,V = V83]). eq(monus(V1, V, Out),0,[],[Out = 0,V85 >= 0,V84 >= 0,V1 = V85,V = V84]). eq(fun9(V1, V, V33, Out),0,[],[Out = 0,V87 >= 0,V33 = V88,V86 >= 0,V1 = V87,V = V86,V88 >= 0]). eq(eqList(V1, V, Out),0,[],[Out = 0,V90 >= 0,V89 >= 0,V1 = V90,V = V89]). eq(lgth(V1, Out),0,[],[Out = 0,V91 >= 0,V1 = V91]). eq(fun10(V1, V, Out),0,[],[Out = 0,V92 >= 0,V93 >= 0,V1 = V92,V = V93]). eq(and(V1, V, Out),0,[],[Out = 0,V95 >= 0,V94 >= 0,V1 = V95,V = V94]). eq(fun(V1, V, Out),0,[],[Out = 0,V96 >= 0,V97 >= 0,V1 = V96,V = V97]). eq(fun1(V1, V, Out),0,[],[Out = 0,V98 >= 0,V99 >= 0,V1 = V98,V = V99]). eq(fun2(V1, V, Out),0,[],[Out = 0,V100 >= 0,V101 >= 0,V1 = V100,V = V101]). eq(fun5(V1, Out),0,[],[Out = 0,V102 >= 0,V1 = V102]). eq(fun4(V1, V, Out),0,[],[Out = 0,V104 >= 0,V103 >= 0,V1 = V104,V = V103]). input_output_vars(fun(V1,V,Out),[V1,V],[Out]). input_output_vars(fun1(V1,V,Out),[V1,V],[Out]). input_output_vars(fun2(V1,V,Out),[V1,V],[Out]). input_output_vars(fun5(V1,Out),[V1],[Out]). input_output_vars(fun6(V1,V,Out),[V1,V],[Out]). input_output_vars(fun4(V1,V,Out),[V1,V],[Out]). input_output_vars(fun7(V1,V,V33,Out),[V1,V,V33],[Out]). input_output_vars(fun3(V1,V,V33,Out),[V1,V,V33],[Out]). input_output_vars(fun8(V1,V,V33,Out),[V1,V,V33],[Out]). input_output_vars(gt0(V1,V,Out),[V1,V],[Out]). input_output_vars(monus(V1,V,Out),[V1,V],[Out]). input_output_vars(fun9(V1,V,V33,Out),[V1,V,V33],[Out]). input_output_vars(eqList(V1,V,Out),[V1,V],[Out]). input_output_vars(lgth(V1,Out),[V1],[Out]). input_output_vars(fun10(V1,V,Out),[V1,V],[Out]). input_output_vars(and(V1,V,Out),[V1,V],[Out]). CoFloCo proof output: Preprocessing Cost Relations ===================================== #### Computed strongly connected components 0. non_recursive : [and/3] 1. recursive [non_tail,multiple] : [eqList/3] 2. recursive : [fun/3] 3. recursive : [fun1/3] 4. recursive : [fun10/3] 5. recursive : [fun4/3] 6. recursive [non_tail] : [lgth/2] 7. recursive : [fun5/2] 8. recursive [non_tail] : [fun6/3,fun7/4] 9. recursive : [fun9/4,monus/3] 10. recursive : [gt0/3] 11. recursive [non_tail] : [fun2/3,fun3/4,fun8/4] 12. non_recursive : [start/3] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into and/3 1. SCC is partially evaluated into eqList/3 2. SCC is partially evaluated into fun/3 3. SCC is partially evaluated into fun1/3 4. SCC is partially evaluated into fun10/3 5. SCC is partially evaluated into fun4/3 6. SCC is partially evaluated into lgth/2 7. SCC is partially evaluated into fun5/2 8. SCC is partially evaluated into fun6/3 9. SCC is partially evaluated into monus/3 10. SCC is partially evaluated into gt0/3 11. SCC is partially evaluated into fun2/3 12. SCC is partially evaluated into start/3 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations and/3 * CE 63 is refined into CE [64] * CE 62 is refined into CE [65] * CE 60 is refined into CE [66] * CE 61 is refined into CE [67] * CE 59 is refined into CE [68] ### Cost equations --> "Loop" of and/3 * CEs [64] --> Loop 42 * CEs [65] --> Loop 43 * CEs [66] --> Loop 44 * CEs [67] --> Loop 45 * CEs [68] --> Loop 46 ### Ranking functions of CR and(V1,V,Out) #### Partial ranking functions of CR and(V1,V,Out) ### Specialization of cost equations eqList/3 * CE 53 is refined into CE [69] * CE 51 is refined into CE [70] * CE 50 is refined into CE [71] * CE 52 is refined into CE [72] * CE 49 is refined into CE [73,74,75,76,77] ### Cost equations --> "Loop" of eqList/3 * CEs [76] --> Loop 47 * CEs [75] --> Loop 48 * CEs [74] --> Loop 49 * CEs [73] --> Loop 50 * CEs [77] --> Loop 51 * CEs [69] --> Loop 52 * CEs [70] --> Loop 53 * CEs [71] --> Loop 54 * CEs [72] --> Loop 55 ### Ranking functions of CR eqList(V1,V,Out) * RF of phase [47]: [V,V1] * RF of phase [48,49,50]: [V,V1] * RF of phase [51]: [V,V1] #### Partial ranking functions of CR eqList(V1,V,Out) * Partial RF of phase [47]: - RF of loop [47:1,47:2]: V V1 * Partial RF of phase [48,49,50]: - RF of loop [48:1,48:2,49:1,49:2,50:1,50:2]: V V1 * Partial RF of phase [51]: - RF of loop [51:1,51:2]: V V1 ### Specialization of cost equations fun/3 * CE 44 is refined into CE [78] * CE 43 is refined into CE [79] ### Cost equations --> "Loop" of fun/3 * CEs [79] --> Loop 56 * CEs [78] --> Loop 57 ### Ranking functions of CR fun(V1,V,Out) * RF of phase [56]: [V1] #### Partial ranking functions of CR fun(V1,V,Out) * Partial RF of phase [56]: - RF of loop [56:1]: V1 ### Specialization of cost equations fun1/3 * CE 25 is refined into CE [80] * CE 28 is refined into CE [81] * CE 27 is refined into CE [82] * CE 26 is refined into CE [83] ### Cost equations --> "Loop" of fun1/3 * CEs [83] --> Loop 58 * CEs [80,81] --> Loop 59 * CEs [82] --> Loop 60 ### Ranking functions of CR fun1(V1,V,Out) * RF of phase [58]: [V,V1] #### Partial ranking functions of CR fun1(V1,V,Out) * Partial RF of phase [58]: - RF of loop [58:1]: V V1 ### Specialization of cost equations fun10/3 * CE 58 is refined into CE [84] * CE 57 is refined into CE [85] * CE 56 is refined into CE [86] ### Cost equations --> "Loop" of fun10/3 * CEs [86] --> Loop 61 * CEs [84] --> Loop 62 * CEs [85] --> Loop 63 ### Ranking functions of CR fun10(V1,V,Out) * RF of phase [61]: [V1] #### Partial ranking functions of CR fun10(V1,V,Out) * Partial RF of phase [61]: - RF of loop [61:1]: V1 ### Specialization of cost equations fun4/3 * CE 48 is refined into CE [87] * CE 47 is refined into CE [88] ### Cost equations --> "Loop" of fun4/3 * CEs [88] --> Loop 64 * CEs [87] --> Loop 65 ### Ranking functions of CR fun4(V1,V,Out) * RF of phase [64]: [V,V1] #### Partial ranking functions of CR fun4(V1,V,Out) * Partial RF of phase [64]: - RF of loop [64:1]: V V1 ### Specialization of cost equations lgth/2 * CE 55 is refined into CE [89] * CE 54 is refined into CE [90,91,92] ### Cost equations --> "Loop" of lgth/2 * CEs [91] --> Loop 66 * CEs [92] --> Loop 67 * CEs [90] --> Loop 68 * CEs [89] --> Loop 69 ### Ranking functions of CR lgth(V1,Out) * RF of phase [66,67,68]: [V1] #### Partial ranking functions of CR lgth(V1,Out) * Partial RF of phase [66,67,68]: - RF of loop [66:1,67:1,68:1]: V1 ### Specialization of cost equations fun5/2 * CE 46 is refined into CE [93] * CE 45 is refined into CE [94,95,96,97] ### Cost equations --> "Loop" of fun5/2 * CEs [95,97] --> Loop 70 * CEs [94,96] --> Loop 71 * CEs [93] --> Loop 72 ### Ranking functions of CR fun5(V1,Out) * RF of phase [70,71]: [V1] #### Partial ranking functions of CR fun5(V1,Out) * Partial RF of phase [70,71]: - RF of loop [70:1,71:1]: V1 ### Specialization of cost equations fun6/3 * CE 42 is refined into CE [98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115] * CE 41 is refined into CE [116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151] ### Cost equations --> "Loop" of fun6/3 * CEs [121,127,133,139,145,151] --> Loop 73 * CEs [117,119,120,123,125,126,129,131,132,135,137,138,141,143,144,147,149,150] --> Loop 74 * CEs [116,118,122,124,128,130,134,136,140,142,146,148] --> Loop 75 * CEs [103,109,115] --> Loop 76 * CEs [111,113] --> Loop 77 * CEs [99,101,102,105,107,108,114] --> Loop 78 * CEs [98,100,104,106,110,112] --> Loop 79 ### Ranking functions of CR fun6(V1,V,Out) * RF of phase [76,77,78,79]: [V,V1] #### Partial ranking functions of CR fun6(V1,V,Out) * Partial RF of phase [76,77,78,79]: - RF of loop [76:1,77:1,78:1,79:1]: V1 - RF of loop [76:1,78:1,79:1]: V - RF of loop [77:1]: V-1 ### Specialization of cost equations monus/3 * CE 30 is refined into CE [152] * CE 29 is refined into CE [153,154,155,156,157,158] * CE 32 is refined into CE [159] * CE 31 is refined into CE [160,161,162] ### Cost equations --> "Loop" of monus/3 * CEs [160,161,162] --> Loop 80 * CEs [152] --> Loop 81 * CEs [153,154,155,156,157,158,159] --> Loop 82 ### Ranking functions of CR monus(V1,V,Out) * RF of phase [80]: [V,V1] #### Partial ranking functions of CR monus(V1,V,Out) * Partial RF of phase [80]: - RF of loop [80:1]: V V1 ### Specialization of cost equations gt0/3 * CE 24 is refined into CE [163] * CE 21 is refined into CE [164] * CE 23 is refined into CE [165] * CE 22 is refined into CE [166] ### Cost equations --> "Loop" of gt0/3 * CEs [166] --> Loop 83 * CEs [163] --> Loop 84 * CEs [164] --> Loop 85 * CEs [165] --> Loop 86 ### Ranking functions of CR gt0(V1,V,Out) * RF of phase [83]: [V,V1] #### Partial ranking functions of CR gt0(V1,V,Out) * Partial RF of phase [83]: - RF of loop [83:1]: V V1 ### Specialization of cost equations fun2/3 * CE 33 is refined into CE [167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184] * CE 36 is refined into CE [185,186,187,188,189,190] * CE 39 is refined into CE [191] * CE 38 is refined into CE [192] * CE 37 is refined into CE [193] * CE 40 is refined into CE [194] * CE 34 is refined into CE [195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,222,223,224,225,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242] * CE 35 is refined into CE [243,244,245,246,247,248,249,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265,266,267,268,269,270,271,272,273,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290] ### Cost equations --> "Loop" of fun2/3 * CEs [248,250,251,252,253,254,255,256,257,258,259,260,261,262,263,264,265,266,272,274,275,276,277,278,279,280,281,282,283,284,285,286,287,288,289,290] --> Loop 87 * CEs [244,245,246,247,249,268,269,270,271,273] --> Loop 88 * CEs [243,267] --> Loop 89 * CEs [200,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,224,226,227,228,229,230,231,232,233,234,235,236,237,238,239,240,241,242] --> Loop 90 * CEs [196,197,198,199,201,220,221,222,223,225] --> Loop 91 * CEs [195,219] --> Loop 92 * CEs [171,177] --> Loop 93 * CEs [172,178,184] --> Loop 94 * CEs [170,176,182,183] --> Loop 95 * CEs [168,169,174,175,180,181] --> Loop 96 * CEs [190] --> Loop 97 * CEs [167,173,179,186,188] --> Loop 98 * CEs [185,187,189] --> Loop 99 * CEs [191] --> Loop 100 * CEs [192] --> Loop 101 * CEs [193,194] --> Loop 102 ### Ranking functions of CR fun2(V1,V,Out) * RF of phase [87,88,89,90,91,92]: [V1+V-2,V1+3*V-4,V1+3/2*V-3,2*V1+V-3] #### Partial ranking functions of CR fun2(V1,V,Out) * Partial RF of phase [87,88,89,90,91,92]: - RF of loop [87:1,88:1,89:1]: V V1+V-2 - RF of loop [90:1,91:1,92:1]: V1-1 ### Specialization of cost equations start/3 * CE 4 is refined into CE [291,292,293,294,295,296,297,298,299,300,301,302,303,304,305,306,307,308,309,310,311,312,313,314,315,316,317,318,319,320,321,322] * CE 1 is refined into CE [323,324,325,326,327,328,329,330,331,332,333,334,335] * CE 2 is refined into CE [336] * CE 3 is refined into CE [337,338,339,340,341,342,343,344,345,346,347,348,349,350,351,352,353,354,355,356,357,358,359,360,361,362,363,364,365,366,367,368,369,370,371,372,373,374,375,376,377,378,379,380,381,382,383,384,385,386,387,388,389,390,391,392,393,394,395,396,397,398,399,400,401,402,403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430,431,432,433] * CE 5 is refined into CE [434,435,436,437,438,439,440,441,442,443,444,445,446,447,448,449,450,451,452,453,454,455,456,457,458,459,460,461,462,463,464,465,466,467,468,469,470,471,472,473,474,475,476,477,478,479,480,481,482,483,484,485,486,487,488,489,490,491,492,493,494,495,496,497,498,499,500,501,502,503,504,505,506,507,508,509,510,511,512,513,514,515,516,517,518,519,520,521,522,523,524,525,526,527,528,529,530,531] * CE 6 is refined into CE [532,533,534,535,536,537,538,539,540,541,542,543,544,545,546,547,548,549,550,551,552,553,554,555,556,557,558,559,560,561,562,563] * CE 7 is refined into CE [564,565] * CE 8 is refined into CE [566,567,568,569] * CE 9 is refined into CE [570,571] * CE 10 is refined into CE [572,573,574,575] * CE 11 is refined into CE [576,577,578,579,580,581,582] * CE 12 is refined into CE [583,584] * CE 13 is refined into CE [585,586,587,588] * CE 14 is refined into CE [589,590] * CE 15 is refined into CE [591,592,593,594,595] * CE 16 is refined into CE [596,597] * CE 17 is refined into CE [598,599,600,601,602,603] * CE 18 is refined into CE [604,605] * CE 19 is refined into CE [606,607,608,609] * CE 20 is refined into CE [610,611,612,613,614] ### Cost equations --> "Loop" of start/3 * CEs [577,592,600] --> Loop 103 * CEs [291,292,293,294,295,296,297,298,299,300,301,302,303,304,305,306,307,308,309,310,311,312,313,314,315,316,317,318,319,320,321,322] --> Loop 104 * CEs [613] --> Loop 105 * CEs [612] --> Loop 106 * CEs [325,337] --> Loop 107 * CEs [611] --> Loop 108 * CEs [603,610] --> Loop 109 * CEs [323,324,326,327,328,329,330,331,332,333,334,335,338,339,340,341,342,343,344,345,346,347,348,349,350,351,352,353,354,355,356,357,358,359,360,361,362,363,364,365,366,367,368,369,370,371,372,373,374,375,376,377,378,379,380,381,382,383,384,385,386,387,388,389,390,391,392,393,394,395,396,397,398,399,400,401,402,403,404,405,406,407,408,409,410,411,412,413,414,415,416,417,418,419,420,421,422,423,424,425,426,427,428,429,430,431,432,433,434,435,436,437,438,439,440,441,442,443,444,445,446,447,448,449,450,451,452,453,454,455,456,457,458,459,460,461,462,463,464,465,466,467,468,469,470,471,472,473,474,475,476,477,478,479,480,481,482,483,484,485,486,487,488,489,490,491,492,493,494,495,496,497,498,499,500,501,502,503,504,505,506,507,508,509,510,511,512,513,514,515,516,517,518,519,520,521,522,523,524,525,526,527,528,529,530,531,532,533,534,535,536,537,538,539,540,541,542,543,544,545,546,547,548,549,550,551,552,553,554,555,556,557,558,559,560,561,562,563,564,565,566,567,568,569] --> Loop 110 * CEs [336,570,571,572,573,574,575,576,578,579,580,581,582,583,584,585,586,587,588,589,590,591,593,594,595,596,597,598,599,601,602,604,605,606,607,608,609,614] --> Loop 111 ### Ranking functions of CR start(V1,V,V33) #### Partial ranking functions of CR start(V1,V,V33) Computing Bounds ===================================== #### Cost of chains of and(V1,V,Out): * Chain [46]: 0 with precondition: [V1=1,V=1,Out=1] * Chain [45]: 0 with precondition: [V1=1,V=2,Out=1] * Chain [44]: 0 with precondition: [V1=2,V=1,Out=1] * Chain [43]: 0 with precondition: [V1=2,V=2,Out=2] * Chain [42]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of eqList(V1,V,Out): * Chain [55]: 0 with precondition: [V1=0,V=0,Out=2] * Chain [54]: 0 with precondition: [V1=0,Out=1,V>=1] * Chain [53]: 0 with precondition: [V=0,Out=1,V1>=1] * Chain [52]: 0 with precondition: [Out=0,V1>=0,V>=0] * Chain [multiple([51],[[multiple([48,49,50],[[multiple([47],[[55]])],[55],[54],[53]])],[multiple([47],[[55]])],[55],[54],[53],[52]])]: 0 with precondition: [Out=0,V1>=1,V>=1] * Chain [multiple([48,49,50],[[multiple([47],[[55]])],[55],[54],[53]])]: 0 with precondition: [Out=1,V1>=1,V>=1,V+V1>=3] * Chain [multiple([47],[[55]])]: 0 with precondition: [Out=2,V1=V,V1>=1] #### Cost of chains of fun(V1,V,Out): * Chain [[56],57]: 1*it(56)+0 Such that:it(56) =< V1 with precondition: [V>=0,Out>=1,V1>=Out] * Chain [57]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of fun1(V1,V,Out): * Chain [[58],60]: 1*it(58)+1 Such that:it(58) =< V with precondition: [Out>=2,V1+1>=Out,V+1>=Out] * Chain [[58],59]: 1*it(58)+1 Such that:it(58) =< V with precondition: [Out>=1,V1>=Out,V>=Out] * Chain [60]: 1 with precondition: [V1=0,Out=1,V>=0] * Chain [59]: 1 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of fun10(V1,V,Out): * Chain [[61],63]: 0 with precondition: [V+V1=Out,V1>=1,V>=0] * Chain [[61],62]: 0 with precondition: [V>=0,Out>=1,V1>=Out] * Chain [63]: 0 with precondition: [V1=0,V=Out,V>=0] * Chain [62]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of fun4(V1,V,Out): * Chain [[64],65]: 1*it(64)+0 Such that:it(64) =< V with precondition: [Out>=1,V1>=Out,V>=Out] * Chain [65]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of lgth(V1,Out): * Chain [[66,67,68],69]: 0 with precondition: [V1>=1,Out>=0,V1>=Out] * Chain [69]: 0 with precondition: [Out=0,V1>=0] #### Cost of chains of fun5(V1,Out): * Chain [[70,71],72]: 4*it(70)+0 Such that:aux(19) =< V1 it(70) =< aux(19) with precondition: [V1>=1,Out>=1,2*V1>=Out] * Chain [72]: 0 with precondition: [Out=0,V1>=0] #### Cost of chains of fun6(V1,V,Out): * Chain [[76,77,78,79],75]: 4*it(76)+6*s(37)+12*s(38)+24*s(41)+1 Such that:aux(34) =< V1 aux(35) =< V aux(25) =< aux(34) it(76) =< aux(34) aux(25) =< aux(35) it(76) =< aux(35) aux(27) =< aux(35) s(39) =< it(76)*aux(35) s(42) =< it(76)*aux(27) s(37) =< aux(25) s(41) =< s(42) s(38) =< s(39) with precondition: [V1>=1,V>=1,Out>=3] * Chain [[76,77,78,79],74]: 4*it(76)+6*s(37)+12*s(38)+24*s(41)+48*s(48)+6*s(51)+1 Such that:aux(36) =< 1 aux(38) =< V1 aux(39) =< V s(51) =< aux(36) s(48) =< aux(39) aux(25) =< aux(38) it(76) =< aux(38) aux(25) =< aux(39) it(76) =< aux(39) aux(27) =< aux(39) s(39) =< it(76)*aux(39) s(42) =< it(76)*aux(27) s(37) =< aux(25) s(41) =< s(42) s(38) =< s(39) with precondition: [V1>=1,V>=2,Out>=4] * Chain [[76,77,78,79],73]: 4*it(76)+6*s(37)+12*s(38)+24*s(41)+6*s(77)+24*s(79)+1 Such that:aux(40) =< 1 aux(42) =< V1 aux(43) =< V s(77) =< aux(40) s(79) =< aux(43) aux(25) =< aux(42) it(76) =< aux(42) aux(25) =< aux(43) it(76) =< aux(43) aux(27) =< aux(43) s(39) =< it(76)*aux(43) s(42) =< it(76)*aux(27) s(37) =< aux(25) s(41) =< s(42) s(38) =< s(39) with precondition: [V1>=1,V>=2,Out>=5] * Chain [75]: 1 with precondition: [Out=1,V1>=0,V>=0] * Chain [74]: 48*s(48)+6*s(51)+1 Such that:aux(36) =< 1 aux(37) =< V s(51) =< aux(36) s(48) =< aux(37) with precondition: [V1>=0,V>=1,Out>=2,2*V+1>=Out] * Chain [73]: 6*s(77)+24*s(79)+1 Such that:aux(40) =< 1 aux(41) =< V s(77) =< aux(40) s(79) =< aux(41) with precondition: [V1>=0,V>=1,Out>=3,2*V+2>=Out] #### Cost of chains of monus(V1,V,Out): * Chain [[80],82]: 0 with precondition: [Out=0,V1>=1,V>=1] * Chain [[80],81]: 0 with precondition: [V>=2,Out>=0,V1>=Out+2] * Chain [82]: 0 with precondition: [Out=0,V1>=0,V>=0] * Chain [81]: 0 with precondition: [V>=1,Out>=0,V1>=Out+1] #### Cost of chains of gt0(V1,V,Out): * Chain [[83],86]: 0 with precondition: [Out=1,V1>=1,V>=1] * Chain [[83],85]: 0 with precondition: [Out=2,V1>=2,V>=1] * Chain [[83],84]: 0 with precondition: [Out=0,V1>=1,V>=1] * Chain [86]: 0 with precondition: [V1=0,Out=1,V>=0] * Chain [85]: 0 with precondition: [V=0,Out=2,V1>=1] * Chain [84]: 0 with precondition: [Out=0,V1>=0,V>=0] #### Cost of chains of fun2(V1,V,Out): * Chain [[87,88,89,90,91,92],102]: 9*it(87)+9*it(90)+56*s(788)+288*s(789)+1728*s(790)+144*s(791)+216*s(792)+864*s(793)+432*s(794)+1784*s(811)+288*s(812)+144*s(813)+216*s(814)+864*s(815)+432*s(816)+1 Such that:aux(127) =< V1 aux(132) =< V1+3/2*V aux(135) =< 2*V1+V aux(136) =< 2*V1+2*V aux(137) =< V aux(139) =< V1+V aux(140) =< V1+3*V aux(141) =< 3*V1+3*V aux(122) =< aux(127) it(90) =< aux(127) aux(114) =< aux(139) aux(122) =< aux(139) it(87) =< aux(139) it(90) =< aux(139) aux(114) =< aux(140) aux(122) =< aux(140) it(87) =< aux(140) it(90) =< aux(140) aux(114) =< aux(141) aux(122) =< aux(141) it(87) =< aux(141) it(90) =< aux(141) aux(114) =< aux(132) aux(122) =< aux(132) it(87) =< aux(132) it(90) =< aux(132) aux(114) =< aux(135) aux(122) =< aux(135) it(87) =< aux(135) it(90) =< aux(135) aux(114) =< aux(136) aux(122) =< aux(136) it(87) =< aux(136) it(90) =< aux(136) aux(114) =< aux(137) it(87) =< aux(137) aux(116) =< aux(137) aux(115) =< aux(127) s(820) =< it(90)*aux(116) s(821) =< it(90)*aux(115) s(796) =< it(87)*aux(115) s(801) =< it(87)*aux(116) s(811) =< s(820) s(812) =< aux(122) s(819) =< s(821) s(813) =< s(821) s(819) =< s(820) s(813) =< s(820) s(817) =< s(813)*aux(137) s(818) =< s(813)*aux(116) s(814) =< s(819) s(815) =< s(818) s(816) =< s(817) s(788) =< s(801) s(789) =< aux(114) s(790) =< s(796) s(799) =< s(801) s(791) =< s(801) s(799) =< s(796) s(791) =< s(796) s(797) =< s(791)*aux(127) s(798) =< s(791)*aux(115) s(792) =< s(799) s(793) =< s(798) s(794) =< s(797) with precondition: [V1>=1,V>=1,Out>=4,V+V1>=3] * Chain [[87,88,89,90,91,92],101]: 9*it(87)+9*it(90)+56*s(788)+288*s(789)+1728*s(790)+144*s(791)+216*s(792)+864*s(793)+432*s(794)+1784*s(811)+288*s(812)+144*s(813)+216*s(814)+864*s(815)+432*s(816)+1 Such that:aux(142) =< V1 aux(143) =< V1+V aux(144) =< V1+3*V aux(145) =< V1+3/2*V aux(146) =< 2*V1+V aux(147) =< V aux(122) =< aux(142) it(90) =< aux(142) aux(114) =< aux(143) aux(122) =< aux(143) it(87) =< aux(143) it(90) =< aux(143) aux(114) =< aux(144) aux(122) =< aux(144) it(87) =< aux(144) it(90) =< aux(144) aux(114) =< aux(145) aux(122) =< aux(145) it(87) =< aux(145) it(90) =< aux(145) aux(114) =< aux(146) aux(122) =< aux(146) it(87) =< aux(146) it(90) =< aux(146) aux(114) =< aux(147) it(87) =< aux(147) aux(116) =< aux(147) aux(115) =< aux(142) s(820) =< it(90)*aux(116) s(821) =< it(90)*aux(115) s(796) =< it(87)*aux(115) s(801) =< it(87)*aux(116) s(811) =< s(820) s(812) =< aux(122) s(819) =< s(821) s(813) =< s(821) s(819) =< s(820) s(813) =< s(820) s(817) =< s(813)*aux(147) s(818) =< s(813)*aux(116) s(814) =< s(819) s(815) =< s(818) s(816) =< s(817) s(788) =< s(801) s(789) =< aux(114) s(790) =< s(796) s(799) =< s(801) s(791) =< s(801) s(799) =< s(796) s(791) =< s(796) s(797) =< s(791)*aux(142) s(798) =< s(791)*aux(115) s(792) =< s(799) s(793) =< s(798) s(794) =< s(797) with precondition: [V1>=2,V>=1,Out>=5] * Chain [[87,88,89,90,91,92],100]: 9*it(87)+9*it(90)+56*s(788)+288*s(789)+1728*s(790)+144*s(791)+216*s(792)+864*s(793)+432*s(794)+1784*s(811)+288*s(812)+144*s(813)+216*s(814)+864*s(815)+432*s(816)+1 Such that:aux(148) =< V1 aux(149) =< V1+V aux(150) =< V1+3*V aux(151) =< V1+3/2*V aux(152) =< 2*V1+V aux(153) =< V aux(122) =< aux(148) it(90) =< aux(148) aux(114) =< aux(149) aux(122) =< aux(149) it(87) =< aux(149) it(90) =< aux(149) aux(114) =< aux(150) aux(122) =< aux(150) it(87) =< aux(150) it(90) =< aux(150) aux(114) =< aux(151) aux(122) =< aux(151) it(87) =< aux(151) it(90) =< aux(151) aux(114) =< aux(152) aux(122) =< aux(152) it(87) =< aux(152) it(90) =< aux(152) aux(114) =< aux(153) it(87) =< aux(153) aux(116) =< aux(153) aux(115) =< aux(148) s(820) =< it(90)*aux(116) s(821) =< it(90)*aux(115) s(796) =< it(87)*aux(115) s(801) =< it(87)*aux(116) s(811) =< s(820) s(812) =< aux(122) s(819) =< s(821) s(813) =< s(821) s(819) =< s(820) s(813) =< s(820) s(817) =< s(813)*aux(153) s(818) =< s(813)*aux(116) s(814) =< s(819) s(815) =< s(818) s(816) =< s(817) s(788) =< s(801) s(789) =< aux(114) s(790) =< s(796) s(799) =< s(801) s(791) =< s(801) s(799) =< s(796) s(791) =< s(796) s(797) =< s(791)*aux(148) s(798) =< s(791)*aux(115) s(792) =< s(799) s(793) =< s(798) s(794) =< s(797) with precondition: [V1>=1,V>=1,Out>=6,V+V1>=3] * Chain [[87,88,89,90,91,92],99]: 9*it(87)+9*it(90)+56*s(788)+288*s(789)+1728*s(790)+144*s(791)+216*s(792)+864*s(793)+432*s(794)+1784*s(811)+288*s(812)+144*s(813)+216*s(814)+864*s(815)+432*s(816)+1 Such that:aux(154) =< V1 aux(155) =< V1+V aux(156) =< V1+3*V aux(157) =< V1+3/2*V aux(158) =< 2*V1+V aux(159) =< V aux(122) =< aux(154) it(90) =< aux(154) aux(114) =< aux(155) aux(122) =< aux(155) it(87) =< aux(155) it(90) =< aux(155) aux(114) =< aux(156) aux(122) =< aux(156) it(87) =< aux(156) it(90) =< aux(156) aux(114) =< aux(157) aux(122) =< aux(157) it(87) =< aux(157) it(90) =< aux(157) aux(114) =< aux(158) aux(122) =< aux(158) it(87) =< aux(158) it(90) =< aux(158) aux(114) =< aux(159) it(87) =< aux(159) aux(116) =< aux(159) aux(115) =< aux(154) s(820) =< it(90)*aux(116) s(821) =< it(90)*aux(115) s(796) =< it(87)*aux(115) s(801) =< it(87)*aux(116) s(811) =< s(820) s(812) =< aux(122) s(819) =< s(821) s(813) =< s(821) s(819) =< s(820) s(813) =< s(820) s(817) =< s(813)*aux(159) s(818) =< s(813)*aux(116) s(814) =< s(819) s(815) =< s(818) s(816) =< s(817) s(788) =< s(801) s(789) =< aux(114) s(790) =< s(796) s(799) =< s(801) s(791) =< s(801) s(799) =< s(796) s(791) =< s(796) s(797) =< s(791)*aux(154) s(798) =< s(791)*aux(115) s(792) =< s(799) s(793) =< s(798) s(794) =< s(797) with precondition: [V1>=1,V>=1,Out>=5,V+V1>=3] * Chain [[87,88,89,90,91,92],98]: 9*it(87)+9*it(90)+56*s(788)+288*s(789)+1728*s(790)+144*s(791)+216*s(792)+864*s(793)+432*s(794)+1784*s(811)+288*s(812)+144*s(813)+216*s(814)+864*s(815)+432*s(816)+2*s(827)+2 Such that:aux(132) =< V1+3/2*V aux(133) =< 2*V1+3*V aux(161) =< V1 aux(162) =< V1+V aux(163) =< V1+3*V aux(164) =< 2*V1+V aux(165) =< V s(827) =< aux(165) aux(122) =< aux(161) it(90) =< aux(161) aux(114) =< aux(162) aux(122) =< aux(162) it(87) =< aux(162) it(90) =< aux(162) aux(114) =< aux(163) aux(122) =< aux(163) it(87) =< aux(163) it(90) =< aux(163) aux(114) =< aux(132) aux(122) =< aux(132) it(87) =< aux(132) it(90) =< aux(132) aux(114) =< aux(133) aux(122) =< aux(133) it(87) =< aux(133) it(90) =< aux(133) aux(114) =< aux(164) aux(122) =< aux(164) it(87) =< aux(164) it(90) =< aux(164) aux(114) =< aux(165) it(87) =< aux(165) aux(116) =< aux(165) aux(115) =< aux(161) s(820) =< it(90)*aux(116) s(821) =< it(90)*aux(115) s(796) =< it(87)*aux(115) s(801) =< it(87)*aux(116) s(811) =< s(820) s(812) =< aux(122) s(819) =< s(821) s(813) =< s(821) s(819) =< s(820) s(813) =< s(820) s(817) =< s(813)*aux(165) s(818) =< s(813)*aux(116) s(814) =< s(819) s(815) =< s(818) s(816) =< s(817) s(788) =< s(801) s(789) =< aux(114) s(790) =< s(796) s(799) =< s(801) s(791) =< s(801) s(799) =< s(796) s(791) =< s(796) s(797) =< s(791)*aux(161) s(798) =< s(791)*aux(115) s(792) =< s(799) s(793) =< s(798) s(794) =< s(797) with precondition: [V1>=1,V>=1,Out>=6,V+V1>=3] * Chain [[87,88,89,90,91,92],97]: 9*it(87)+9*it(90)+56*s(788)+288*s(789)+1728*s(790)+144*s(791)+216*s(792)+864*s(793)+432*s(794)+1784*s(811)+288*s(812)+144*s(813)+216*s(814)+864*s(815)+432*s(816)+1*s(829)+1 Such that:aux(132) =< V1+3/2*V aux(133) =< 2*V1+3*V aux(166) =< V1 aux(167) =< V1+V aux(168) =< V1+3*V aux(169) =< 2*V1+V aux(170) =< V s(829) =< aux(169) aux(122) =< aux(166) it(90) =< aux(166) aux(114) =< aux(167) aux(122) =< aux(167) it(87) =< aux(167) it(90) =< aux(167) aux(114) =< aux(168) aux(122) =< aux(168) it(87) =< aux(168) it(90) =< aux(168) aux(114) =< aux(132) aux(122) =< aux(132) it(87) =< aux(132) it(90) =< aux(132) aux(114) =< aux(133) aux(122) =< aux(133) it(87) =< aux(133) it(90) =< aux(133) aux(114) =< aux(169) aux(122) =< aux(169) it(87) =< aux(169) it(90) =< aux(169) aux(114) =< aux(170) it(87) =< aux(170) aux(116) =< aux(170) aux(115) =< aux(166) s(820) =< it(90)*aux(116) s(821) =< it(90)*aux(115) s(796) =< it(87)*aux(115) s(801) =< it(87)*aux(116) s(811) =< s(820) s(812) =< aux(122) s(819) =< s(821) s(813) =< s(821) s(819) =< s(820) s(813) =< s(820) s(817) =< s(813)*aux(170) s(818) =< s(813)*aux(116) s(814) =< s(819) s(815) =< s(818) s(816) =< s(817) s(788) =< s(801) s(789) =< aux(114) s(790) =< s(796) s(799) =< s(801) s(791) =< s(801) s(799) =< s(796) s(791) =< s(796) s(797) =< s(791)*aux(166) s(798) =< s(791)*aux(115) s(792) =< s(799) s(793) =< s(798) s(794) =< s(797) with precondition: [V1>=1,V>=1,Out>=6,V+V1>=3] * Chain [[87,88,89,90,91,92],96]: 9*it(87)+9*it(90)+56*s(788)+288*s(789)+1728*s(790)+144*s(791)+216*s(792)+864*s(793)+432*s(794)+1784*s(811)+288*s(812)+144*s(813)+216*s(814)+864*s(815)+432*s(816)+6*s(830)+2 Such that:aux(127) =< V1 aux(130) =< V1+3*V aux(132) =< V1+3/2*V aux(135) =< 2*V1+V aux(136) =< 4*V1+4*V aux(172) =< V1+V aux(173) =< 3*V1+3*V aux(174) =< V s(830) =< aux(174) aux(122) =< aux(127) it(90) =< aux(127) aux(114) =< aux(172) aux(122) =< aux(172) it(87) =< aux(172) it(90) =< aux(172) aux(114) =< aux(130) aux(122) =< aux(130) it(87) =< aux(130) it(90) =< aux(130) aux(114) =< aux(173) aux(122) =< aux(173) it(87) =< aux(173) it(90) =< aux(173) aux(114) =< aux(132) aux(122) =< aux(132) it(87) =< aux(132) it(90) =< aux(132) aux(114) =< aux(135) aux(122) =< aux(135) it(87) =< aux(135) it(90) =< aux(135) aux(114) =< aux(136) aux(122) =< aux(136) it(87) =< aux(136) it(90) =< aux(136) aux(114) =< aux(174) it(87) =< aux(174) aux(116) =< aux(174) aux(115) =< aux(127) s(820) =< it(90)*aux(116) s(821) =< it(90)*aux(115) s(796) =< it(87)*aux(115) s(801) =< it(87)*aux(116) s(811) =< s(820) s(812) =< aux(122) s(819) =< s(821) s(813) =< s(821) s(819) =< s(820) s(813) =< s(820) s(817) =< s(813)*aux(174) s(818) =< s(813)*aux(116) s(814) =< s(819) s(815) =< s(818) s(816) =< s(817) s(788) =< s(801) s(789) =< aux(114) s(790) =< s(796) s(799) =< s(801) s(791) =< s(801) s(799) =< s(796) s(791) =< s(796) s(797) =< s(791)*aux(127) s(798) =< s(791)*aux(115) s(792) =< s(799) s(793) =< s(798) s(794) =< s(797) with precondition: [V1>=1,V>=1,Out>=7,V+V1>=4] * Chain [[87,88,89,90,91,92],95]: 9*it(87)+9*it(90)+56*s(788)+288*s(789)+1728*s(790)+144*s(791)+216*s(792)+864*s(793)+432*s(794)+1784*s(811)+288*s(812)+144*s(813)+216*s(814)+864*s(815)+432*s(816)+7*s(836)+2 Such that:aux(127) =< V1 aux(130) =< V1+3*V aux(132) =< V1+3/2*V aux(135) =< 2*V1+V aux(136) =< 4*V1+4*V aux(179) =< V1+V aux(180) =< 3*V1+3*V aux(181) =< V s(836) =< aux(181) aux(122) =< aux(127) it(90) =< aux(127) aux(114) =< aux(179) aux(122) =< aux(179) it(87) =< aux(179) it(90) =< aux(179) aux(114) =< aux(130) aux(122) =< aux(130) it(87) =< aux(130) it(90) =< aux(130) aux(114) =< aux(180) aux(122) =< aux(180) it(87) =< aux(180) it(90) =< aux(180) aux(114) =< aux(132) aux(122) =< aux(132) it(87) =< aux(132) it(90) =< aux(132) aux(114) =< aux(135) aux(122) =< aux(135) it(87) =< aux(135) it(90) =< aux(135) aux(114) =< aux(136) aux(122) =< aux(136) it(87) =< aux(136) it(90) =< aux(136) aux(114) =< aux(181) it(87) =< aux(181) aux(116) =< aux(181) aux(115) =< aux(127) s(820) =< it(90)*aux(116) s(821) =< it(90)*aux(115) s(796) =< it(87)*aux(115) s(801) =< it(87)*aux(116) s(811) =< s(820) s(812) =< aux(122) s(819) =< s(821) s(813) =< s(821) s(819) =< s(820) s(813) =< s(820) s(817) =< s(813)*aux(181) s(818) =< s(813)*aux(116) s(814) =< s(819) s(815) =< s(818) s(816) =< s(817) s(788) =< s(801) s(789) =< aux(114) s(790) =< s(796) s(799) =< s(801) s(791) =< s(801) s(799) =< s(796) s(791) =< s(796) s(797) =< s(791)*aux(127) s(798) =< s(791)*aux(115) s(792) =< s(799) s(793) =< s(798) s(794) =< s(797) with precondition: [V1>=1,V>=1,Out>=8,V+V1>=4] * Chain [[87,88,89,90,91,92],94]: 9*it(87)+9*it(90)+56*s(788)+288*s(789)+1728*s(790)+144*s(791)+216*s(792)+864*s(793)+432*s(794)+1784*s(811)+288*s(812)+144*s(813)+216*s(814)+864*s(815)+432*s(816)+6*s(843)+2 Such that:aux(127) =< V1 aux(130) =< V1+3*V aux(132) =< V1+3/2*V aux(135) =< 2*V1+V aux(136) =< 4*V1+4*V aux(186) =< V1+V aux(187) =< 3*V1+3*V aux(188) =< V s(843) =< aux(188) aux(122) =< aux(127) it(90) =< aux(127) aux(114) =< aux(186) aux(122) =< aux(186) it(87) =< aux(186) it(90) =< aux(186) aux(114) =< aux(130) aux(122) =< aux(130) it(87) =< aux(130) it(90) =< aux(130) aux(114) =< aux(187) aux(122) =< aux(187) it(87) =< aux(187) it(90) =< aux(187) aux(114) =< aux(132) aux(122) =< aux(132) it(87) =< aux(132) it(90) =< aux(132) aux(114) =< aux(135) aux(122) =< aux(135) it(87) =< aux(135) it(90) =< aux(135) aux(114) =< aux(136) aux(122) =< aux(136) it(87) =< aux(136) it(90) =< aux(136) aux(114) =< aux(188) it(87) =< aux(188) aux(116) =< aux(188) aux(115) =< aux(127) s(820) =< it(90)*aux(116) s(821) =< it(90)*aux(115) s(796) =< it(87)*aux(115) s(801) =< it(87)*aux(116) s(811) =< s(820) s(812) =< aux(122) s(819) =< s(821) s(813) =< s(821) s(819) =< s(820) s(813) =< s(820) s(817) =< s(813)*aux(188) s(818) =< s(813)*aux(116) s(814) =< s(819) s(815) =< s(818) s(816) =< s(817) s(788) =< s(801) s(789) =< aux(114) s(790) =< s(796) s(799) =< s(801) s(791) =< s(801) s(799) =< s(796) s(791) =< s(796) s(797) =< s(791)*aux(127) s(798) =< s(791)*aux(115) s(792) =< s(799) s(793) =< s(798) s(794) =< s(797) with precondition: [V1>=1,V>=1,Out>=9,V+V1>=4] * Chain [[87,88,89,90,91,92],93]: 9*it(87)+9*it(90)+56*s(788)+288*s(789)+1728*s(790)+144*s(791)+216*s(792)+864*s(793)+432*s(794)+1784*s(811)+288*s(812)+144*s(813)+216*s(814)+864*s(815)+432*s(816)+2*s(849)+2 Such that:aux(127) =< V1 aux(130) =< V1+3*V aux(132) =< V1+3/2*V aux(135) =< 2*V1+V aux(136) =< 4*V1+4*V aux(190) =< V1+V aux(191) =< 3*V1+3*V aux(192) =< V s(849) =< aux(192) aux(122) =< aux(127) it(90) =< aux(127) aux(114) =< aux(190) aux(122) =< aux(190) it(87) =< aux(190) it(90) =< aux(190) aux(114) =< aux(130) aux(122) =< aux(130) it(87) =< aux(130) it(90) =< aux(130) aux(114) =< aux(191) aux(122) =< aux(191) it(87) =< aux(191) it(90) =< aux(191) aux(114) =< aux(132) aux(122) =< aux(132) it(87) =< aux(132) it(90) =< aux(132) aux(114) =< aux(135) aux(122) =< aux(135) it(87) =< aux(135) it(90) =< aux(135) aux(114) =< aux(136) aux(122) =< aux(136) it(87) =< aux(136) it(90) =< aux(136) aux(114) =< aux(192) it(87) =< aux(192) aux(116) =< aux(192) aux(115) =< aux(127) s(820) =< it(90)*aux(116) s(821) =< it(90)*aux(115) s(796) =< it(87)*aux(115) s(801) =< it(87)*aux(116) s(811) =< s(820) s(812) =< aux(122) s(819) =< s(821) s(813) =< s(821) s(819) =< s(820) s(813) =< s(820) s(817) =< s(813)*aux(192) s(818) =< s(813)*aux(116) s(814) =< s(819) s(815) =< s(818) s(816) =< s(817) s(788) =< s(801) s(789) =< aux(114) s(790) =< s(796) s(799) =< s(801) s(791) =< s(801) s(799) =< s(796) s(791) =< s(796) s(797) =< s(791)*aux(127) s(798) =< s(791)*aux(115) s(792) =< s(799) s(793) =< s(798) s(794) =< s(797) with precondition: [V1>=1,V>=1,Out>=8,V+V1>=4] * Chain [102]: 1 with precondition: [Out=0,V1>=0,V>=0] * Chain [101]: 1 with precondition: [V1=0,Out=1,V>=1] * Chain [100]: 1 with precondition: [V=0,Out=2,V1>=1] * Chain [99]: 1 with precondition: [Out=1,V1>=1,V>=1] * Chain [98]: 2*s(827)+2 Such that:aux(160) =< V s(827) =< aux(160) with precondition: [Out>=2,V1+1>=Out,V+1>=Out] * Chain [97]: 1*s(829)+1 Such that:s(829) =< V with precondition: [V1=V,Out>=2,V1+1>=Out] * Chain [96]: 6*s(830)+2 Such that:aux(171) =< V s(830) =< aux(171) with precondition: [Out>=3,V1+2>=Out,V+2>=Out,V+V1>=3] * Chain [95]: 7*s(836)+2 Such that:aux(178) =< V s(836) =< aux(178) with precondition: [Out>=4,2*V1+2>=Out,2*V+2>=Out,V+V1>=3] * Chain [94]: 6*s(843)+2 Such that:aux(185) =< V s(843) =< aux(185) with precondition: [Out>=5,2*V1+3>=Out,2*V+3>=Out,V+V1>=3] * Chain [93]: 2*s(849)+2 Such that:aux(189) =< V s(849) =< aux(189) with precondition: [Out>=4,V1+3>=Out,V+3>=Out,V+V1>=3] #### Cost of chains of start(V1,V,V33): * Chain [111]: 5*s(1228)+194*s(1229)+36*s(1245)+36*s(1247)+7136*s(1254)+1152*s(1255)+576*s(1257)+864*s(1260)+3456*s(1261)+1728*s(1262)+224*s(1263)+1152*s(1264)+6912*s(1265)+576*s(1267)+864*s(1270)+3456*s(1271)+1728*s(1272)+27*s(1274)+27*s(1276)+5352*s(1281)+864*s(1282)+432*s(1284)+648*s(1287)+2592*s(1288)+1296*s(1289)+168*s(1290)+864*s(1291)+5184*s(1292)+432*s(1294)+648*s(1297)+2592*s(1298)+1296*s(1299)+9*s(1301)+9*s(1303)+1784*s(1308)+288*s(1309)+144*s(1311)+216*s(1314)+864*s(1315)+432*s(1316)+56*s(1317)+288*s(1318)+1728*s(1319)+144*s(1321)+216*s(1324)+864*s(1325)+432*s(1326)+1*s(1327)+18*s(1329)+18*s(1331)+3568*s(1336)+576*s(1337)+288*s(1339)+432*s(1342)+1728*s(1343)+864*s(1344)+112*s(1345)+576*s(1346)+3456*s(1347)+288*s(1349)+432*s(1352)+1728*s(1353)+864*s(1354)+24*s(1361)+12*s(1373)+18*s(1377)+72*s(1378)+36*s(1379)+2 Such that:s(1235) =< V1+V s(1236) =< V1+3*V s(1237) =< V1+3/2*V s(1238) =< 2*V1+V s(1233) =< 2*V1+2*V s(1239) =< 2*V1+3*V s(1240) =< 3*V1+3*V s(1241) =< 4*V1+4*V aux(203) =< 1 aux(204) =< V1 aux(205) =< V s(1228) =< aux(204) s(1229) =< aux(205) s(1361) =< aux(203) s(1372) =< aux(204) s(1373) =< aux(204) s(1372) =< aux(205) s(1373) =< aux(205) s(1248) =< aux(205) s(1375) =< s(1373)*aux(205) s(1376) =< s(1373)*s(1248) s(1377) =< s(1372) s(1378) =< s(1376) s(1379) =< s(1375) s(1244) =< aux(204) s(1245) =< aux(204) s(1246) =< s(1235) s(1244) =< s(1235) s(1247) =< s(1235) s(1245) =< s(1235) s(1246) =< s(1236) s(1244) =< s(1236) s(1247) =< s(1236) s(1245) =< s(1236) s(1246) =< s(1240) s(1244) =< s(1240) s(1247) =< s(1240) s(1245) =< s(1240) s(1246) =< s(1237) s(1244) =< s(1237) s(1247) =< s(1237) s(1245) =< s(1237) s(1246) =< s(1238) s(1244) =< s(1238) s(1247) =< s(1238) s(1245) =< s(1238) s(1246) =< s(1241) s(1244) =< s(1241) s(1247) =< s(1241) s(1245) =< s(1241) s(1246) =< aux(205) s(1247) =< aux(205) s(1249) =< aux(204) s(1250) =< s(1245)*s(1248) s(1251) =< s(1245)*s(1249) s(1252) =< s(1247)*s(1249) s(1253) =< s(1247)*s(1248) s(1254) =< s(1250) s(1255) =< s(1244) s(1256) =< s(1251) s(1257) =< s(1251) s(1256) =< s(1250) s(1257) =< s(1250) s(1258) =< s(1257)*aux(205) s(1259) =< s(1257)*s(1248) s(1260) =< s(1256) s(1261) =< s(1259) s(1262) =< s(1258) s(1263) =< s(1253) s(1264) =< s(1246) s(1265) =< s(1252) s(1266) =< s(1253) s(1267) =< s(1253) s(1266) =< s(1252) s(1267) =< s(1252) s(1268) =< s(1267)*aux(204) s(1269) =< s(1267)*s(1249) s(1270) =< s(1266) s(1271) =< s(1269) s(1272) =< s(1268) s(1273) =< aux(204) s(1274) =< aux(204) s(1275) =< s(1235) s(1273) =< s(1235) s(1276) =< s(1235) s(1274) =< s(1235) s(1275) =< s(1236) s(1273) =< s(1236) s(1276) =< s(1236) s(1274) =< s(1236) s(1275) =< s(1237) s(1273) =< s(1237) s(1276) =< s(1237) s(1274) =< s(1237) s(1275) =< s(1238) s(1273) =< s(1238) s(1276) =< s(1238) s(1274) =< s(1238) s(1275) =< aux(205) s(1276) =< aux(205) s(1277) =< s(1274)*s(1248) s(1278) =< s(1274)*s(1249) s(1279) =< s(1276)*s(1249) s(1280) =< s(1276)*s(1248) s(1281) =< s(1277) s(1282) =< s(1273) s(1283) =< s(1278) s(1284) =< s(1278) s(1283) =< s(1277) s(1284) =< s(1277) s(1285) =< s(1284)*aux(205) s(1286) =< s(1284)*s(1248) s(1287) =< s(1283) s(1288) =< s(1286) s(1289) =< s(1285) s(1290) =< s(1280) s(1291) =< s(1275) s(1292) =< s(1279) s(1293) =< s(1280) s(1294) =< s(1280) s(1293) =< s(1279) s(1294) =< s(1279) s(1295) =< s(1294)*aux(204) s(1296) =< s(1294)*s(1249) s(1297) =< s(1293) s(1298) =< s(1296) s(1299) =< s(1295) s(1300) =< aux(204) s(1301) =< aux(204) s(1302) =< s(1235) s(1300) =< s(1235) s(1303) =< s(1235) s(1301) =< s(1235) s(1302) =< s(1236) s(1300) =< s(1236) s(1303) =< s(1236) s(1301) =< s(1236) s(1302) =< s(1240) s(1300) =< s(1240) s(1303) =< s(1240) s(1301) =< s(1240) s(1302) =< s(1237) s(1300) =< s(1237) s(1303) =< s(1237) s(1301) =< s(1237) s(1302) =< s(1238) s(1300) =< s(1238) s(1303) =< s(1238) s(1301) =< s(1238) s(1302) =< s(1233) s(1300) =< s(1233) s(1303) =< s(1233) s(1301) =< s(1233) s(1302) =< aux(205) s(1303) =< aux(205) s(1304) =< s(1301)*s(1248) s(1305) =< s(1301)*s(1249) s(1306) =< s(1303)*s(1249) s(1307) =< s(1303)*s(1248) s(1308) =< s(1304) s(1309) =< s(1300) s(1310) =< s(1305) s(1311) =< s(1305) s(1310) =< s(1304) s(1311) =< s(1304) s(1312) =< s(1311)*aux(205) s(1313) =< s(1311)*s(1248) s(1314) =< s(1310) s(1315) =< s(1313) s(1316) =< s(1312) s(1317) =< s(1307) s(1318) =< s(1302) s(1319) =< s(1306) s(1320) =< s(1307) s(1321) =< s(1307) s(1320) =< s(1306) s(1321) =< s(1306) s(1322) =< s(1321)*aux(204) s(1323) =< s(1321)*s(1249) s(1324) =< s(1320) s(1325) =< s(1323) s(1326) =< s(1322) s(1327) =< s(1238) s(1328) =< aux(204) s(1329) =< aux(204) s(1330) =< s(1235) s(1328) =< s(1235) s(1331) =< s(1235) s(1329) =< s(1235) s(1330) =< s(1236) s(1328) =< s(1236) s(1331) =< s(1236) s(1329) =< s(1236) s(1330) =< s(1237) s(1328) =< s(1237) s(1331) =< s(1237) s(1329) =< s(1237) s(1330) =< s(1239) s(1328) =< s(1239) s(1331) =< s(1239) s(1329) =< s(1239) s(1330) =< s(1238) s(1328) =< s(1238) s(1331) =< s(1238) s(1329) =< s(1238) s(1330) =< aux(205) s(1331) =< aux(205) s(1332) =< s(1329)*s(1248) s(1333) =< s(1329)*s(1249) s(1334) =< s(1331)*s(1249) s(1335) =< s(1331)*s(1248) s(1336) =< s(1332) s(1337) =< s(1328) s(1338) =< s(1333) s(1339) =< s(1333) s(1338) =< s(1332) s(1339) =< s(1332) s(1340) =< s(1339)*aux(205) s(1341) =< s(1339)*s(1248) s(1342) =< s(1338) s(1343) =< s(1341) s(1344) =< s(1340) s(1345) =< s(1335) s(1346) =< s(1330) s(1347) =< s(1334) s(1348) =< s(1335) s(1349) =< s(1335) s(1348) =< s(1334) s(1349) =< s(1334) s(1350) =< s(1349)*aux(204) s(1351) =< s(1349)*s(1249) s(1352) =< s(1348) s(1353) =< s(1351) s(1354) =< s(1350) with precondition: [V1>=0] * Chain [110]: 5050*s(1381)+1368*s(1391)+684*s(1423)+1026*s(1427)+1800*s(1428)+900*s(1429)+1008*s(1849)+1008*s(1851)+199808*s(1858)+32256*s(1859)+16128*s(1861)+24192*s(1864)+96768*s(1865)+48384*s(1866)+6272*s(1867)+32256*s(1868)+193536*s(1869)+16128*s(1871)+24192*s(1874)+96768*s(1875)+48384*s(1876)+756*s(1878)+756*s(1880)+149856*s(1885)+24192*s(1886)+12096*s(1888)+18144*s(1891)+72576*s(1892)+36288*s(1893)+4704*s(1894)+24192*s(1895)+145152*s(1896)+12096*s(1898)+18144*s(1901)+72576*s(1902)+36288*s(1903)+252*s(1905)+252*s(1907)+49952*s(1912)+8064*s(1913)+4032*s(1915)+6048*s(1918)+24192*s(1919)+12096*s(1920)+1568*s(1921)+8064*s(1922)+48384*s(1923)+4032*s(1925)+6048*s(1928)+24192*s(1929)+12096*s(1930)+28*s(1931)+504*s(1933)+504*s(1935)+99904*s(1940)+16128*s(1941)+8064*s(1943)+12096*s(1946)+48384*s(1947)+24192*s(1948)+3136*s(1949)+16128*s(1950)+96768*s(1951)+8064*s(1953)+12096*s(1956)+48384*s(1957)+24192*s(1958)+4608*s(3472)+2304*s(3508)+1152*s(3509)+4 Such that:aux(324) =< 1 aux(325) =< V aux(326) =< V+V33 aux(327) =< V+3*V33 aux(328) =< V+3/2*V33 aux(329) =< 2*V+V33 aux(330) =< 2*V+2*V33 aux(331) =< 2*V+3*V33 aux(332) =< 3*V+3*V33 aux(333) =< 4*V+4*V33 aux(334) =< V33 s(1381) =< aux(334) s(1391) =< aux(324) s(1422) =< aux(325) s(1423) =< aux(325) s(1422) =< aux(334) s(1423) =< aux(334) s(1424) =< aux(334) s(1425) =< s(1423)*aux(334) s(1426) =< s(1423)*s(1424) s(1427) =< s(1422) s(1428) =< s(1426) s(1429) =< s(1425) s(1848) =< aux(325) s(1849) =< aux(325) s(1850) =< aux(326) s(1848) =< aux(326) s(1851) =< aux(326) s(1849) =< aux(326) s(1850) =< aux(327) s(1848) =< aux(327) s(1851) =< aux(327) s(1849) =< aux(327) s(1850) =< aux(332) s(1848) =< aux(332) s(1851) =< aux(332) s(1849) =< aux(332) s(1850) =< aux(328) s(1848) =< aux(328) s(1851) =< aux(328) s(1849) =< aux(328) s(1850) =< aux(329) s(1848) =< aux(329) s(1851) =< aux(329) s(1849) =< aux(329) s(1850) =< aux(333) s(1848) =< aux(333) s(1851) =< aux(333) s(1849) =< aux(333) s(1850) =< aux(334) s(1851) =< aux(334) s(1853) =< aux(325) s(1854) =< s(1849)*s(1424) s(1855) =< s(1849)*s(1853) s(1856) =< s(1851)*s(1853) s(1857) =< s(1851)*s(1424) s(1858) =< s(1854) s(1859) =< s(1848) s(1860) =< s(1855) s(1861) =< s(1855) s(1860) =< s(1854) s(1861) =< s(1854) s(1862) =< s(1861)*aux(334) s(1863) =< s(1861)*s(1424) s(1864) =< s(1860) s(1865) =< s(1863) s(1866) =< s(1862) s(1867) =< s(1857) s(1868) =< s(1850) s(1869) =< s(1856) s(1870) =< s(1857) s(1871) =< s(1857) s(1870) =< s(1856) s(1871) =< s(1856) s(1872) =< s(1871)*aux(325) s(1873) =< s(1871)*s(1853) s(1874) =< s(1870) s(1875) =< s(1873) s(1876) =< s(1872) s(1877) =< aux(325) s(1878) =< aux(325) s(1879) =< aux(326) s(1877) =< aux(326) s(1880) =< aux(326) s(1878) =< aux(326) s(1879) =< aux(327) s(1877) =< aux(327) s(1880) =< aux(327) s(1878) =< aux(327) s(1879) =< aux(328) s(1877) =< aux(328) s(1880) =< aux(328) s(1878) =< aux(328) s(1879) =< aux(329) s(1877) =< aux(329) s(1880) =< aux(329) s(1878) =< aux(329) s(1879) =< aux(334) s(1880) =< aux(334) s(1881) =< s(1878)*s(1424) s(1882) =< s(1878)*s(1853) s(1883) =< s(1880)*s(1853) s(1884) =< s(1880)*s(1424) s(1885) =< s(1881) s(1886) =< s(1877) s(1887) =< s(1882) s(1888) =< s(1882) s(1887) =< s(1881) s(1888) =< s(1881) s(1889) =< s(1888)*aux(334) s(1890) =< s(1888)*s(1424) s(1891) =< s(1887) s(1892) =< s(1890) s(1893) =< s(1889) s(1894) =< s(1884) s(1895) =< s(1879) s(1896) =< s(1883) s(1897) =< s(1884) s(1898) =< s(1884) s(1897) =< s(1883) s(1898) =< s(1883) s(1899) =< s(1898)*aux(325) s(1900) =< s(1898)*s(1853) s(1901) =< s(1897) s(1902) =< s(1900) s(1903) =< s(1899) s(1904) =< aux(325) s(1905) =< aux(325) s(1906) =< aux(326) s(1904) =< aux(326) s(1907) =< aux(326) s(1905) =< aux(326) s(1906) =< aux(327) s(1904) =< aux(327) s(1907) =< aux(327) s(1905) =< aux(327) s(1906) =< aux(332) s(1904) =< aux(332) s(1907) =< aux(332) s(1905) =< aux(332) s(1906) =< aux(328) s(1904) =< aux(328) s(1907) =< aux(328) s(1905) =< aux(328) s(1906) =< aux(329) s(1904) =< aux(329) s(1907) =< aux(329) s(1905) =< aux(329) s(1906) =< aux(330) s(1904) =< aux(330) s(1907) =< aux(330) s(1905) =< aux(330) s(1906) =< aux(334) s(1907) =< aux(334) s(1908) =< s(1905)*s(1424) s(1909) =< s(1905)*s(1853) s(1910) =< s(1907)*s(1853) s(1911) =< s(1907)*s(1424) s(1912) =< s(1908) s(1913) =< s(1904) s(1914) =< s(1909) s(1915) =< s(1909) s(1914) =< s(1908) s(1915) =< s(1908) s(1916) =< s(1915)*aux(334) s(1917) =< s(1915)*s(1424) s(1918) =< s(1914) s(1919) =< s(1917) s(1920) =< s(1916) s(1921) =< s(1911) s(1922) =< s(1906) s(1923) =< s(1910) s(1924) =< s(1911) s(1925) =< s(1911) s(1924) =< s(1910) s(1925) =< s(1910) s(1926) =< s(1925)*aux(325) s(1927) =< s(1925)*s(1853) s(1928) =< s(1924) s(1929) =< s(1927) s(1930) =< s(1926) s(1931) =< aux(329) s(1932) =< aux(325) s(1933) =< aux(325) s(1934) =< aux(326) s(1932) =< aux(326) s(1935) =< aux(326) s(1933) =< aux(326) s(1934) =< aux(327) s(1932) =< aux(327) s(1935) =< aux(327) s(1933) =< aux(327) s(1934) =< aux(328) s(1932) =< aux(328) s(1935) =< aux(328) s(1933) =< aux(328) s(1934) =< aux(331) s(1932) =< aux(331) s(1935) =< aux(331) s(1933) =< aux(331) s(1934) =< aux(329) s(1932) =< aux(329) s(1935) =< aux(329) s(1933) =< aux(329) s(1934) =< aux(334) s(1935) =< aux(334) s(1936) =< s(1933)*s(1424) s(1937) =< s(1933)*s(1853) s(1938) =< s(1935)*s(1853) s(1939) =< s(1935)*s(1424) s(1940) =< s(1936) s(1941) =< s(1932) s(1942) =< s(1937) s(1943) =< s(1937) s(1942) =< s(1936) s(1943) =< s(1936) s(1944) =< s(1943)*aux(334) s(1945) =< s(1943)*s(1424) s(1946) =< s(1942) s(1947) =< s(1945) s(1948) =< s(1944) s(1949) =< s(1939) s(1950) =< s(1934) s(1951) =< s(1938) s(1952) =< s(1939) s(1953) =< s(1939) s(1952) =< s(1938) s(1953) =< s(1938) s(1954) =< s(1953)*aux(325) s(1955) =< s(1953)*s(1853) s(1956) =< s(1952) s(1957) =< s(1955) s(1958) =< s(1954) s(3472) =< aux(325) s(3505) =< s(1423)*aux(325) s(3506) =< s(1423)*s(1853) s(3508) =< s(3506) s(3509) =< s(3505) with precondition: [V1=1,V>=0,V33>=0] * Chain [109]: 0 with precondition: [V1=V,V1>=1] * Chain [108]: 0 with precondition: [V1=1,V=2] * Chain [107]: 3 with precondition: [V1=1,V33=0,V>=1] * Chain [106]: 0 with precondition: [V1=2,V=1] * Chain [105]: 0 with precondition: [V1=2,V=2] * Chain [104]: 192*s(6242)+1340*s(6243)+96*s(6254)+144*s(6258)+576*s(6259)+288*s(6260)+144*s(6386)+144*s(6388)+28544*s(6395)+4608*s(6396)+2304*s(6398)+3456*s(6401)+13824*s(6402)+6912*s(6403)+896*s(6404)+4608*s(6405)+27648*s(6406)+2304*s(6408)+3456*s(6411)+13824*s(6412)+6912*s(6413)+108*s(6415)+108*s(6417)+21408*s(6422)+3456*s(6423)+1728*s(6425)+2592*s(6428)+10368*s(6429)+5184*s(6430)+672*s(6431)+3456*s(6432)+20736*s(6433)+1728*s(6435)+2592*s(6438)+10368*s(6439)+5184*s(6440)+36*s(6442)+36*s(6444)+7136*s(6449)+1152*s(6450)+576*s(6452)+864*s(6455)+3456*s(6456)+1728*s(6457)+224*s(6458)+1152*s(6459)+6912*s(6460)+576*s(6462)+864*s(6465)+3456*s(6466)+1728*s(6467)+4*s(6468)+72*s(6470)+72*s(6472)+14272*s(6477)+2304*s(6478)+1152*s(6480)+1728*s(6483)+6912*s(6484)+3456*s(6485)+448*s(6486)+2304*s(6487)+13824*s(6488)+1152*s(6490)+1728*s(6493)+6912*s(6494)+3456*s(6495)+3 Such that:aux(345) =< 1 aux(346) =< V aux(347) =< V+V33 aux(348) =< V+3*V33 aux(349) =< V+3/2*V33 aux(350) =< 2*V+V33 aux(351) =< 2*V+2*V33 aux(352) =< 2*V+3*V33 aux(353) =< 3*V+3*V33 aux(354) =< 4*V+4*V33 aux(355) =< V33 s(6242) =< aux(345) s(6243) =< aux(355) s(6253) =< aux(346) s(6254) =< aux(346) s(6253) =< aux(355) s(6254) =< aux(355) s(6255) =< aux(355) s(6256) =< s(6254)*aux(355) s(6257) =< s(6254)*s(6255) s(6258) =< s(6253) s(6259) =< s(6257) s(6260) =< s(6256) s(6385) =< aux(346) s(6386) =< aux(346) s(6387) =< aux(347) s(6385) =< aux(347) s(6388) =< aux(347) s(6386) =< aux(347) s(6387) =< aux(348) s(6385) =< aux(348) s(6388) =< aux(348) s(6386) =< aux(348) s(6387) =< aux(353) s(6385) =< aux(353) s(6388) =< aux(353) s(6386) =< aux(353) s(6387) =< aux(349) s(6385) =< aux(349) s(6388) =< aux(349) s(6386) =< aux(349) s(6387) =< aux(350) s(6385) =< aux(350) s(6388) =< aux(350) s(6386) =< aux(350) s(6387) =< aux(354) s(6385) =< aux(354) s(6388) =< aux(354) s(6386) =< aux(354) s(6387) =< aux(355) s(6388) =< aux(355) s(6390) =< aux(346) s(6391) =< s(6386)*s(6255) s(6392) =< s(6386)*s(6390) s(6393) =< s(6388)*s(6390) s(6394) =< s(6388)*s(6255) s(6395) =< s(6391) s(6396) =< s(6385) s(6397) =< s(6392) s(6398) =< s(6392) s(6397) =< s(6391) s(6398) =< s(6391) s(6399) =< s(6398)*aux(355) s(6400) =< s(6398)*s(6255) s(6401) =< s(6397) s(6402) =< s(6400) s(6403) =< s(6399) s(6404) =< s(6394) s(6405) =< s(6387) s(6406) =< s(6393) s(6407) =< s(6394) s(6408) =< s(6394) s(6407) =< s(6393) s(6408) =< s(6393) s(6409) =< s(6408)*aux(346) s(6410) =< s(6408)*s(6390) s(6411) =< s(6407) s(6412) =< s(6410) s(6413) =< s(6409) s(6414) =< aux(346) s(6415) =< aux(346) s(6416) =< aux(347) s(6414) =< aux(347) s(6417) =< aux(347) s(6415) =< aux(347) s(6416) =< aux(348) s(6414) =< aux(348) s(6417) =< aux(348) s(6415) =< aux(348) s(6416) =< aux(349) s(6414) =< aux(349) s(6417) =< aux(349) s(6415) =< aux(349) s(6416) =< aux(350) s(6414) =< aux(350) s(6417) =< aux(350) s(6415) =< aux(350) s(6416) =< aux(355) s(6417) =< aux(355) s(6418) =< s(6415)*s(6255) s(6419) =< s(6415)*s(6390) s(6420) =< s(6417)*s(6390) s(6421) =< s(6417)*s(6255) s(6422) =< s(6418) s(6423) =< s(6414) s(6424) =< s(6419) s(6425) =< s(6419) s(6424) =< s(6418) s(6425) =< s(6418) s(6426) =< s(6425)*aux(355) s(6427) =< s(6425)*s(6255) s(6428) =< s(6424) s(6429) =< s(6427) s(6430) =< s(6426) s(6431) =< s(6421) s(6432) =< s(6416) s(6433) =< s(6420) s(6434) =< s(6421) s(6435) =< s(6421) s(6434) =< s(6420) s(6435) =< s(6420) s(6436) =< s(6435)*aux(346) s(6437) =< s(6435)*s(6390) s(6438) =< s(6434) s(6439) =< s(6437) s(6440) =< s(6436) s(6441) =< aux(346) s(6442) =< aux(346) s(6443) =< aux(347) s(6441) =< aux(347) s(6444) =< aux(347) s(6442) =< aux(347) s(6443) =< aux(348) s(6441) =< aux(348) s(6444) =< aux(348) s(6442) =< aux(348) s(6443) =< aux(353) s(6441) =< aux(353) s(6444) =< aux(353) s(6442) =< aux(353) s(6443) =< aux(349) s(6441) =< aux(349) s(6444) =< aux(349) s(6442) =< aux(349) s(6443) =< aux(350) s(6441) =< aux(350) s(6444) =< aux(350) s(6442) =< aux(350) s(6443) =< aux(351) s(6441) =< aux(351) s(6444) =< aux(351) s(6442) =< aux(351) s(6443) =< aux(355) s(6444) =< aux(355) s(6445) =< s(6442)*s(6255) s(6446) =< s(6442)*s(6390) s(6447) =< s(6444)*s(6390) s(6448) =< s(6444)*s(6255) s(6449) =< s(6445) s(6450) =< s(6441) s(6451) =< s(6446) s(6452) =< s(6446) s(6451) =< s(6445) s(6452) =< s(6445) s(6453) =< s(6452)*aux(355) s(6454) =< s(6452)*s(6255) s(6455) =< s(6451) s(6456) =< s(6454) s(6457) =< s(6453) s(6458) =< s(6448) s(6459) =< s(6443) s(6460) =< s(6447) s(6461) =< s(6448) s(6462) =< s(6448) s(6461) =< s(6447) s(6462) =< s(6447) s(6463) =< s(6462)*aux(346) s(6464) =< s(6462)*s(6390) s(6465) =< s(6461) s(6466) =< s(6464) s(6467) =< s(6463) s(6468) =< aux(350) s(6469) =< aux(346) s(6470) =< aux(346) s(6471) =< aux(347) s(6469) =< aux(347) s(6472) =< aux(347) s(6470) =< aux(347) s(6471) =< aux(348) s(6469) =< aux(348) s(6472) =< aux(348) s(6470) =< aux(348) s(6471) =< aux(349) s(6469) =< aux(349) s(6472) =< aux(349) s(6470) =< aux(349) s(6471) =< aux(352) s(6469) =< aux(352) s(6472) =< aux(352) s(6470) =< aux(352) s(6471) =< aux(350) s(6469) =< aux(350) s(6472) =< aux(350) s(6470) =< aux(350) s(6471) =< aux(355) s(6472) =< aux(355) s(6473) =< s(6470)*s(6255) s(6474) =< s(6470)*s(6390) s(6475) =< s(6472)*s(6390) s(6476) =< s(6472)*s(6255) s(6477) =< s(6473) s(6478) =< s(6469) s(6479) =< s(6474) s(6480) =< s(6474) s(6479) =< s(6473) s(6480) =< s(6473) s(6481) =< s(6480)*aux(355) s(6482) =< s(6480)*s(6255) s(6483) =< s(6479) s(6484) =< s(6482) s(6485) =< s(6481) s(6486) =< s(6476) s(6487) =< s(6471) s(6488) =< s(6475) s(6489) =< s(6476) s(6490) =< s(6476) s(6489) =< s(6475) s(6490) =< s(6475) s(6491) =< s(6490)*aux(346) s(6492) =< s(6490)*s(6390) s(6493) =< s(6489) s(6494) =< s(6492) s(6495) =< s(6491) with precondition: [V1=2,V>=0,V33>=0] * Chain [103]: 1 with precondition: [V=0,V1>=1] Closed-form bounds of start(V1,V,V33): ------------------------------------- * Chain [111] with precondition: [V1>=0] - Upper bound: 3005*V1+26+3600*V1*V1+12960*V1*V1*nat(V)+17948*V1*nat(V)+12960*V1*nat(V)*nat(V1+V)+17280*V1*nat(V1+V)+nat(V)*194+nat(V)*4160*nat(V1+V)+nat(V1+V)*2970+nat(2*V1+V) - Complexity: n^3 * Chain [110] with precondition: [V1=1,V>=0,V33>=0] - Upper bound: 89478*V+1372+104256*V*V+362880*V*V*V33+502220*V*V33+(V+V33)*(362880*V*V33)+(V+V33)*(483840*V)+5050*V33+(V+V33)*(116480*V33)+(83160*V+83160*V33)+(56*V+28*V33) - Complexity: n^3 * Chain [109] with precondition: [V1=V,V1>=1] - Upper bound: 0 - Complexity: constant * Chain [108] with precondition: [V1=1,V=2] - Upper bound: 0 - Complexity: constant * Chain [107] with precondition: [V1=1,V33=0,V>=1] - Upper bound: 3 - Complexity: constant * Chain [106] with precondition: [V1=2,V=1] - Upper bound: 0 - Complexity: constant * Chain [105] with precondition: [V1=2,V=2] - Upper bound: 0 - Complexity: constant * Chain [104] with precondition: [V1=2,V>=0,V33>=0] - Upper bound: 12120*V+195+14400*V*V+51840*V*V*V33+72224*V*V33+(V+V33)*(51840*V*V33)+(V+V33)*(69120*V)+1340*V33+(V+V33)*(16640*V33)+(11880*V+11880*V33)+(8*V+4*V33) - Complexity: n^3 * Chain [103] with precondition: [V=0,V1>=1] - Upper bound: 1 - Complexity: constant ### Maximum cost of start(V1,V,V33): max([3,nat(V)*194+26+max([3600*V1*V1+3005*V1+12960*V1*V1*nat(V)+17948*V1*nat(V)+12960*V1*nat(V)*nat(V1+V)+17280*V1*nat(V1+V)+nat(V)*4160*nat(V1+V)+nat(V1+V)*2970+nat(2*V1+V),nat(V)*77358+1177+nat(V)*89856*nat(V)+nat(V)*311040*nat(V)*nat(V33)+nat(V)*429996*nat(V33)+nat(V)*311040*nat(V33)*nat(V+V33)+nat(V)*414720*nat(V+V33)+nat(V33)*3710+nat(V33)*99840*nat(V+V33)+nat(V+V33)*71280+nat(2*V+V33)*24+(nat(V)*11926+169+nat(V)*14400*nat(V)+nat(V)*51840*nat(V)*nat(V33)+nat(V)*72224*nat(V33)+nat(V)*51840*nat(V33)*nat(V+V33)+nat(V)*69120*nat(V+V33)+nat(V33)*1340+nat(V33)*16640*nat(V+V33)+nat(V+V33)*11880+nat(2*V+V33)*4)])]) Asymptotic class: n^3 * Total analysis performed in 53027 ms. ---------------------------------------- (22) BOUNDS(1, n^3) ---------------------------------------- (23) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID)) Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT ---------------------------------------- (24) Obligation: Complexity Dependency Tuples Problem Rules: and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Tuples: AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) MONUS[ITE](True, Cons(z0, z1), z2) -> c5 GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[ITE](True, z0, z1) -> c7 GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) S tuples: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) K tuples:none Defined Rule Symbols: @_2, gt0_2, gcd_2, lgth_1, eqList_2, monus_2, goal_2, and_2, monus[Ite]_3, gcd[Ite]_3, gcd[False][Ite]_3 Defined Pair Symbols: AND_2, MONUS[ITE]_3, GCD[ITE]_3, GCD[FALSE][ITE]_3, @'_2, GT0_2, GCD_2, LGTH_1, EQLIST_2, MONUS_2, GOAL_2 Compound Symbols: c, c1, c2, c3, c4_1, c5, c6_2, c7, c8_2, c9_2, c10_1, c11, c12, c13_1, c14, c15, c16, c17, c18_2, c19_2, c20, c21_2, c22_2, c23, c24, c25, c26_3, c27_1 ---------------------------------------- (25) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID)) Converted S to standard rules, and D \ S as well as R to relative rules. ---------------------------------------- (26) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) The (relative) TRS S consists of the following rules: AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) MONUS[ITE](True, Cons(z0, z1), z2) -> c5 GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[ITE](True, z0, z1) -> c7 GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Rewrite Strategy: INNERMOST ---------------------------------------- (27) RenamingProof (BOTH BOUNDS(ID, ID)) Renamed function symbols to avoid clashes with predefined symbol. ---------------------------------------- (28) Obligation: The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF). The TRS R consists of the following rules: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) The (relative) TRS S consists of the following rules: AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) MONUS[ITE](True, Cons(z0, z1), z2) -> c5 GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[ITE](True, z0, z1) -> c7 GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Rewrite Strategy: INNERMOST ---------------------------------------- (29) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Inferred types. ---------------------------------------- (30) Obligation: Innermost TRS: Rules: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) MONUS[ITE](True, Cons(z0, z1), z2) -> c5 GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[ITE](True, z0, z1) -> c7 GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Types: @' :: Cons:Nil -> Cons:Nil -> c10:c11 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c10 :: c10:c11 -> c10:c11 Nil :: Cons:Nil c11 :: c10:c11 GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14 c12 :: c12:c13:c14 c13 :: c12:c13:c14 -> c12:c13:c14 c14 :: c12:c13:c14 GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18 c15 :: c15:c16:c17:c18 c16 :: c15:c16:c17:c18 c17 :: c15:c16:c17:c18 c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18 GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7 eqList :: Cons:Nil -> Cons:Nil -> False:True EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25 LGTH :: Cons:Nil -> c19:c20 c19 :: c10:c11 -> c19:c20 -> c19:c20 lgth :: Cons:Nil -> Cons:Nil c20 :: c19:c20 c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 AND :: False:True -> False:True -> c:c1:c2:c3 c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 c23 :: c21:c22:c23:c24:c25 c24 :: c21:c22:c23:c24:c25 c25 :: c21:c22:c23:c24:c25 MONUS :: Cons:Nil -> Cons:Nil -> c26 c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26 MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5 GOAL :: Cons:Nil -> Cons:Nil -> c27 c27 :: c15:c16:c17:c18 -> c27 False :: False:True c :: c:c1:c2:c3 True :: False:True c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 c4 :: c26 -> c4:c5 c5 :: c4:c5 c6 :: c8:c9 -> c12:c13:c14 -> c6:c7 GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9 gt0 :: Cons:Nil -> Cons:Nil -> False:True c7 :: c6:c7 c8 :: c15:c16:c17:c18 -> c26 -> c8:c9 monus :: Cons:Nil -> Cons:Nil -> Cons:Nil c9 :: c15:c16:c17:c18 -> c26 -> c8:c9 and :: False:True -> False:True -> False:True monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil @ :: Cons:Nil -> Cons:Nil -> Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil hole_c10:c111_28 :: c10:c11 hole_Cons:Nil2_28 :: Cons:Nil hole_c12:c13:c143_28 :: c12:c13:c14 hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18 hole_c6:c75_28 :: c6:c7 hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25 hole_False:True7_28 :: False:True hole_c19:c208_28 :: c19:c20 hole_c:c1:c2:c39_28 :: c:c1:c2:c3 hole_c2610_28 :: c26 hole_c4:c511_28 :: c4:c5 hole_c2712_28 :: c27 hole_c8:c913_28 :: c8:c9 gen_c10:c1114_28 :: Nat -> c10:c11 gen_Cons:Nil15_28 :: Nat -> Cons:Nil gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14 gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25 gen_c19:c2018_28 :: Nat -> c19:c20 ---------------------------------------- (31) OrderProof (LOWER BOUND(ID)) Heuristically decided to analyse the following defined symbols: @', GT0, GCD, eqList, EQLIST, LGTH, lgth, MONUS, gt0, monus, gcd, @ They will be analysed ascendingly in the following order: @' < LGTH GT0 < GCD eqList < GCD EQLIST < GCD MONUS < GCD gt0 < GCD monus < GCD eqList < EQLIST eqList < MONUS eqList < monus eqList < gcd EQLIST < MONUS lgth < LGTH LGTH < MONUS lgth < MONUS lgth < monus @ < lgth gt0 < gcd monus < gcd ---------------------------------------- (32) Obligation: Innermost TRS: Rules: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) MONUS[ITE](True, Cons(z0, z1), z2) -> c5 GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[ITE](True, z0, z1) -> c7 GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Types: @' :: Cons:Nil -> Cons:Nil -> c10:c11 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c10 :: c10:c11 -> c10:c11 Nil :: Cons:Nil c11 :: c10:c11 GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14 c12 :: c12:c13:c14 c13 :: c12:c13:c14 -> c12:c13:c14 c14 :: c12:c13:c14 GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18 c15 :: c15:c16:c17:c18 c16 :: c15:c16:c17:c18 c17 :: c15:c16:c17:c18 c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18 GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7 eqList :: Cons:Nil -> Cons:Nil -> False:True EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25 LGTH :: Cons:Nil -> c19:c20 c19 :: c10:c11 -> c19:c20 -> c19:c20 lgth :: Cons:Nil -> Cons:Nil c20 :: c19:c20 c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 AND :: False:True -> False:True -> c:c1:c2:c3 c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 c23 :: c21:c22:c23:c24:c25 c24 :: c21:c22:c23:c24:c25 c25 :: c21:c22:c23:c24:c25 MONUS :: Cons:Nil -> Cons:Nil -> c26 c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26 MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5 GOAL :: Cons:Nil -> Cons:Nil -> c27 c27 :: c15:c16:c17:c18 -> c27 False :: False:True c :: c:c1:c2:c3 True :: False:True c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 c4 :: c26 -> c4:c5 c5 :: c4:c5 c6 :: c8:c9 -> c12:c13:c14 -> c6:c7 GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9 gt0 :: Cons:Nil -> Cons:Nil -> False:True c7 :: c6:c7 c8 :: c15:c16:c17:c18 -> c26 -> c8:c9 monus :: Cons:Nil -> Cons:Nil -> Cons:Nil c9 :: c15:c16:c17:c18 -> c26 -> c8:c9 and :: False:True -> False:True -> False:True monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil @ :: Cons:Nil -> Cons:Nil -> Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil hole_c10:c111_28 :: c10:c11 hole_Cons:Nil2_28 :: Cons:Nil hole_c12:c13:c143_28 :: c12:c13:c14 hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18 hole_c6:c75_28 :: c6:c7 hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25 hole_False:True7_28 :: False:True hole_c19:c208_28 :: c19:c20 hole_c:c1:c2:c39_28 :: c:c1:c2:c3 hole_c2610_28 :: c26 hole_c4:c511_28 :: c4:c5 hole_c2712_28 :: c27 hole_c8:c913_28 :: c8:c9 gen_c10:c1114_28 :: Nat -> c10:c11 gen_Cons:Nil15_28 :: Nat -> Cons:Nil gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14 gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25 gen_c19:c2018_28 :: Nat -> c19:c20 Generator Equations: gen_c10:c1114_28(0) <=> c11 gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x)) gen_Cons:Nil15_28(0) <=> Nil gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x)) gen_c12:c13:c1416_28(0) <=> c12 gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x)) gen_c21:c22:c23:c24:c2517_28(0) <=> c23 gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x)) gen_c19:c2018_28(0) <=> c20 gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x)) The following defined symbols remain to be analysed: @', GT0, GCD, eqList, EQLIST, LGTH, lgth, MONUS, gt0, monus, gcd, @ They will be analysed ascendingly in the following order: @' < LGTH GT0 < GCD eqList < GCD EQLIST < GCD MONUS < GCD gt0 < GCD monus < GCD eqList < EQLIST eqList < MONUS eqList < monus eqList < gcd EQLIST < MONUS lgth < LGTH LGTH < MONUS lgth < MONUS lgth < monus @ < lgth gt0 < gcd monus < gcd ---------------------------------------- (33) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: @'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28) Induction Base: @'(gen_Cons:Nil15_28(0), gen_Cons:Nil15_28(b)) ->_R^Omega(1) c11 Induction Step: @'(gen_Cons:Nil15_28(+(n20_28, 1)), gen_Cons:Nil15_28(b)) ->_R^Omega(1) c10(@'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b))) ->_IH c10(gen_c10:c1114_28(c21_28)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (34) Complex Obligation (BEST) ---------------------------------------- (35) Obligation: Proved the lower bound n^1 for the following obligation: Innermost TRS: Rules: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) MONUS[ITE](True, Cons(z0, z1), z2) -> c5 GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[ITE](True, z0, z1) -> c7 GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Types: @' :: Cons:Nil -> Cons:Nil -> c10:c11 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c10 :: c10:c11 -> c10:c11 Nil :: Cons:Nil c11 :: c10:c11 GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14 c12 :: c12:c13:c14 c13 :: c12:c13:c14 -> c12:c13:c14 c14 :: c12:c13:c14 GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18 c15 :: c15:c16:c17:c18 c16 :: c15:c16:c17:c18 c17 :: c15:c16:c17:c18 c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18 GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7 eqList :: Cons:Nil -> Cons:Nil -> False:True EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25 LGTH :: Cons:Nil -> c19:c20 c19 :: c10:c11 -> c19:c20 -> c19:c20 lgth :: Cons:Nil -> Cons:Nil c20 :: c19:c20 c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 AND :: False:True -> False:True -> c:c1:c2:c3 c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 c23 :: c21:c22:c23:c24:c25 c24 :: c21:c22:c23:c24:c25 c25 :: c21:c22:c23:c24:c25 MONUS :: Cons:Nil -> Cons:Nil -> c26 c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26 MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5 GOAL :: Cons:Nil -> Cons:Nil -> c27 c27 :: c15:c16:c17:c18 -> c27 False :: False:True c :: c:c1:c2:c3 True :: False:True c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 c4 :: c26 -> c4:c5 c5 :: c4:c5 c6 :: c8:c9 -> c12:c13:c14 -> c6:c7 GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9 gt0 :: Cons:Nil -> Cons:Nil -> False:True c7 :: c6:c7 c8 :: c15:c16:c17:c18 -> c26 -> c8:c9 monus :: Cons:Nil -> Cons:Nil -> Cons:Nil c9 :: c15:c16:c17:c18 -> c26 -> c8:c9 and :: False:True -> False:True -> False:True monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil @ :: Cons:Nil -> Cons:Nil -> Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil hole_c10:c111_28 :: c10:c11 hole_Cons:Nil2_28 :: Cons:Nil hole_c12:c13:c143_28 :: c12:c13:c14 hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18 hole_c6:c75_28 :: c6:c7 hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25 hole_False:True7_28 :: False:True hole_c19:c208_28 :: c19:c20 hole_c:c1:c2:c39_28 :: c:c1:c2:c3 hole_c2610_28 :: c26 hole_c4:c511_28 :: c4:c5 hole_c2712_28 :: c27 hole_c8:c913_28 :: c8:c9 gen_c10:c1114_28 :: Nat -> c10:c11 gen_Cons:Nil15_28 :: Nat -> Cons:Nil gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14 gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25 gen_c19:c2018_28 :: Nat -> c19:c20 Generator Equations: gen_c10:c1114_28(0) <=> c11 gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x)) gen_Cons:Nil15_28(0) <=> Nil gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x)) gen_c12:c13:c1416_28(0) <=> c12 gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x)) gen_c21:c22:c23:c24:c2517_28(0) <=> c23 gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x)) gen_c19:c2018_28(0) <=> c20 gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x)) The following defined symbols remain to be analysed: @', GT0, GCD, eqList, EQLIST, LGTH, lgth, MONUS, gt0, monus, gcd, @ They will be analysed ascendingly in the following order: @' < LGTH GT0 < GCD eqList < GCD EQLIST < GCD MONUS < GCD gt0 < GCD monus < GCD eqList < EQLIST eqList < MONUS eqList < monus eqList < gcd EQLIST < MONUS lgth < LGTH LGTH < MONUS lgth < MONUS lgth < monus @ < lgth gt0 < gcd monus < gcd ---------------------------------------- (36) LowerBoundPropagationProof (FINISHED) Propagated lower bound. ---------------------------------------- (37) BOUNDS(n^1, INF) ---------------------------------------- (38) Obligation: Innermost TRS: Rules: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) MONUS[ITE](True, Cons(z0, z1), z2) -> c5 GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[ITE](True, z0, z1) -> c7 GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Types: @' :: Cons:Nil -> Cons:Nil -> c10:c11 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c10 :: c10:c11 -> c10:c11 Nil :: Cons:Nil c11 :: c10:c11 GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14 c12 :: c12:c13:c14 c13 :: c12:c13:c14 -> c12:c13:c14 c14 :: c12:c13:c14 GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18 c15 :: c15:c16:c17:c18 c16 :: c15:c16:c17:c18 c17 :: c15:c16:c17:c18 c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18 GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7 eqList :: Cons:Nil -> Cons:Nil -> False:True EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25 LGTH :: Cons:Nil -> c19:c20 c19 :: c10:c11 -> c19:c20 -> c19:c20 lgth :: Cons:Nil -> Cons:Nil c20 :: c19:c20 c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 AND :: False:True -> False:True -> c:c1:c2:c3 c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 c23 :: c21:c22:c23:c24:c25 c24 :: c21:c22:c23:c24:c25 c25 :: c21:c22:c23:c24:c25 MONUS :: Cons:Nil -> Cons:Nil -> c26 c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26 MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5 GOAL :: Cons:Nil -> Cons:Nil -> c27 c27 :: c15:c16:c17:c18 -> c27 False :: False:True c :: c:c1:c2:c3 True :: False:True c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 c4 :: c26 -> c4:c5 c5 :: c4:c5 c6 :: c8:c9 -> c12:c13:c14 -> c6:c7 GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9 gt0 :: Cons:Nil -> Cons:Nil -> False:True c7 :: c6:c7 c8 :: c15:c16:c17:c18 -> c26 -> c8:c9 monus :: Cons:Nil -> Cons:Nil -> Cons:Nil c9 :: c15:c16:c17:c18 -> c26 -> c8:c9 and :: False:True -> False:True -> False:True monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil @ :: Cons:Nil -> Cons:Nil -> Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil hole_c10:c111_28 :: c10:c11 hole_Cons:Nil2_28 :: Cons:Nil hole_c12:c13:c143_28 :: c12:c13:c14 hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18 hole_c6:c75_28 :: c6:c7 hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25 hole_False:True7_28 :: False:True hole_c19:c208_28 :: c19:c20 hole_c:c1:c2:c39_28 :: c:c1:c2:c3 hole_c2610_28 :: c26 hole_c4:c511_28 :: c4:c5 hole_c2712_28 :: c27 hole_c8:c913_28 :: c8:c9 gen_c10:c1114_28 :: Nat -> c10:c11 gen_Cons:Nil15_28 :: Nat -> Cons:Nil gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14 gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25 gen_c19:c2018_28 :: Nat -> c19:c20 Lemmas: @'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28) Generator Equations: gen_c10:c1114_28(0) <=> c11 gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x)) gen_Cons:Nil15_28(0) <=> Nil gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x)) gen_c12:c13:c1416_28(0) <=> c12 gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x)) gen_c21:c22:c23:c24:c2517_28(0) <=> c23 gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x)) gen_c19:c2018_28(0) <=> c20 gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x)) The following defined symbols remain to be analysed: GT0, GCD, eqList, EQLIST, LGTH, lgth, MONUS, gt0, monus, gcd, @ They will be analysed ascendingly in the following order: GT0 < GCD eqList < GCD EQLIST < GCD MONUS < GCD gt0 < GCD monus < GCD eqList < EQLIST eqList < MONUS eqList < monus eqList < gcd EQLIST < MONUS lgth < LGTH LGTH < MONUS lgth < MONUS lgth < monus @ < lgth gt0 < gcd monus < gcd ---------------------------------------- (39) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28)) -> gen_c12:c13:c1416_28(n1084_28), rt in Omega(1 + n1084_28) Induction Base: GT0(gen_Cons:Nil15_28(+(1, 0)), gen_Cons:Nil15_28(0)) ->_R^Omega(1) c12 Induction Step: GT0(gen_Cons:Nil15_28(+(1, +(n1084_28, 1))), gen_Cons:Nil15_28(+(n1084_28, 1))) ->_R^Omega(1) c13(GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28))) ->_IH c13(gen_c12:c13:c1416_28(c1085_28)) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (40) Obligation: Innermost TRS: Rules: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) MONUS[ITE](True, Cons(z0, z1), z2) -> c5 GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[ITE](True, z0, z1) -> c7 GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Types: @' :: Cons:Nil -> Cons:Nil -> c10:c11 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c10 :: c10:c11 -> c10:c11 Nil :: Cons:Nil c11 :: c10:c11 GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14 c12 :: c12:c13:c14 c13 :: c12:c13:c14 -> c12:c13:c14 c14 :: c12:c13:c14 GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18 c15 :: c15:c16:c17:c18 c16 :: c15:c16:c17:c18 c17 :: c15:c16:c17:c18 c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18 GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7 eqList :: Cons:Nil -> Cons:Nil -> False:True EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25 LGTH :: Cons:Nil -> c19:c20 c19 :: c10:c11 -> c19:c20 -> c19:c20 lgth :: Cons:Nil -> Cons:Nil c20 :: c19:c20 c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 AND :: False:True -> False:True -> c:c1:c2:c3 c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 c23 :: c21:c22:c23:c24:c25 c24 :: c21:c22:c23:c24:c25 c25 :: c21:c22:c23:c24:c25 MONUS :: Cons:Nil -> Cons:Nil -> c26 c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26 MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5 GOAL :: Cons:Nil -> Cons:Nil -> c27 c27 :: c15:c16:c17:c18 -> c27 False :: False:True c :: c:c1:c2:c3 True :: False:True c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 c4 :: c26 -> c4:c5 c5 :: c4:c5 c6 :: c8:c9 -> c12:c13:c14 -> c6:c7 GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9 gt0 :: Cons:Nil -> Cons:Nil -> False:True c7 :: c6:c7 c8 :: c15:c16:c17:c18 -> c26 -> c8:c9 monus :: Cons:Nil -> Cons:Nil -> Cons:Nil c9 :: c15:c16:c17:c18 -> c26 -> c8:c9 and :: False:True -> False:True -> False:True monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil @ :: Cons:Nil -> Cons:Nil -> Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil hole_c10:c111_28 :: c10:c11 hole_Cons:Nil2_28 :: Cons:Nil hole_c12:c13:c143_28 :: c12:c13:c14 hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18 hole_c6:c75_28 :: c6:c7 hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25 hole_False:True7_28 :: False:True hole_c19:c208_28 :: c19:c20 hole_c:c1:c2:c39_28 :: c:c1:c2:c3 hole_c2610_28 :: c26 hole_c4:c511_28 :: c4:c5 hole_c2712_28 :: c27 hole_c8:c913_28 :: c8:c9 gen_c10:c1114_28 :: Nat -> c10:c11 gen_Cons:Nil15_28 :: Nat -> Cons:Nil gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14 gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25 gen_c19:c2018_28 :: Nat -> c19:c20 Lemmas: @'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28) GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28)) -> gen_c12:c13:c1416_28(n1084_28), rt in Omega(1 + n1084_28) Generator Equations: gen_c10:c1114_28(0) <=> c11 gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x)) gen_Cons:Nil15_28(0) <=> Nil gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x)) gen_c12:c13:c1416_28(0) <=> c12 gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x)) gen_c21:c22:c23:c24:c2517_28(0) <=> c23 gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x)) gen_c19:c2018_28(0) <=> c20 gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x)) The following defined symbols remain to be analysed: eqList, GCD, EQLIST, LGTH, lgth, MONUS, gt0, monus, gcd, @ They will be analysed ascendingly in the following order: eqList < GCD EQLIST < GCD MONUS < GCD gt0 < GCD monus < GCD eqList < EQLIST eqList < MONUS eqList < monus eqList < gcd EQLIST < MONUS lgth < LGTH LGTH < MONUS lgth < MONUS lgth < monus @ < lgth gt0 < gcd monus < gcd ---------------------------------------- (41) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28)) -> False, rt in Omega(0) Induction Base: eqList(gen_Cons:Nil15_28(+(1, 0)), gen_Cons:Nil15_28(0)) ->_R^Omega(0) False Induction Step: eqList(gen_Cons:Nil15_28(+(1, +(n2068_28, 1))), gen_Cons:Nil15_28(+(n2068_28, 1))) ->_R^Omega(0) and(eqList(Nil, Nil), eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28))) ->_R^Omega(0) and(True, eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28))) ->_IH and(True, False) ->_R^Omega(0) False We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (42) Obligation: Innermost TRS: Rules: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) MONUS[ITE](True, Cons(z0, z1), z2) -> c5 GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[ITE](True, z0, z1) -> c7 GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Types: @' :: Cons:Nil -> Cons:Nil -> c10:c11 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c10 :: c10:c11 -> c10:c11 Nil :: Cons:Nil c11 :: c10:c11 GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14 c12 :: c12:c13:c14 c13 :: c12:c13:c14 -> c12:c13:c14 c14 :: c12:c13:c14 GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18 c15 :: c15:c16:c17:c18 c16 :: c15:c16:c17:c18 c17 :: c15:c16:c17:c18 c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18 GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7 eqList :: Cons:Nil -> Cons:Nil -> False:True EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25 LGTH :: Cons:Nil -> c19:c20 c19 :: c10:c11 -> c19:c20 -> c19:c20 lgth :: Cons:Nil -> Cons:Nil c20 :: c19:c20 c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 AND :: False:True -> False:True -> c:c1:c2:c3 c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 c23 :: c21:c22:c23:c24:c25 c24 :: c21:c22:c23:c24:c25 c25 :: c21:c22:c23:c24:c25 MONUS :: Cons:Nil -> Cons:Nil -> c26 c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26 MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5 GOAL :: Cons:Nil -> Cons:Nil -> c27 c27 :: c15:c16:c17:c18 -> c27 False :: False:True c :: c:c1:c2:c3 True :: False:True c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 c4 :: c26 -> c4:c5 c5 :: c4:c5 c6 :: c8:c9 -> c12:c13:c14 -> c6:c7 GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9 gt0 :: Cons:Nil -> Cons:Nil -> False:True c7 :: c6:c7 c8 :: c15:c16:c17:c18 -> c26 -> c8:c9 monus :: Cons:Nil -> Cons:Nil -> Cons:Nil c9 :: c15:c16:c17:c18 -> c26 -> c8:c9 and :: False:True -> False:True -> False:True monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil @ :: Cons:Nil -> Cons:Nil -> Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil hole_c10:c111_28 :: c10:c11 hole_Cons:Nil2_28 :: Cons:Nil hole_c12:c13:c143_28 :: c12:c13:c14 hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18 hole_c6:c75_28 :: c6:c7 hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25 hole_False:True7_28 :: False:True hole_c19:c208_28 :: c19:c20 hole_c:c1:c2:c39_28 :: c:c1:c2:c3 hole_c2610_28 :: c26 hole_c4:c511_28 :: c4:c5 hole_c2712_28 :: c27 hole_c8:c913_28 :: c8:c9 gen_c10:c1114_28 :: Nat -> c10:c11 gen_Cons:Nil15_28 :: Nat -> Cons:Nil gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14 gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25 gen_c19:c2018_28 :: Nat -> c19:c20 Lemmas: @'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28) GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28)) -> gen_c12:c13:c1416_28(n1084_28), rt in Omega(1 + n1084_28) eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28)) -> False, rt in Omega(0) Generator Equations: gen_c10:c1114_28(0) <=> c11 gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x)) gen_Cons:Nil15_28(0) <=> Nil gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x)) gen_c12:c13:c1416_28(0) <=> c12 gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x)) gen_c21:c22:c23:c24:c2517_28(0) <=> c23 gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x)) gen_c19:c2018_28(0) <=> c20 gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x)) The following defined symbols remain to be analysed: EQLIST, GCD, LGTH, lgth, MONUS, gt0, monus, gcd, @ They will be analysed ascendingly in the following order: EQLIST < GCD MONUS < GCD gt0 < GCD monus < GCD EQLIST < MONUS lgth < LGTH LGTH < MONUS lgth < MONUS lgth < monus @ < lgth gt0 < gcd monus < gcd ---------------------------------------- (43) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: gt0(gen_Cons:Nil15_28(+(1, n3442_28)), gen_Cons:Nil15_28(n3442_28)) -> True, rt in Omega(0) Induction Base: gt0(gen_Cons:Nil15_28(+(1, 0)), gen_Cons:Nil15_28(0)) ->_R^Omega(0) True Induction Step: gt0(gen_Cons:Nil15_28(+(1, +(n3442_28, 1))), gen_Cons:Nil15_28(+(n3442_28, 1))) ->_R^Omega(0) gt0(gen_Cons:Nil15_28(+(1, n3442_28)), gen_Cons:Nil15_28(n3442_28)) ->_IH True We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (44) Obligation: Innermost TRS: Rules: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) MONUS[ITE](True, Cons(z0, z1), z2) -> c5 GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[ITE](True, z0, z1) -> c7 GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Types: @' :: Cons:Nil -> Cons:Nil -> c10:c11 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c10 :: c10:c11 -> c10:c11 Nil :: Cons:Nil c11 :: c10:c11 GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14 c12 :: c12:c13:c14 c13 :: c12:c13:c14 -> c12:c13:c14 c14 :: c12:c13:c14 GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18 c15 :: c15:c16:c17:c18 c16 :: c15:c16:c17:c18 c17 :: c15:c16:c17:c18 c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18 GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7 eqList :: Cons:Nil -> Cons:Nil -> False:True EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25 LGTH :: Cons:Nil -> c19:c20 c19 :: c10:c11 -> c19:c20 -> c19:c20 lgth :: Cons:Nil -> Cons:Nil c20 :: c19:c20 c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 AND :: False:True -> False:True -> c:c1:c2:c3 c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 c23 :: c21:c22:c23:c24:c25 c24 :: c21:c22:c23:c24:c25 c25 :: c21:c22:c23:c24:c25 MONUS :: Cons:Nil -> Cons:Nil -> c26 c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26 MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5 GOAL :: Cons:Nil -> Cons:Nil -> c27 c27 :: c15:c16:c17:c18 -> c27 False :: False:True c :: c:c1:c2:c3 True :: False:True c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 c4 :: c26 -> c4:c5 c5 :: c4:c5 c6 :: c8:c9 -> c12:c13:c14 -> c6:c7 GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9 gt0 :: Cons:Nil -> Cons:Nil -> False:True c7 :: c6:c7 c8 :: c15:c16:c17:c18 -> c26 -> c8:c9 monus :: Cons:Nil -> Cons:Nil -> Cons:Nil c9 :: c15:c16:c17:c18 -> c26 -> c8:c9 and :: False:True -> False:True -> False:True monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil @ :: Cons:Nil -> Cons:Nil -> Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil hole_c10:c111_28 :: c10:c11 hole_Cons:Nil2_28 :: Cons:Nil hole_c12:c13:c143_28 :: c12:c13:c14 hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18 hole_c6:c75_28 :: c6:c7 hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25 hole_False:True7_28 :: False:True hole_c19:c208_28 :: c19:c20 hole_c:c1:c2:c39_28 :: c:c1:c2:c3 hole_c2610_28 :: c26 hole_c4:c511_28 :: c4:c5 hole_c2712_28 :: c27 hole_c8:c913_28 :: c8:c9 gen_c10:c1114_28 :: Nat -> c10:c11 gen_Cons:Nil15_28 :: Nat -> Cons:Nil gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14 gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25 gen_c19:c2018_28 :: Nat -> c19:c20 Lemmas: @'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28) GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28)) -> gen_c12:c13:c1416_28(n1084_28), rt in Omega(1 + n1084_28) eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28)) -> False, rt in Omega(0) gt0(gen_Cons:Nil15_28(+(1, n3442_28)), gen_Cons:Nil15_28(n3442_28)) -> True, rt in Omega(0) Generator Equations: gen_c10:c1114_28(0) <=> c11 gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x)) gen_Cons:Nil15_28(0) <=> Nil gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x)) gen_c12:c13:c1416_28(0) <=> c12 gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x)) gen_c21:c22:c23:c24:c2517_28(0) <=> c23 gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x)) gen_c19:c2018_28(0) <=> c20 gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x)) The following defined symbols remain to be analysed: @, GCD, LGTH, lgth, MONUS, monus, gcd They will be analysed ascendingly in the following order: MONUS < GCD monus < GCD lgth < LGTH LGTH < MONUS lgth < MONUS lgth < monus @ < lgth monus < gcd ---------------------------------------- (45) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: @(gen_Cons:Nil15_28(n4101_28), gen_Cons:Nil15_28(b)) -> gen_Cons:Nil15_28(+(n4101_28, b)), rt in Omega(0) Induction Base: @(gen_Cons:Nil15_28(0), gen_Cons:Nil15_28(b)) ->_R^Omega(0) gen_Cons:Nil15_28(b) Induction Step: @(gen_Cons:Nil15_28(+(n4101_28, 1)), gen_Cons:Nil15_28(b)) ->_R^Omega(0) Cons(Nil, @(gen_Cons:Nil15_28(n4101_28), gen_Cons:Nil15_28(b))) ->_IH Cons(Nil, gen_Cons:Nil15_28(+(b, c4102_28))) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (46) Obligation: Innermost TRS: Rules: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) MONUS[ITE](True, Cons(z0, z1), z2) -> c5 GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[ITE](True, z0, z1) -> c7 GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Types: @' :: Cons:Nil -> Cons:Nil -> c10:c11 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c10 :: c10:c11 -> c10:c11 Nil :: Cons:Nil c11 :: c10:c11 GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14 c12 :: c12:c13:c14 c13 :: c12:c13:c14 -> c12:c13:c14 c14 :: c12:c13:c14 GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18 c15 :: c15:c16:c17:c18 c16 :: c15:c16:c17:c18 c17 :: c15:c16:c17:c18 c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18 GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7 eqList :: Cons:Nil -> Cons:Nil -> False:True EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25 LGTH :: Cons:Nil -> c19:c20 c19 :: c10:c11 -> c19:c20 -> c19:c20 lgth :: Cons:Nil -> Cons:Nil c20 :: c19:c20 c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 AND :: False:True -> False:True -> c:c1:c2:c3 c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 c23 :: c21:c22:c23:c24:c25 c24 :: c21:c22:c23:c24:c25 c25 :: c21:c22:c23:c24:c25 MONUS :: Cons:Nil -> Cons:Nil -> c26 c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26 MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5 GOAL :: Cons:Nil -> Cons:Nil -> c27 c27 :: c15:c16:c17:c18 -> c27 False :: False:True c :: c:c1:c2:c3 True :: False:True c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 c4 :: c26 -> c4:c5 c5 :: c4:c5 c6 :: c8:c9 -> c12:c13:c14 -> c6:c7 GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9 gt0 :: Cons:Nil -> Cons:Nil -> False:True c7 :: c6:c7 c8 :: c15:c16:c17:c18 -> c26 -> c8:c9 monus :: Cons:Nil -> Cons:Nil -> Cons:Nil c9 :: c15:c16:c17:c18 -> c26 -> c8:c9 and :: False:True -> False:True -> False:True monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil @ :: Cons:Nil -> Cons:Nil -> Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil hole_c10:c111_28 :: c10:c11 hole_Cons:Nil2_28 :: Cons:Nil hole_c12:c13:c143_28 :: c12:c13:c14 hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18 hole_c6:c75_28 :: c6:c7 hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25 hole_False:True7_28 :: False:True hole_c19:c208_28 :: c19:c20 hole_c:c1:c2:c39_28 :: c:c1:c2:c3 hole_c2610_28 :: c26 hole_c4:c511_28 :: c4:c5 hole_c2712_28 :: c27 hole_c8:c913_28 :: c8:c9 gen_c10:c1114_28 :: Nat -> c10:c11 gen_Cons:Nil15_28 :: Nat -> Cons:Nil gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14 gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25 gen_c19:c2018_28 :: Nat -> c19:c20 Lemmas: @'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28) GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28)) -> gen_c12:c13:c1416_28(n1084_28), rt in Omega(1 + n1084_28) eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28)) -> False, rt in Omega(0) gt0(gen_Cons:Nil15_28(+(1, n3442_28)), gen_Cons:Nil15_28(n3442_28)) -> True, rt in Omega(0) @(gen_Cons:Nil15_28(n4101_28), gen_Cons:Nil15_28(b)) -> gen_Cons:Nil15_28(+(n4101_28, b)), rt in Omega(0) Generator Equations: gen_c10:c1114_28(0) <=> c11 gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x)) gen_Cons:Nil15_28(0) <=> Nil gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x)) gen_c12:c13:c1416_28(0) <=> c12 gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x)) gen_c21:c22:c23:c24:c2517_28(0) <=> c23 gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x)) gen_c19:c2018_28(0) <=> c20 gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x)) The following defined symbols remain to be analysed: lgth, GCD, LGTH, MONUS, monus, gcd They will be analysed ascendingly in the following order: MONUS < GCD monus < GCD lgth < LGTH LGTH < MONUS lgth < MONUS lgth < monus monus < gcd ---------------------------------------- (47) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: lgth(gen_Cons:Nil15_28(n6126_28)) -> gen_Cons:Nil15_28(n6126_28), rt in Omega(0) Induction Base: lgth(gen_Cons:Nil15_28(0)) ->_R^Omega(0) Nil Induction Step: lgth(gen_Cons:Nil15_28(+(n6126_28, 1))) ->_R^Omega(0) @(Cons(Nil, Nil), lgth(gen_Cons:Nil15_28(n6126_28))) ->_IH @(Cons(Nil, Nil), gen_Cons:Nil15_28(c6127_28)) ->_L^Omega(0) gen_Cons:Nil15_28(+(+(0, 1), n6126_28)) We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0). ---------------------------------------- (48) Obligation: Innermost TRS: Rules: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) MONUS[ITE](True, Cons(z0, z1), z2) -> c5 GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[ITE](True, z0, z1) -> c7 GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Types: @' :: Cons:Nil -> Cons:Nil -> c10:c11 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c10 :: c10:c11 -> c10:c11 Nil :: Cons:Nil c11 :: c10:c11 GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14 c12 :: c12:c13:c14 c13 :: c12:c13:c14 -> c12:c13:c14 c14 :: c12:c13:c14 GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18 c15 :: c15:c16:c17:c18 c16 :: c15:c16:c17:c18 c17 :: c15:c16:c17:c18 c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18 GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7 eqList :: Cons:Nil -> Cons:Nil -> False:True EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25 LGTH :: Cons:Nil -> c19:c20 c19 :: c10:c11 -> c19:c20 -> c19:c20 lgth :: Cons:Nil -> Cons:Nil c20 :: c19:c20 c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 AND :: False:True -> False:True -> c:c1:c2:c3 c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 c23 :: c21:c22:c23:c24:c25 c24 :: c21:c22:c23:c24:c25 c25 :: c21:c22:c23:c24:c25 MONUS :: Cons:Nil -> Cons:Nil -> c26 c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26 MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5 GOAL :: Cons:Nil -> Cons:Nil -> c27 c27 :: c15:c16:c17:c18 -> c27 False :: False:True c :: c:c1:c2:c3 True :: False:True c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 c4 :: c26 -> c4:c5 c5 :: c4:c5 c6 :: c8:c9 -> c12:c13:c14 -> c6:c7 GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9 gt0 :: Cons:Nil -> Cons:Nil -> False:True c7 :: c6:c7 c8 :: c15:c16:c17:c18 -> c26 -> c8:c9 monus :: Cons:Nil -> Cons:Nil -> Cons:Nil c9 :: c15:c16:c17:c18 -> c26 -> c8:c9 and :: False:True -> False:True -> False:True monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil @ :: Cons:Nil -> Cons:Nil -> Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil hole_c10:c111_28 :: c10:c11 hole_Cons:Nil2_28 :: Cons:Nil hole_c12:c13:c143_28 :: c12:c13:c14 hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18 hole_c6:c75_28 :: c6:c7 hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25 hole_False:True7_28 :: False:True hole_c19:c208_28 :: c19:c20 hole_c:c1:c2:c39_28 :: c:c1:c2:c3 hole_c2610_28 :: c26 hole_c4:c511_28 :: c4:c5 hole_c2712_28 :: c27 hole_c8:c913_28 :: c8:c9 gen_c10:c1114_28 :: Nat -> c10:c11 gen_Cons:Nil15_28 :: Nat -> Cons:Nil gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14 gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25 gen_c19:c2018_28 :: Nat -> c19:c20 Lemmas: @'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28) GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28)) -> gen_c12:c13:c1416_28(n1084_28), rt in Omega(1 + n1084_28) eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28)) -> False, rt in Omega(0) gt0(gen_Cons:Nil15_28(+(1, n3442_28)), gen_Cons:Nil15_28(n3442_28)) -> True, rt in Omega(0) @(gen_Cons:Nil15_28(n4101_28), gen_Cons:Nil15_28(b)) -> gen_Cons:Nil15_28(+(n4101_28, b)), rt in Omega(0) lgth(gen_Cons:Nil15_28(n6126_28)) -> gen_Cons:Nil15_28(n6126_28), rt in Omega(0) Generator Equations: gen_c10:c1114_28(0) <=> c11 gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x)) gen_Cons:Nil15_28(0) <=> Nil gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x)) gen_c12:c13:c1416_28(0) <=> c12 gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x)) gen_c21:c22:c23:c24:c2517_28(0) <=> c23 gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x)) gen_c19:c2018_28(0) <=> c20 gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x)) The following defined symbols remain to be analysed: LGTH, GCD, MONUS, monus, gcd They will be analysed ascendingly in the following order: MONUS < GCD monus < GCD LGTH < MONUS monus < gcd ---------------------------------------- (49) RewriteLemmaProof (LOWER BOUND(ID)) Proved the following rewrite lemma: LGTH(gen_Cons:Nil15_28(+(1, n7147_28))) -> *19_28, rt in Omega(n7147_28) Induction Base: LGTH(gen_Cons:Nil15_28(+(1, 0))) Induction Step: LGTH(gen_Cons:Nil15_28(+(1, +(n7147_28, 1)))) ->_R^Omega(1) c19(@'(Cons(Nil, Nil), lgth(gen_Cons:Nil15_28(+(1, n7147_28)))), LGTH(gen_Cons:Nil15_28(+(1, n7147_28)))) ->_L^Omega(0) c19(@'(Cons(Nil, Nil), gen_Cons:Nil15_28(+(1, n7147_28))), LGTH(gen_Cons:Nil15_28(+(1, n7147_28)))) ->_L^Omega(2) c19(gen_c10:c1114_28(+(0, 1)), LGTH(gen_Cons:Nil15_28(+(1, n7147_28)))) ->_IH c19(gen_c10:c1114_28(1), *19_28) We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n). ---------------------------------------- (50) Obligation: Innermost TRS: Rules: @'(Cons(z0, z1), z2) -> c10(@'(z1, z2)) @'(Nil, z0) -> c11 GT0(Cons(z0, z1), Nil) -> c12 GT0(Cons(z0, z1), Cons(z2, z3)) -> c13(GT0(z1, z3)) GT0(Nil, z0) -> c14 GCD(Nil, Nil) -> c15 GCD(Nil, Cons(z0, z1)) -> c16 GCD(Cons(z0, z1), Nil) -> c17 GCD(Cons(z0, z1), Cons(z2, z3)) -> c18(GCD[ITE](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)), EQLIST(Cons(z0, z1), Cons(z2, z3))) LGTH(Cons(z0, z1)) -> c19(@'(Cons(Nil, Nil), lgth(z1)), LGTH(z1)) LGTH(Nil) -> c20 EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c21(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z0, z2)) EQLIST(Cons(z0, z1), Cons(z2, z3)) -> c22(AND(eqList(z0, z2), eqList(z1, z3)), EQLIST(z1, z3)) EQLIST(Cons(z0, z1), Nil) -> c23 EQLIST(Nil, Cons(z0, z1)) -> c24 EQLIST(Nil, Nil) -> c25 MONUS(z0, z1) -> c26(MONUS[ITE](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1), EQLIST(lgth(z1), Cons(Nil, Nil)), LGTH(z1)) GOAL(z0, z1) -> c27(GCD(z0, z1)) AND(False, False) -> c AND(True, False) -> c1 AND(False, True) -> c2 AND(True, True) -> c3 MONUS[ITE](False, Cons(z0, z1), Cons(z2, z3)) -> c4(MONUS(z1, z3)) MONUS[ITE](True, Cons(z0, z1), z2) -> c5 GCD[ITE](False, z0, z1) -> c6(GCD[FALSE][ITE](gt0(z0, z1), z0, z1), GT0(z0, z1)) GCD[ITE](True, z0, z1) -> c7 GCD[FALSE][ITE](False, z0, z1) -> c8(GCD(z0, monus(z1, z0)), MONUS(z1, z0)) GCD[FALSE][ITE](True, z0, z1) -> c9(GCD(monus(z0, z1), z1), MONUS(z0, z1)) and(False, False) -> False and(True, False) -> False and(False, True) -> False and(True, True) -> True monus[Ite](False, Cons(z0, z1), Cons(z2, z3)) -> monus(z1, z3) monus[Ite](True, Cons(z0, z1), z2) -> z1 gcd[Ite](False, z0, z1) -> gcd[False][Ite](gt0(z0, z1), z0, z1) gcd[Ite](True, z0, z1) -> z0 gcd[False][Ite](False, z0, z1) -> gcd(z0, monus(z1, z0)) gcd[False][Ite](True, z0, z1) -> gcd(monus(z0, z1), z1) @(Cons(z0, z1), z2) -> Cons(z0, @(z1, z2)) @(Nil, z0) -> z0 gt0(Cons(z0, z1), Nil) -> True gt0(Cons(z0, z1), Cons(z2, z3)) -> gt0(z1, z3) gt0(Nil, z0) -> False gcd(Nil, Nil) -> Nil gcd(Nil, Cons(z0, z1)) -> Nil gcd(Cons(z0, z1), Nil) -> Nil gcd(Cons(z0, z1), Cons(z2, z3)) -> gcd[Ite](eqList(Cons(z0, z1), Cons(z2, z3)), Cons(z0, z1), Cons(z2, z3)) lgth(Cons(z0, z1)) -> @(Cons(Nil, Nil), lgth(z1)) lgth(Nil) -> Nil eqList(Cons(z0, z1), Cons(z2, z3)) -> and(eqList(z0, z2), eqList(z1, z3)) eqList(Cons(z0, z1), Nil) -> False eqList(Nil, Cons(z0, z1)) -> False eqList(Nil, Nil) -> True monus(z0, z1) -> monus[Ite](eqList(lgth(z1), Cons(Nil, Nil)), z0, z1) goal(z0, z1) -> gcd(z0, z1) Types: @' :: Cons:Nil -> Cons:Nil -> c10:c11 Cons :: Cons:Nil -> Cons:Nil -> Cons:Nil c10 :: c10:c11 -> c10:c11 Nil :: Cons:Nil c11 :: c10:c11 GT0 :: Cons:Nil -> Cons:Nil -> c12:c13:c14 c12 :: c12:c13:c14 c13 :: c12:c13:c14 -> c12:c13:c14 c14 :: c12:c13:c14 GCD :: Cons:Nil -> Cons:Nil -> c15:c16:c17:c18 c15 :: c15:c16:c17:c18 c16 :: c15:c16:c17:c18 c17 :: c15:c16:c17:c18 c18 :: c6:c7 -> c21:c22:c23:c24:c25 -> c15:c16:c17:c18 GCD[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c6:c7 eqList :: Cons:Nil -> Cons:Nil -> False:True EQLIST :: Cons:Nil -> Cons:Nil -> c21:c22:c23:c24:c25 LGTH :: Cons:Nil -> c19:c20 c19 :: c10:c11 -> c19:c20 -> c19:c20 lgth :: Cons:Nil -> Cons:Nil c20 :: c19:c20 c21 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 AND :: False:True -> False:True -> c:c1:c2:c3 c22 :: c:c1:c2:c3 -> c21:c22:c23:c24:c25 -> c21:c22:c23:c24:c25 c23 :: c21:c22:c23:c24:c25 c24 :: c21:c22:c23:c24:c25 c25 :: c21:c22:c23:c24:c25 MONUS :: Cons:Nil -> Cons:Nil -> c26 c26 :: c4:c5 -> c21:c22:c23:c24:c25 -> c19:c20 -> c26 MONUS[ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c4:c5 GOAL :: Cons:Nil -> Cons:Nil -> c27 c27 :: c15:c16:c17:c18 -> c27 False :: False:True c :: c:c1:c2:c3 True :: False:True c1 :: c:c1:c2:c3 c2 :: c:c1:c2:c3 c3 :: c:c1:c2:c3 c4 :: c26 -> c4:c5 c5 :: c4:c5 c6 :: c8:c9 -> c12:c13:c14 -> c6:c7 GCD[FALSE][ITE] :: False:True -> Cons:Nil -> Cons:Nil -> c8:c9 gt0 :: Cons:Nil -> Cons:Nil -> False:True c7 :: c6:c7 c8 :: c15:c16:c17:c18 -> c26 -> c8:c9 monus :: Cons:Nil -> Cons:Nil -> Cons:Nil c9 :: c15:c16:c17:c18 -> c26 -> c8:c9 and :: False:True -> False:True -> False:True monus[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd[False][Ite] :: False:True -> Cons:Nil -> Cons:Nil -> Cons:Nil gcd :: Cons:Nil -> Cons:Nil -> Cons:Nil @ :: Cons:Nil -> Cons:Nil -> Cons:Nil goal :: Cons:Nil -> Cons:Nil -> Cons:Nil hole_c10:c111_28 :: c10:c11 hole_Cons:Nil2_28 :: Cons:Nil hole_c12:c13:c143_28 :: c12:c13:c14 hole_c15:c16:c17:c184_28 :: c15:c16:c17:c18 hole_c6:c75_28 :: c6:c7 hole_c21:c22:c23:c24:c256_28 :: c21:c22:c23:c24:c25 hole_False:True7_28 :: False:True hole_c19:c208_28 :: c19:c20 hole_c:c1:c2:c39_28 :: c:c1:c2:c3 hole_c2610_28 :: c26 hole_c4:c511_28 :: c4:c5 hole_c2712_28 :: c27 hole_c8:c913_28 :: c8:c9 gen_c10:c1114_28 :: Nat -> c10:c11 gen_Cons:Nil15_28 :: Nat -> Cons:Nil gen_c12:c13:c1416_28 :: Nat -> c12:c13:c14 gen_c21:c22:c23:c24:c2517_28 :: Nat -> c21:c22:c23:c24:c25 gen_c19:c2018_28 :: Nat -> c19:c20 Lemmas: @'(gen_Cons:Nil15_28(n20_28), gen_Cons:Nil15_28(b)) -> gen_c10:c1114_28(n20_28), rt in Omega(1 + n20_28) GT0(gen_Cons:Nil15_28(+(1, n1084_28)), gen_Cons:Nil15_28(n1084_28)) -> gen_c12:c13:c1416_28(n1084_28), rt in Omega(1 + n1084_28) eqList(gen_Cons:Nil15_28(+(1, n2068_28)), gen_Cons:Nil15_28(n2068_28)) -> False, rt in Omega(0) gt0(gen_Cons:Nil15_28(+(1, n3442_28)), gen_Cons:Nil15_28(n3442_28)) -> True, rt in Omega(0) @(gen_Cons:Nil15_28(n4101_28), gen_Cons:Nil15_28(b)) -> gen_Cons:Nil15_28(+(n4101_28, b)), rt in Omega(0) lgth(gen_Cons:Nil15_28(n6126_28)) -> gen_Cons:Nil15_28(n6126_28), rt in Omega(0) LGTH(gen_Cons:Nil15_28(+(1, n7147_28))) -> *19_28, rt in Omega(n7147_28) Generator Equations: gen_c10:c1114_28(0) <=> c11 gen_c10:c1114_28(+(x, 1)) <=> c10(gen_c10:c1114_28(x)) gen_Cons:Nil15_28(0) <=> Nil gen_Cons:Nil15_28(+(x, 1)) <=> Cons(Nil, gen_Cons:Nil15_28(x)) gen_c12:c13:c1416_28(0) <=> c12 gen_c12:c13:c1416_28(+(x, 1)) <=> c13(gen_c12:c13:c1416_28(x)) gen_c21:c22:c23:c24:c2517_28(0) <=> c23 gen_c21:c22:c23:c24:c2517_28(+(x, 1)) <=> c21(c, gen_c21:c22:c23:c24:c2517_28(x)) gen_c19:c2018_28(0) <=> c20 gen_c19:c2018_28(+(x, 1)) <=> c19(c11, gen_c19:c2018_28(x)) The following defined symbols remain to be analysed: MONUS, GCD, monus, gcd They will be analysed ascendingly in the following order: MONUS < GCD monus < GCD monus < gcd