src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.siv
changeset 41561 d1318f3c86ba
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.siv	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,547 @@
     1.4 +*****************************************************************************
     1.5 +                       Semantic Analysis of SPARK Text
     1.6 +    Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
     1.7 +             Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
     1.8 +*****************************************************************************
     1.9 +
    1.10 +
    1.11 +CREATED 29-NOV-2010, 14:30:13  SIMPLIFIED 29-NOV-2010, 14:30:13
    1.12 +
    1.13 +SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
    1.14 +Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
    1.15 +
    1.16 +procedure Liseq.Liseq_length
    1.17 +
    1.18 +
    1.19 +
    1.20 +
    1.21 +For path(s) from start to run-time check associated with statement of line 11:
    1.22 +
    1.23 +procedure_liseq_length_1.
    1.24 +*** true .          /* all conclusions proved */
    1.25 +
    1.26 +
    1.27 +For path(s) from start to run-time check associated with statement of line 12:
    1.28 +
    1.29 +procedure_liseq_length_2.
    1.30 +*** true .          /* all conclusions proved */
    1.31 +
    1.32 +
    1.33 +For path(s) from start to run-time check associated with statement of line 13:
    1.34 +
    1.35 +procedure_liseq_length_3.
    1.36 +*** true .          /* all conclusions proved */
    1.37 +
    1.38 +
    1.39 +For path(s) from start to run-time check associated with statement of line 14:
    1.40 +
    1.41 +procedure_liseq_length_4.
    1.42 +*** true .          /* all conclusions proved */
    1.43 +
    1.44 +
    1.45 +For path(s) from start to assertion of line 15:
    1.46 +
    1.47 +procedure_liseq_length_5.
    1.48 +H1:    a__index__subtype__1__first = 0 .
    1.49 +H2:    l__index__subtype__1__first = 0 .
    1.50 +H3:    a__index__subtype__1__last = l__index__subtype__1__last .
    1.51 +H4:    a__index__subtype__1__last < 2147483647 .
    1.52 +H5:    for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 
    1.53 +          <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) 
    1.54 +          and element(a, [i___1]) <= 2147483647) .
    1.55 +H6:    for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 
    1.56 +          <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) 
    1.57 +          and element(l, [i___1]) <= 2147483647) .
    1.58 +H7:    0 <= l__index__subtype__1__last .
    1.59 +H8:    integer__size >= 0 .
    1.60 +H9:    a__index__subtype__1__first <= a__index__subtype__1__last .
    1.61 +H10:   l__index__subtype__1__first <= l__index__subtype__1__last .
    1.62 +H11:   a__index__subtype__1__first >= - 2147483648 .
    1.63 +H12:   a__index__subtype__1__last >= - 2147483648 .
    1.64 +H13:   l__index__subtype__1__first >= - 2147483648 .
    1.65 +H14:   l__index__subtype__1__last >= - 2147483648 .
    1.66 +H15:   a__index__subtype__1__last <= 2147483647 .
    1.67 +H16:   a__index__subtype__1__first <= 2147483647 .
    1.68 +H17:   l__index__subtype__1__last <= 2147483647 .
    1.69 +H18:   l__index__subtype__1__first <= 2147483647 .
    1.70 +       ->
    1.71 +C1:    for_all(i2_ : integer, 0 <= i2_ and i2_ <= 0 -> element(update(l, [0], 1)
    1.72 +          , [i2_]) = liseq_ends_at(a, i2_)) .
    1.73 +C2:    1 = liseq_prfx(a, 1) .
    1.74 +
    1.75 +
    1.76 +For path(s) from assertion of line 15 to assertion of line 15:
    1.77 +
    1.78 +procedure_liseq_length_6.
    1.79 +H1:    for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = 
    1.80 +          liseq_ends_at(a, i2_)) .
    1.81 +H2:    element(l, [pmax]) = liseq_prfx(a, i) .
    1.82 +H3:    0 <= pmax .
    1.83 +H4:    pmax < i .
    1.84 +H5:    a__index__subtype__1__first = 0 .
    1.85 +H6:    l__index__subtype__1__first = 0 .
    1.86 +H7:    a__index__subtype__1__last = l__index__subtype__1__last .
    1.87 +H8:    a__index__subtype__1__last < 2147483647 .
    1.88 +H9:    for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 
    1.89 +          <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) 
    1.90 +          and element(a, [i___1]) <= 2147483647) .
    1.91 +H10:   for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 
    1.92 +          <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) 
    1.93 +          and element(l, [i___1]) <= 2147483647) .
    1.94 +H11:   i <= l__index__subtype__1__last .
    1.95 +H12:   pmax >= a__index__subtype__1__first .
    1.96 +H13:   i <= a__index__subtype__1__last .
    1.97 +H14:   element(a, [pmax]) <= element(a, [i]) .
    1.98 +H15:   element(l, [pmax]) >= - 2147483648 .
    1.99 +H16:   element(l, [pmax]) <= 2147483646 .
   1.100 +H17:   i >= l__index__subtype__1__first .
   1.101 +H18:   i <= 2147483646 .
   1.102 +H19:   integer__size >= 0 .
   1.103 +H20:   a__index__subtype__1__first <= a__index__subtype__1__last .
   1.104 +H21:   l__index__subtype__1__first <= l__index__subtype__1__last .
   1.105 +H22:   a__index__subtype__1__first >= - 2147483648 .
   1.106 +H23:   a__index__subtype__1__last >= - 2147483648 .
   1.107 +H24:   l__index__subtype__1__first >= - 2147483648 .
   1.108 +H25:   l__index__subtype__1__last >= - 2147483648 .
   1.109 +H26:   a__index__subtype__1__last <= 2147483647 .
   1.110 +H27:   a__index__subtype__1__first <= 2147483647 .
   1.111 +H28:   l__index__subtype__1__last <= 2147483647 .
   1.112 +H29:   l__index__subtype__1__first <= 2147483647 .
   1.113 +       ->
   1.114 +C1:    for_all(i2_ : integer, 0 <= i2_ and i2_ <= i -> element(update(l, [i], 
   1.115 +          element(l, [pmax]) + 1), [i2_]) = liseq_ends_at(a, i2_)) .
   1.116 +C2:    element(l, [pmax]) + 1 = liseq_prfx(a, i + 1) .
   1.117 +
   1.118 +
   1.119 +For path(s) from assertion of line 26 to assertion of line 15:
   1.120 +
   1.121 +procedure_liseq_length_7.
   1.122 +H1:    for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = 
   1.123 +          liseq_ends_at(a, i2_)) .
   1.124 +H2:    element(l, [pmax]) = liseq_prfx(a, i) .
   1.125 +H3:    i <= l__index__subtype__1__last .
   1.126 +H4:    0 <= pmax .
   1.127 +H5:    pmax < i .
   1.128 +H6:    0 <= i .
   1.129 +H7:    a__index__subtype__1__first = 0 .
   1.130 +H8:    l__index__subtype__1__first = 0 .
   1.131 +H9:    a__index__subtype__1__last = l__index__subtype__1__last .
   1.132 +H10:   a__index__subtype__1__last < 2147483647 .
   1.133 +H11:   for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 
   1.134 +          <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) 
   1.135 +          and element(a, [i___1]) <= 2147483647) .
   1.136 +H12:   for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 
   1.137 +          <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) 
   1.138 +          and element(l, [i___1]) <= 2147483647) .
   1.139 +H13:   i <= 2147483647 .
   1.140 +H14:   max_ext(a, i, i) >= - 2147483648 .
   1.141 +H15:   max_ext(a, i, i) <= 2147483646 .
   1.142 +H16:   i >= l__index__subtype__1__first .
   1.143 +H17:   element(l, [pmax]) >= - 2147483648 .
   1.144 +H18:   max_ext(a, i, i) + 1 > element(l, [pmax]) .
   1.145 +H19:   element(l, [pmax]) <= 2147483646 .
   1.146 +H20:   i <= 2147483646 .
   1.147 +H21:   integer__size >= 0 .
   1.148 +H22:   a__index__subtype__1__first <= a__index__subtype__1__last .
   1.149 +H23:   l__index__subtype__1__first <= l__index__subtype__1__last .
   1.150 +H24:   a__index__subtype__1__first >= - 2147483648 .
   1.151 +H25:   a__index__subtype__1__last >= - 2147483648 .
   1.152 +H26:   l__index__subtype__1__first >= - 2147483648 .
   1.153 +H27:   l__index__subtype__1__last >= - 2147483648 .
   1.154 +H28:   a__index__subtype__1__last <= 2147483647 .
   1.155 +H29:   a__index__subtype__1__first <= 2147483647 .
   1.156 +H30:   l__index__subtype__1__last <= 2147483647 .
   1.157 +H31:   l__index__subtype__1__first <= 2147483647 .
   1.158 +       ->
   1.159 +C1:    for_all(i2_ : integer, 0 <= i2_ and i2_ <= i -> element(update(l, [i], 
   1.160 +          max_ext(a, i, i) + 1), [i2_]) = liseq_ends_at(a, i2_)) .
   1.161 +C2:    max_ext(a, i, i) + 1 = element(l, [pmax]) + 1 .
   1.162 +C3:    max_ext(a, i, i) + 1 = liseq_prfx(a, i + 1) .
   1.163 +
   1.164 +
   1.165 +procedure_liseq_length_8.
   1.166 +H1:    for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = 
   1.167 +          liseq_ends_at(a, i2_)) .
   1.168 +H2:    element(l, [pmax]) = liseq_prfx(a, i) .
   1.169 +H3:    i <= l__index__subtype__1__last .
   1.170 +H4:    0 <= pmax .
   1.171 +H5:    pmax < i .
   1.172 +H6:    0 <= i .
   1.173 +H7:    a__index__subtype__1__first = 0 .
   1.174 +H8:    l__index__subtype__1__first = 0 .
   1.175 +H9:    a__index__subtype__1__last = l__index__subtype__1__last .
   1.176 +H10:   a__index__subtype__1__last < 2147483647 .
   1.177 +H11:   for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 
   1.178 +          <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) 
   1.179 +          and element(a, [i___1]) <= 2147483647) .
   1.180 +H12:   for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 
   1.181 +          <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) 
   1.182 +          and element(l, [i___1]) <= 2147483647) .
   1.183 +H13:   i <= 2147483647 .
   1.184 +H14:   max_ext(a, i, i) >= - 2147483648 .
   1.185 +H15:   max_ext(a, i, i) <= 2147483646 .
   1.186 +H16:   i >= l__index__subtype__1__first .
   1.187 +H17:   element(l, [pmax]) <= 2147483647 .
   1.188 +H18:   max_ext(a, i, i) + 1 <= element(l, [pmax]) .
   1.189 +H19:   i <= 2147483646 .
   1.190 +H20:   integer__size >= 0 .
   1.191 +H21:   a__index__subtype__1__first <= a__index__subtype__1__last .
   1.192 +H22:   l__index__subtype__1__first <= l__index__subtype__1__last .
   1.193 +H23:   a__index__subtype__1__first >= - 2147483648 .
   1.194 +H24:   a__index__subtype__1__last >= - 2147483648 .
   1.195 +H25:   l__index__subtype__1__first >= - 2147483648 .
   1.196 +H26:   l__index__subtype__1__last >= - 2147483648 .
   1.197 +H27:   a__index__subtype__1__last <= 2147483647 .
   1.198 +H28:   a__index__subtype__1__first <= 2147483647 .
   1.199 +H29:   l__index__subtype__1__last <= 2147483647 .
   1.200 +H30:   l__index__subtype__1__first <= 2147483647 .
   1.201 +       ->
   1.202 +C1:    for_all(i2_ : integer, 0 <= i2_ and i2_ <= i -> element(update(l, [i], 
   1.203 +          max_ext(a, i, i) + 1), [i2_]) = liseq_ends_at(a, i2_)) .
   1.204 +C2:    element(l, [pmax]) = liseq_prfx(a, i + 1) .
   1.205 +
   1.206 +
   1.207 +For path(s) from assertion of line 15 to run-time check associated with 
   1.208 +          statement of line 23:
   1.209 +
   1.210 +procedure_liseq_length_9.
   1.211 +*** true .          /* all conclusions proved */
   1.212 +
   1.213 +
   1.214 +For path(s) from assertion of line 15 to run-time check associated with 
   1.215 +          statement of line 24:
   1.216 +
   1.217 +procedure_liseq_length_10.
   1.218 +*** true .          /* all conclusions proved */
   1.219 +
   1.220 +
   1.221 +For path(s) from assertion of line 15 to run-time check associated with 
   1.222 +          statement of line 25:
   1.223 +
   1.224 +procedure_liseq_length_11.
   1.225 +*** true .          /* all conclusions proved */
   1.226 +
   1.227 +
   1.228 +For path(s) from assertion of line 15 to assertion of line 26:
   1.229 +
   1.230 +procedure_liseq_length_12.
   1.231 +H1:    for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = 
   1.232 +          liseq_ends_at(a, i2_)) .
   1.233 +H2:    element(l, [pmax]) = liseq_prfx(a, i) .
   1.234 +H3:    0 <= pmax .
   1.235 +H4:    pmax < i .
   1.236 +H5:    a__index__subtype__1__first = 0 .
   1.237 +H6:    l__index__subtype__1__first = 0 .
   1.238 +H7:    a__index__subtype__1__last = l__index__subtype__1__last .
   1.239 +H8:    a__index__subtype__1__last < 2147483647 .
   1.240 +H9:    for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 
   1.241 +          <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) 
   1.242 +          and element(a, [i___1]) <= 2147483647) .
   1.243 +H10:   for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 
   1.244 +          <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) 
   1.245 +          and element(l, [i___1]) <= 2147483647) .
   1.246 +H11:   i <= l__index__subtype__1__last .
   1.247 +H12:   pmax <= 2147483647 .
   1.248 +H13:   pmax >= a__index__subtype__1__first .
   1.249 +H14:   i <= a__index__subtype__1__last .
   1.250 +H15:   element(a, [i]) < element(a, [pmax]) .
   1.251 +H16:   integer__size >= 0 .
   1.252 +H17:   a__index__subtype__1__first <= a__index__subtype__1__last .
   1.253 +H18:   l__index__subtype__1__first <= l__index__subtype__1__last .
   1.254 +H19:   a__index__subtype__1__first >= - 2147483648 .
   1.255 +H20:   a__index__subtype__1__last >= - 2147483648 .
   1.256 +H21:   l__index__subtype__1__first >= - 2147483648 .
   1.257 +H22:   l__index__subtype__1__last >= - 2147483648 .
   1.258 +H23:   a__index__subtype__1__last <= 2147483647 .
   1.259 +H24:   a__index__subtype__1__first <= 2147483647 .
   1.260 +H25:   l__index__subtype__1__last <= 2147483647 .
   1.261 +H26:   l__index__subtype__1__first <= 2147483647 .
   1.262 +       ->
   1.263 +C1:    0 = max_ext(a, i, 0) .
   1.264 +
   1.265 +
   1.266 +For path(s) from assertion of line 26 to assertion of line 26:
   1.267 +
   1.268 +procedure_liseq_length_13.
   1.269 +H1:    for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = 
   1.270 +          liseq_ends_at(a, i2_)) .
   1.271 +H2:    element(l, [pmax]) = liseq_prfx(a, i) .
   1.272 +H3:    i <= l__index__subtype__1__last .
   1.273 +H4:    0 <= pmax .
   1.274 +H5:    pmax < i .
   1.275 +H6:    0 <= j .
   1.276 +H7:    a__index__subtype__1__first = 0 .
   1.277 +H8:    l__index__subtype__1__first = 0 .
   1.278 +H9:    a__index__subtype__1__last = l__index__subtype__1__last .
   1.279 +H10:   a__index__subtype__1__last < 2147483647 .
   1.280 +H11:   for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 
   1.281 +          <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) 
   1.282 +          and element(a, [i___1]) <= 2147483647) .
   1.283 +H12:   for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 
   1.284 +          <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) 
   1.285 +          and element(l, [i___1]) <= 2147483647) .
   1.286 +H13:   j < i .
   1.287 +H14:   max_ext(a, i, j) >= - 2147483648 .
   1.288 +H15:   max_ext(a, i, j) <= 2147483647 .
   1.289 +H16:   j >= l__index__subtype__1__first .
   1.290 +H17:   i >= a__index__subtype__1__first .
   1.291 +H18:   i <= a__index__subtype__1__last .
   1.292 +H19:   j >= a__index__subtype__1__first .
   1.293 +H20:   j <= a__index__subtype__1__last .
   1.294 +H21:   element(a, [j]) <= element(a, [i]) .
   1.295 +H22:   max_ext(a, i, j) < element(l, [j]) .
   1.296 +H23:   element(l, [j]) >= - 2147483648 .
   1.297 +H24:   element(l, [j]) <= 2147483647 .
   1.298 +H25:   j <= 2147483646 .
   1.299 +H26:   integer__size >= 0 .
   1.300 +H27:   a__index__subtype__1__first <= a__index__subtype__1__last .
   1.301 +H28:   l__index__subtype__1__first <= l__index__subtype__1__last .
   1.302 +H29:   a__index__subtype__1__first >= - 2147483648 .
   1.303 +H30:   a__index__subtype__1__last >= - 2147483648 .
   1.304 +H31:   l__index__subtype__1__first >= - 2147483648 .
   1.305 +H32:   l__index__subtype__1__last >= - 2147483648 .
   1.306 +H33:   a__index__subtype__1__last <= 2147483647 .
   1.307 +H34:   a__index__subtype__1__first <= 2147483647 .
   1.308 +H35:   l__index__subtype__1__last <= 2147483647 .
   1.309 +H36:   l__index__subtype__1__first <= 2147483647 .
   1.310 +       ->
   1.311 +C1:    element(l, [j]) = max_ext(a, i, j + 1) .
   1.312 +
   1.313 +
   1.314 +procedure_liseq_length_14.
   1.315 +H1:    for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = 
   1.316 +          liseq_ends_at(a, i2_)) .
   1.317 +H2:    element(l, [pmax]) = liseq_prfx(a, i) .
   1.318 +H3:    i <= l__index__subtype__1__last .
   1.319 +H4:    0 <= pmax .
   1.320 +H5:    pmax < i .
   1.321 +H6:    0 <= j .
   1.322 +H7:    a__index__subtype__1__first = 0 .
   1.323 +H8:    l__index__subtype__1__first = 0 .
   1.324 +H9:    a__index__subtype__1__last = l__index__subtype__1__last .
   1.325 +H10:   a__index__subtype__1__last < 2147483647 .
   1.326 +H11:   for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 
   1.327 +          <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) 
   1.328 +          and element(a, [i___1]) <= 2147483647) .
   1.329 +H12:   for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 
   1.330 +          <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) 
   1.331 +          and element(l, [i___1]) <= 2147483647) .
   1.332 +H13:   j < i .
   1.333 +H14:   max_ext(a, i, j) >= - 2147483648 .
   1.334 +H15:   max_ext(a, i, j) <= 2147483647 .
   1.335 +H16:   j >= l__index__subtype__1__first .
   1.336 +H17:   i >= a__index__subtype__1__first .
   1.337 +H18:   i <= a__index__subtype__1__last .
   1.338 +H19:   j >= a__index__subtype__1__first .
   1.339 +H20:   j <= a__index__subtype__1__last .
   1.340 +H21:   element(a, [i]) < element(a, [j]) or element(l, [j]) <= max_ext(a, i, j) 
   1.341 +          .
   1.342 +H22:   j <= 2147483646 .
   1.343 +H23:   integer__size >= 0 .
   1.344 +H24:   a__index__subtype__1__first <= a__index__subtype__1__last .
   1.345 +H25:   l__index__subtype__1__first <= l__index__subtype__1__last .
   1.346 +H26:   a__index__subtype__1__first >= - 2147483648 .
   1.347 +H27:   a__index__subtype__1__last >= - 2147483648 .
   1.348 +H28:   l__index__subtype__1__first >= - 2147483648 .
   1.349 +H29:   l__index__subtype__1__last >= - 2147483648 .
   1.350 +H30:   a__index__subtype__1__last <= 2147483647 .
   1.351 +H31:   a__index__subtype__1__first <= 2147483647 .
   1.352 +H32:   l__index__subtype__1__last <= 2147483647 .
   1.353 +H33:   l__index__subtype__1__first <= 2147483647 .
   1.354 +       ->
   1.355 +C1:    max_ext(a, i, j) = max_ext(a, i, j + 1) .
   1.356 +
   1.357 +
   1.358 +For path(s) from assertion of line 26 to run-time check associated with 
   1.359 +          statement of line 36:
   1.360 +
   1.361 +procedure_liseq_length_15.
   1.362 +*** true .          /* all conclusions proved */
   1.363 +
   1.364 +
   1.365 +For path(s) from assertion of line 26 to run-time check associated with 
   1.366 +          statement of line 38:
   1.367 +
   1.368 +procedure_liseq_length_16.
   1.369 +*** true .          /* all conclusions proved */
   1.370 +
   1.371 +
   1.372 +For path(s) from assertion of line 26 to run-time check associated with 
   1.373 +          statement of line 40:
   1.374 +
   1.375 +procedure_liseq_length_17.
   1.376 +*** true .          /* all conclusions proved */
   1.377 +
   1.378 +
   1.379 +procedure_liseq_length_18.
   1.380 +*** true .          /* all conclusions proved */
   1.381 +
   1.382 +
   1.383 +For path(s) from assertion of line 26 to run-time check associated with 
   1.384 +          statement of line 42:
   1.385 +
   1.386 +procedure_liseq_length_19.
   1.387 +H1:    for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = 
   1.388 +          liseq_ends_at(a, i2_)) .
   1.389 +H2:    element(l, [pmax]) = liseq_prfx(a, i) .
   1.390 +H3:    i <= l__index__subtype__1__last .
   1.391 +H4:    0 <= pmax .
   1.392 +H5:    pmax < i .
   1.393 +H6:    a__index__subtype__1__first = 0 .
   1.394 +H7:    l__index__subtype__1__first = 0 .
   1.395 +H8:    a__index__subtype__1__last = l__index__subtype__1__last .
   1.396 +H9:    a__index__subtype__1__last < 2147483647 .
   1.397 +H10:   for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 
   1.398 +          <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) 
   1.399 +          and element(a, [i___1]) <= 2147483647) .
   1.400 +H11:   for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 
   1.401 +          <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) 
   1.402 +          and element(l, [i___1]) <= 2147483647) .
   1.403 +H12:   i <= 2147483647 .
   1.404 +H13:   max_ext(a, i, i) >= - 2147483648 .
   1.405 +H14:   max_ext(a, i, i) <= 2147483647 .
   1.406 +H15:   integer__size >= 0 .
   1.407 +H16:   a__index__subtype__1__first <= a__index__subtype__1__last .
   1.408 +H17:   l__index__subtype__1__first <= l__index__subtype__1__last .
   1.409 +H18:   a__index__subtype__1__first >= - 2147483648 .
   1.410 +H19:   a__index__subtype__1__last >= - 2147483648 .
   1.411 +H20:   l__index__subtype__1__first >= - 2147483648 .
   1.412 +H21:   l__index__subtype__1__last >= - 2147483648 .
   1.413 +H22:   a__index__subtype__1__last <= 2147483647 .
   1.414 +H23:   a__index__subtype__1__first <= 2147483647 .
   1.415 +H24:   l__index__subtype__1__last <= 2147483647 .
   1.416 +H25:   l__index__subtype__1__first <= 2147483647 .
   1.417 +       ->
   1.418 +C1:    max_ext(a, i, i) <= 2147483646 .
   1.419 +
   1.420 +
   1.421 +For path(s) from assertion of line 26 to run-time check associated with 
   1.422 +          statement of line 43:
   1.423 +
   1.424 +procedure_liseq_length_20.
   1.425 +*** true .          /* all conclusions proved */
   1.426 +
   1.427 +
   1.428 +For path(s) from assertion of line 26 to run-time check associated with 
   1.429 +          statement of line 44:
   1.430 +
   1.431 +procedure_liseq_length_21.
   1.432 +*** true .          /* all conclusions proved */
   1.433 +
   1.434 +
   1.435 +For path(s) from assertion of line 26 to run-time check associated with 
   1.436 +          statement of line 45:
   1.437 +
   1.438 +procedure_liseq_length_22.
   1.439 +*** true .          /* all conclusions proved */
   1.440 +
   1.441 +
   1.442 +For path(s) from assertion of line 15 to run-time check associated with 
   1.443 +          statement of line 48:
   1.444 +
   1.445 +procedure_liseq_length_23.
   1.446 +H1:    for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = 
   1.447 +          liseq_ends_at(a, i2_)) .
   1.448 +H2:    element(l, [pmax]) = liseq_prfx(a, i) .
   1.449 +H3:    0 <= pmax .
   1.450 +H4:    pmax < i .
   1.451 +H5:    a__index__subtype__1__first = 0 .
   1.452 +H6:    l__index__subtype__1__first = 0 .
   1.453 +H7:    a__index__subtype__1__last = l__index__subtype__1__last .
   1.454 +H8:    a__index__subtype__1__last < 2147483647 .
   1.455 +H9:    for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 
   1.456 +          <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) 
   1.457 +          and element(a, [i___1]) <= 2147483647) .
   1.458 +H10:   for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 
   1.459 +          <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) 
   1.460 +          and element(l, [i___1]) <= 2147483647) .
   1.461 +H11:   i <= l__index__subtype__1__last .
   1.462 +H12:   pmax <= 2147483647 .
   1.463 +H13:   pmax >= a__index__subtype__1__first .
   1.464 +H14:   i <= a__index__subtype__1__last .
   1.465 +H15:   element(a, [pmax]) <= element(a, [i]) .
   1.466 +H16:   element(l, [pmax]) >= - 2147483648 .
   1.467 +H17:   element(l, [pmax]) <= 2147483647 .
   1.468 +H18:   integer__size >= 0 .
   1.469 +H19:   a__index__subtype__1__first <= a__index__subtype__1__last .
   1.470 +H20:   l__index__subtype__1__first <= l__index__subtype__1__last .
   1.471 +H21:   a__index__subtype__1__first >= - 2147483648 .
   1.472 +H22:   a__index__subtype__1__last >= - 2147483648 .
   1.473 +H23:   l__index__subtype__1__first >= - 2147483648 .
   1.474 +H24:   l__index__subtype__1__last >= - 2147483648 .
   1.475 +H25:   a__index__subtype__1__last <= 2147483647 .
   1.476 +H26:   a__index__subtype__1__first <= 2147483647 .
   1.477 +H27:   l__index__subtype__1__last <= 2147483647 .
   1.478 +H28:   l__index__subtype__1__first <= 2147483647 .
   1.479 +       ->
   1.480 +C1:    element(l, [pmax]) <= 2147483646 .
   1.481 +
   1.482 +
   1.483 +For path(s) from assertion of line 15 to run-time check associated with 
   1.484 +          statement of line 49:
   1.485 +
   1.486 +procedure_liseq_length_24.
   1.487 +*** true .          /* all conclusions proved */
   1.488 +
   1.489 +
   1.490 +For path(s) from assertion of line 15 to run-time check associated with 
   1.491 +          statement of line 50:
   1.492 +
   1.493 +procedure_liseq_length_25.
   1.494 +*** true .          /* all conclusions proved */
   1.495 +
   1.496 +
   1.497 +For path(s) from assertion of line 15 to run-time check associated with 
   1.498 +          statement of line 52:
   1.499 +
   1.500 +procedure_liseq_length_26.
   1.501 +*** true .          /* all conclusions proved */
   1.502 +
   1.503 +
   1.504 +For path(s) from assertion of line 26 to run-time check associated with 
   1.505 +          statement of line 52:
   1.506 +
   1.507 +procedure_liseq_length_27.
   1.508 +*** true .          /* all conclusions proved */
   1.509 +
   1.510 +
   1.511 +procedure_liseq_length_28.
   1.512 +*** true .          /* all conclusions proved */
   1.513 +
   1.514 +
   1.515 +For path(s) from assertion of line 15 to finish:
   1.516 +
   1.517 +procedure_liseq_length_29.
   1.518 +H1:    for_all(i2_ : integer, 0 <= i2_ and i2_ <= i - 1 -> element(l, [i2_]) = 
   1.519 +          liseq_ends_at(a, i2_)) .
   1.520 +H2:    element(l, [pmax]) = liseq_prfx(a, i) .
   1.521 +H3:    i <= l__index__subtype__1__last + 1 .
   1.522 +H4:    0 <= pmax .
   1.523 +H5:    pmax < i .
   1.524 +H6:    a__index__subtype__1__first = 0 .
   1.525 +H7:    l__index__subtype__1__first = 0 .
   1.526 +H8:    a__index__subtype__1__last = l__index__subtype__1__last .
   1.527 +H9:    a__index__subtype__1__last < 2147483647 .
   1.528 +H10:   for_all(i___1 : integer, a__index__subtype__1__first <= i___1 and i___1 
   1.529 +          <= a__index__subtype__1__last -> - 2147483648 <= element(a, [i___1]) 
   1.530 +          and element(a, [i___1]) <= 2147483647) .
   1.531 +H11:   for_all(i___1 : integer, l__index__subtype__1__first <= i___1 and i___1 
   1.532 +          <= l__index__subtype__1__last -> - 2147483648 <= element(l, [i___1]) 
   1.533 +          and element(l, [i___1]) <= 2147483647) .
   1.534 +H12:   i <= 2147483647 .
   1.535 +H13:   l__index__subtype__1__last < i .
   1.536 +H14:   integer__size >= 0 .
   1.537 +H15:   a__index__subtype__1__first <= a__index__subtype__1__last .
   1.538 +H16:   l__index__subtype__1__first <= l__index__subtype__1__last .
   1.539 +H17:   a__index__subtype__1__first >= - 2147483648 .
   1.540 +H18:   a__index__subtype__1__last >= - 2147483648 .
   1.541 +H19:   l__index__subtype__1__first >= - 2147483648 .
   1.542 +H20:   l__index__subtype__1__last >= - 2147483648 .
   1.543 +H21:   a__index__subtype__1__last <= 2147483647 .
   1.544 +H22:   a__index__subtype__1__first <= 2147483647 .
   1.545 +H23:   l__index__subtype__1__last <= 2147483647 .
   1.546 +H24:   l__index__subtype__1__first <= 2147483647 .
   1.547 +       ->
   1.548 +C1:    element(l, [pmax]) = liseq_prfx(a, a__index__subtype__1__last + 1) .
   1.549 +
   1.550 +