*****************************************************************************
                       Semantic Analysis of SPARK Text
                             Examiner GPL Edition

*****************************************************************************



SPARK Simplifier GPL 2012
Copyright (C) 2012 Altran Praxis Limited, Bath, U.K.

procedure Parser_Utilities.ConvertTimeString






@@@@@@@@@@  VC: procedure_converttimestring_1.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  true
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  true
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  true
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  true
%%%  Simplified C6 on reading formula in, to give:
     %%%  C6:  true
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified C8 on reading formula in, to give:
     %%%  C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  true
%%%  Simplified C11 on reading formula in, to give:
     %%%  C11:  true
***  Proved C2:  true
***  Proved C3:  true
***  Proved C4:  true
***  Proved C5:  true
***  Proved C6:  true
***  Proved C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
     using hypothesis H2.
***  Proved C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
     using hypothesis H1.
***  Proved C9:  true
***  Proved C11:  true
-S-  Applied substitution rule converttimes_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__max_year by:
          2020.
<S>  New C1:  true
-S-  Applied substitution rule converttimes_rules(34).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__first by:
          1.
<S>  New H1:  for_all(i_ : integer, 1 <= i_ and i_ <= 
          rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
<S>  New C10:  1 <= rr_type__rrsig_record_type__timestringtypeindex__last
<S>  New C12:  1 <= rr_type__rrsig_record_type__timestringtypeindex__last
-S-  Applied substitution rule converttimes_rules(35).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__last by:
          14.
<S>  New H1:  for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
          timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
<S>  New C10:  true
<S>  New C12:  true
***  Proved C1:  true
***  Proved C10:  true
***  Proved C12:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_2.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H23).
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified C8 on reading formula in, to give:
     %%%  C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
***  Proved C2:  month <= 12
     using hypothesis H2.
***  Proved C3:  day <= 31
     using hypothesis H3.
***  Proved C4:  hour <= 23
     using hypothesis H4.
***  Proved C5:  minute <= 59
     using hypothesis H5.
***  Proved C6:  second <= 59
     using hypothesis H6.
***  Proved C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
     using hypothesis H7.
***  Proved C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
     using hypothesis H8.
***  Proved C9:  loop__1__i + 1 >= 
          rr_type__rrsig_record_type__timestringtypeindex__first
     using hypothesis H9.
***  Proved C11:  loop__1__i + 1 >= 
          rr_type__rrsig_record_type__timestringtypeindex__first
     using hypothesis H9.
-S-  Applied substitution rule converttimes_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__max_year by:
          2020.
<S>  New H1:  year <= 2020
<S>  New H38:  not (10 * year + (element(timestring, [loop__1__i]) - 48) > 2020 
          or (month > monthsinayear or day > maxdaysinamonth or hour >= 
          hoursinaday or minute >= minutesinanhour or second >= 
          secondsinaminute))
<S>  New C1:  10 * year + (element(timestring, [loop__1__i]) - 48) <= 2020
-S-  Applied substitution rule converttimes_rules(35).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__last by:
          14.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> character__first <= element(timestring, [i___1]) and 
          element(timestring, [i___1]) <= character__last)
<S>  New H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= 14 -> 48 <= element(timestring, [i_]) and element(timestring, [i_])
           <= 57)
<S>  New H10:  loop__1__i <= 14
<S>  New H39:  not loop__1__i = 14
<S>  New C10:  loop__1__i <= 13
<S>  New C12:  loop__1__i <= 13
***  Proved C10:  loop__1__i <= 13
     using hypotheses H10 & H39.
***  Proved C12:  loop__1__i <= 13
     using hypotheses H10 & H39.
>>>  Restructured hypothesis H38 into:
     >>>  H38:  10 * year + (element(timestring, [loop__1__i]) - 48) <= 2020 
          and (month <= monthsinayear and day <= maxdaysinamonth and hour < 
          hoursinaday and minute < minutesinanhour and second < 
          secondsinaminute)
>>>  Restructured hypothesis H39 into:
     >>>  H39:  loop__1__i <> 14
>>>  Hypothesis H38 has now been split into two, giving:
     >>>  H40:  10 * year + (element(timestring, [loop__1__i]) - 48) <= 2020
     >>>  H41:  month <= monthsinayear and day <= maxdaysinamonth and hour < 
          hoursinaday and minute < minutesinanhour and second < secondsinaminute
>>>  Hypothesis H41 has now been split into two, giving:
     >>>  H42:  month <= monthsinayear and day <= maxdaysinamonth and hour < 
          hoursinaday and minute < minutesinanhour
     >>>  H43:  second < secondsinaminute
>>>  Hypothesis H42 has now been split into two, giving:
     >>>  H44:  month <= monthsinayear and day <= maxdaysinamonth and hour < 
          hoursinaday
     >>>  H45:  minute < minutesinanhour
>>>  Hypothesis H44 has now been split into two, giving:
     >>>  H46:  month <= monthsinayear and day <= maxdaysinamonth
     >>>  H47:  hour < hoursinaday
>>>  Hypothesis H46 has now been split into two, giving:
     >>>  H48:  month <= monthsinayear
     >>>  H49:  day <= maxdaysinamonth
-S-  Applied substitution rule converttimes_rules(2).
     This was achieved by replacing all occurrences of secondsinaminute by:
          60.
<S>  New H43:  second < 60
-S-  Applied substitution rule converttimes_rules(3).
     This was achieved by replacing all occurrences of minutesinanhour by:
          60.
<S>  New H45:  minute < 60
-S-  Applied substitution rule converttimes_rules(4).
     This was achieved by replacing all occurrences of hoursinaday by:
          24.
<S>  New H47:  hour < 24
-S-  Applied substitution rule converttimes_rules(5).
     This was achieved by replacing all occurrences of maxdaysinamonth by:
          31.
<S>  New H49:  day <= 31
-S-  Applied substitution rule converttimes_rules(6).
     This was achieved by replacing all occurrences of monthsinayear by:
          12.
<S>  New H48:  month <= 12
-S-  Applied substitution rule converttimes_rules(10).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H24:  10 * year >= - 2147483648
-S-  Applied substitution rule converttimes_rules(11).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H25:  10 * year <= 2147483647
-S-  Applied substitution rule converttimes_rules(13).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
-S-  Applied substitution rule converttimes_rules(14).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= 255)
-S-  Applied substitution rule converttimes_rules(18).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H13:  element(timestring, [loop__1__i]) >= 48
<S>  New H18:  year >= 0
<S>  New H22:  10 * year + (element(timestring, [loop__1__i]) - 48) >= 0
<S>  New H28:  month >= 0
<S>  New H30:  day >= 0
<S>  New H32:  hour >= 0
<S>  New H34:  minute >= 0
<S>  New H36:  second >= 0
-S-  Applied substitution rule converttimes_rules(19).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H14:  element(timestring, [loop__1__i]) <= 2147483695
<S>  New H19:  year <= 2147483647
<S>  New H23:  10 * year + (element(timestring, [loop__1__i]) - 48) <= 
          2147483647
<S>  New H29:  month <= 2147483647
<S>  New H31:  day <= 2147483647
<S>  New H33:  hour <= 2147483647
<S>  New H35:  minute <= 2147483647
<S>  New H37:  second <= 2147483647
-S-  Applied substitution rule converttimes_rules(34).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__first by:
          1.
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
          timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H9:  loop__1__i >= 1
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <= 
          element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
%%%  Hypotheses H10 & H39 together imply that
          loop__1__i < 14.
     H10 & H39 have therefore been deleted and a new H50 added to this effect.
***  Proved C1:  10 * year + (element(timestring, [loop__1__i]) - 48) <= 2020
     using hypothesis H40.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_3.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H24).
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified C8 on reading formula in, to give:
     %%%  C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
***  Proved C1:  year <= rr_type__rrsig_record_type__max_year
     using hypothesis H1.
***  Proved C3:  day <= 31
     using hypothesis H3.
***  Proved C4:  hour <= 23
     using hypothesis H4.
***  Proved C5:  minute <= 59
     using hypothesis H5.
***  Proved C6:  second <= 59
     using hypothesis H6.
***  Proved C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
     using hypothesis H7.
***  Proved C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
     using hypothesis H8.
***  Proved C9:  loop__1__i + 1 >= 
          rr_type__rrsig_record_type__timestringtypeindex__first
     using hypothesis H9.
***  Proved C11:  loop__1__i + 1 >= 
          rr_type__rrsig_record_type__timestringtypeindex__first
     using hypothesis H9.
-S-  Applied substitution rule converttimes_rules(35).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__last by:
          14.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> character__first <= element(timestring, [i___1]) and 
          element(timestring, [i___1]) <= character__last)
<S>  New H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= 14 -> 48 <= element(timestring, [i_]) and element(timestring, [i_])
           <= 57)
<S>  New H10:  loop__1__i <= 14
<S>  New H40:  not loop__1__i = 14
<S>  New C10:  loop__1__i <= 13
<S>  New C12:  loop__1__i <= 13
***  Proved C10:  loop__1__i <= 13
     using hypotheses H10 & H40.
***  Proved C12:  loop__1__i <= 13
     using hypotheses H10 & H40.
>>>  Restructured hypothesis H17 into:
     >>>  H17:  4 < loop__1__i
>>>  Restructured hypothesis H39 into:
     >>>  H39:  year <= rr_type__rrsig_record_type__max_year and (10 * month + (
          element(timestring, [loop__1__i]) - 48) <= monthsinayear and day <= 
          maxdaysinamonth and hour < hoursinaday and minute < minutesinanhour 
          and second < secondsinaminute)
>>>  Restructured hypothesis H40 into:
     >>>  H40:  loop__1__i <> 14
---  Attempted addition of new hypothesis:
          year <= rr_type__rrsig_record_type__max_year
     eliminated: this already exists (as H1).
>>>  Hypothesis H39 has now been split into two, giving:
     >>>  H1:  year <= rr_type__rrsig_record_type__max_year
     >>>  H41:  10 * month + (element(timestring, [loop__1__i]) - 48) <= 
          monthsinayear and day <= maxdaysinamonth and hour < hoursinaday and 
          minute < minutesinanhour and second < secondsinaminute
>>>  Hypothesis H41 has now been split into two, giving:
     >>>  H42:  10 * month + (element(timestring, [loop__1__i]) - 48) <= 
          monthsinayear and day <= maxdaysinamonth and hour < hoursinaday and 
          minute < minutesinanhour
     >>>  H43:  second < secondsinaminute
>>>  Hypothesis H42 has now been split into two, giving:
     >>>  H44:  10 * month + (element(timestring, [loop__1__i]) - 48) <= 
          monthsinayear and day <= maxdaysinamonth and hour < hoursinaday
     >>>  H45:  minute < minutesinanhour
>>>  Hypothesis H44 has now been split into two, giving:
     >>>  H46:  10 * month + (element(timestring, [loop__1__i]) - 48) <= 
          monthsinayear and day <= maxdaysinamonth
     >>>  H47:  hour < hoursinaday
>>>  Hypothesis H46 has now been split into two, giving:
     >>>  H48:  10 * month + (element(timestring, [loop__1__i]) - 48) <= 
          monthsinayear
     >>>  H49:  day <= maxdaysinamonth
-S-  Applied substitution rule converttimes_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__max_year by:
          2020.
<S>  New H1:  year <= 2020
-S-  Applied substitution rule converttimes_rules(2).
     This was achieved by replacing all occurrences of secondsinaminute by:
          60.
<S>  New H43:  second < 60
-S-  Applied substitution rule converttimes_rules(3).
     This was achieved by replacing all occurrences of minutesinanhour by:
          60.
<S>  New H45:  minute < 60
-S-  Applied substitution rule converttimes_rules(4).
     This was achieved by replacing all occurrences of hoursinaday by:
          24.
<S>  New H47:  hour < 24
-S-  Applied substitution rule converttimes_rules(5).
     This was achieved by replacing all occurrences of maxdaysinamonth by:
          31.
<S>  New H49:  day <= 31
-S-  Applied substitution rule converttimes_rules(6).
     This was achieved by replacing all occurrences of monthsinayear by:
          12.
<S>  New H48:  10 * month + (element(timestring, [loop__1__i]) - 48) <= 12
-S-  Applied substitution rule converttimes_rules(10).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H25:  10 * month >= - 2147483648
-S-  Applied substitution rule converttimes_rules(11).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H26:  10 * month <= 2147483647
-S-  Applied substitution rule converttimes_rules(13).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
-S-  Applied substitution rule converttimes_rules(14).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= 255)
-S-  Applied substitution rule converttimes_rules(18).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H13:  element(timestring, [loop__1__i]) >= 48
<S>  New H19:  month >= 0
<S>  New H23:  10 * month + (element(timestring, [loop__1__i]) - 48) >= 0
<S>  New H27:  year >= 0
<S>  New H31:  day >= 0
<S>  New H33:  hour >= 0
<S>  New H35:  minute >= 0
<S>  New H37:  second >= 0
-S-  Applied substitution rule converttimes_rules(19).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H14:  element(timestring, [loop__1__i]) <= 2147483695
<S>  New H20:  month <= 2147483647
<S>  New H24:  10 * month + (element(timestring, [loop__1__i]) - 48) <= 
          2147483647
<S>  New H28:  year <= 2147483647
<S>  New H32:  day <= 2147483647
<S>  New H34:  hour <= 2147483647
<S>  New H36:  minute <= 2147483647
<S>  New H38:  second <= 2147483647
-S-  Applied substitution rule converttimes_rules(34).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__first by:
          1.
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
          timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H9:  loop__1__i >= 1
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <= 
          element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
%%%  Hypotheses H10 & H40 together imply that
          loop__1__i < 14.
     H10 & H40 have therefore been deleted and a new H50 added to this effect.
***  Proved C2:  10 * month + (element(timestring, [loop__1__i]) - 48) <= 12
     using hypothesis H48.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_4.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H25).
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified C8 on reading formula in, to give:
     %%%  C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
***  Proved C1:  year <= rr_type__rrsig_record_type__max_year
     using hypothesis H1.
***  Proved C2:  month <= 12
     using hypothesis H2.
***  Proved C4:  hour <= 23
     using hypothesis H4.
***  Proved C5:  minute <= 59
     using hypothesis H5.
***  Proved C6:  second <= 59
     using hypothesis H6.
***  Proved C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
     using hypothesis H7.
***  Proved C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
     using hypothesis H8.
***  Proved C9:  loop__1__i + 1 >= 
          rr_type__rrsig_record_type__timestringtypeindex__first
     using hypothesis H9.
***  Proved C11:  loop__1__i + 1 >= 
          rr_type__rrsig_record_type__timestringtypeindex__first
     using hypothesis H9.
-S-  Applied substitution rule converttimes_rules(35).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__last by:
          14.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> character__first <= element(timestring, [i___1]) and 
          element(timestring, [i___1]) <= character__last)
<S>  New H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= 14 -> 48 <= element(timestring, [i_]) and element(timestring, [i_])
           <= 57)
<S>  New H10:  loop__1__i <= 14
<S>  New H41:  not loop__1__i = 14
<S>  New C10:  loop__1__i <= 13
<S>  New C12:  loop__1__i <= 13
***  Proved C10:  loop__1__i <= 13
     using hypotheses H10 & H41.
***  Proved C12:  loop__1__i <= 13
     using hypotheses H10 & H41.
>>>  Restructured hypothesis H17 into:
     >>>  H17:  4 < loop__1__i
>>>  Restructured hypothesis H18 into:
     >>>  H18:  6 < loop__1__i
>>>  Restructured hypothesis H40 into:
     >>>  H40:  year <= rr_type__rrsig_record_type__max_year and (month <= 
          monthsinayear and 10 * day + (element(timestring, [loop__1__i]) - 48) 
          <= maxdaysinamonth and hour < hoursinaday and minute < 
          minutesinanhour and second < secondsinaminute)
>>>  Restructured hypothesis H41 into:
     >>>  H41:  loop__1__i <> 14
---  Attempted addition of new hypothesis:
          year <= rr_type__rrsig_record_type__max_year
     eliminated: this already exists (as H1).
>>>  Hypothesis H40 has now been split into two, giving:
     >>>  H1:  year <= rr_type__rrsig_record_type__max_year
     >>>  H42:  month <= monthsinayear and 10 * day + (element(timestring, [
          loop__1__i]) - 48) <= maxdaysinamonth and hour < hoursinaday and 
          minute < minutesinanhour and second < secondsinaminute
>>>  Hypothesis H42 has now been split into two, giving:
     >>>  H43:  month <= monthsinayear and 10 * day + (element(timestring, [
          loop__1__i]) - 48) <= maxdaysinamonth and hour < hoursinaday and 
          minute < minutesinanhour
     >>>  H44:  second < secondsinaminute
>>>  Hypothesis H43 has now been split into two, giving:
     >>>  H45:  month <= monthsinayear and 10 * day + (element(timestring, [
          loop__1__i]) - 48) <= maxdaysinamonth and hour < hoursinaday
     >>>  H46:  minute < minutesinanhour
>>>  Hypothesis H45 has now been split into two, giving:
     >>>  H47:  month <= monthsinayear and 10 * day + (element(timestring, [
          loop__1__i]) - 48) <= maxdaysinamonth
     >>>  H48:  hour < hoursinaday
>>>  Hypothesis H47 has now been split into two, giving:
     >>>  H49:  month <= monthsinayear
     >>>  H50:  10 * day + (element(timestring, [loop__1__i]) - 48) <= 
          maxdaysinamonth
-S-  Applied substitution rule converttimes_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__max_year by:
          2020.
<S>  New H1:  year <= 2020
-S-  Applied substitution rule converttimes_rules(2).
     This was achieved by replacing all occurrences of secondsinaminute by:
          60.
<S>  New H44:  second < 60
-S-  Applied substitution rule converttimes_rules(3).
     This was achieved by replacing all occurrences of minutesinanhour by:
          60.
<S>  New H46:  minute < 60
-S-  Applied substitution rule converttimes_rules(4).
     This was achieved by replacing all occurrences of hoursinaday by:
          24.
<S>  New H48:  hour < 24
-S-  Applied substitution rule converttimes_rules(5).
     This was achieved by replacing all occurrences of maxdaysinamonth by:
          31.
<S>  New H50:  10 * day + (element(timestring, [loop__1__i]) - 48) <= 31
-S-  Applied substitution rule converttimes_rules(6).
     This was achieved by replacing all occurrences of monthsinayear by:
          12.
<S>  New H49:  month <= 12
-S-  Applied substitution rule converttimes_rules(10).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H26:  10 * day >= - 2147483648
-S-  Applied substitution rule converttimes_rules(11).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H27:  10 * day <= 2147483647
-S-  Applied substitution rule converttimes_rules(13).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
-S-  Applied substitution rule converttimes_rules(14).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= 255)
-S-  Applied substitution rule converttimes_rules(18).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H13:  element(timestring, [loop__1__i]) >= 48
<S>  New H20:  day >= 0
<S>  New H24:  10 * day + (element(timestring, [loop__1__i]) - 48) >= 0
<S>  New H28:  year >= 0
<S>  New H30:  month >= 0
<S>  New H34:  hour >= 0
<S>  New H36:  minute >= 0
<S>  New H38:  second >= 0
-S-  Applied substitution rule converttimes_rules(19).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H14:  element(timestring, [loop__1__i]) <= 2147483695
<S>  New H21:  day <= 2147483647
<S>  New H25:  10 * day + (element(timestring, [loop__1__i]) - 48) <= 2147483647
<S>  New H29:  year <= 2147483647
<S>  New H31:  month <= 2147483647
<S>  New H35:  hour <= 2147483647
<S>  New H37:  minute <= 2147483647
<S>  New H39:  second <= 2147483647
-S-  Applied substitution rule converttimes_rules(34).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__first by:
          1.
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
          timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H9:  loop__1__i >= 1
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <= 
          element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
%%%  Hypotheses H10 & H41 together imply that
          loop__1__i < 14.
     H10 & H41 have therefore been deleted and a new H51 added to this effect.
***  Proved C3:  10 * day + (element(timestring, [loop__1__i]) - 48) <= 31
     using hypothesis H50.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_5.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified C8 on reading formula in, to give:
     %%%  C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
***  Proved C1:  year <= rr_type__rrsig_record_type__max_year
     using hypothesis H1.
***  Proved C2:  month <= 12
     using hypothesis H2.
***  Proved C3:  day <= 31
     using hypothesis H3.
***  Proved C5:  minute <= 59
     using hypothesis H5.
***  Proved C6:  second <= 59
     using hypothesis H6.
***  Proved C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
     using hypothesis H7.
***  Proved C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
     using hypothesis H8.
***  Proved C9:  loop__1__i + 1 >= 
          rr_type__rrsig_record_type__timestringtypeindex__first
     using hypothesis H9.
***  Proved C11:  loop__1__i + 1 >= 
          rr_type__rrsig_record_type__timestringtypeindex__first
     using hypothesis H9.
-S-  Applied substitution rule converttimes_rules(35).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__last by:
          14.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> character__first <= element(timestring, [i___1]) and 
          element(timestring, [i___1]) <= character__last)
<S>  New H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= 14 -> 48 <= element(timestring, [i_]) and element(timestring, [i_])
           <= 57)
<S>  New H10:  loop__1__i <= 14
<S>  New H42:  not loop__1__i = 14
<S>  New C10:  loop__1__i <= 13
<S>  New C12:  loop__1__i <= 13
***  Proved C10:  loop__1__i <= 13
     using hypotheses H10 & H42.
***  Proved C12:  loop__1__i <= 13
     using hypotheses H10 & H42.
>>>  Restructured hypothesis H17 into:
     >>>  H17:  4 < loop__1__i
>>>  Restructured hypothesis H18 into:
     >>>  H18:  6 < loop__1__i
>>>  Restructured hypothesis H19 into:
     >>>  H19:  8 < loop__1__i
>>>  Restructured hypothesis H41 into:
     >>>  H41:  year <= rr_type__rrsig_record_type__max_year and (month <= 
          monthsinayear and day <= maxdaysinamonth and 10 * hour + (element(
          timestring, [loop__1__i]) - 48) < hoursinaday and minute < 
          minutesinanhour and second < secondsinaminute)
>>>  Restructured hypothesis H42 into:
     >>>  H42:  loop__1__i <> 14
---  Attempted addition of new hypothesis:
          year <= rr_type__rrsig_record_type__max_year
     eliminated: this already exists (as H1).
>>>  Hypothesis H41 has now been split into two, giving:
     >>>  H1:  year <= rr_type__rrsig_record_type__max_year
     >>>  H43:  month <= monthsinayear and day <= maxdaysinamonth and 10 * hour 
          + (element(timestring, [loop__1__i]) - 48) < hoursinaday and minute < 
          minutesinanhour and second < secondsinaminute
>>>  Hypothesis H43 has now been split into two, giving:
     >>>  H44:  month <= monthsinayear and day <= maxdaysinamonth and 10 * hour 
          + (element(timestring, [loop__1__i]) - 48) < hoursinaday and minute < 
          minutesinanhour
     >>>  H45:  second < secondsinaminute
>>>  Hypothesis H44 has now been split into two, giving:
     >>>  H46:  month <= monthsinayear and day <= maxdaysinamonth and 10 * hour 
          + (element(timestring, [loop__1__i]) - 48) < hoursinaday
     >>>  H47:  minute < minutesinanhour
>>>  Hypothesis H46 has now been split into two, giving:
     >>>  H48:  month <= monthsinayear and day <= maxdaysinamonth
     >>>  H49:  10 * hour + (element(timestring, [loop__1__i]) - 48) < 
          hoursinaday
>>>  Hypothesis H48 has now been split into two, giving:
     >>>  H50:  month <= monthsinayear
     >>>  H51:  day <= maxdaysinamonth
-S-  Applied substitution rule converttimes_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__max_year by:
          2020.
<S>  New H1:  year <= 2020
-S-  Applied substitution rule converttimes_rules(2).
     This was achieved by replacing all occurrences of secondsinaminute by:
          60.
<S>  New H45:  second < 60
-S-  Applied substitution rule converttimes_rules(3).
     This was achieved by replacing all occurrences of minutesinanhour by:
          60.
<S>  New H47:  minute < 60
-S-  Applied substitution rule converttimes_rules(4).
     This was achieved by replacing all occurrences of hoursinaday by:
          24.
<S>  New H49:  10 * hour + (element(timestring, [loop__1__i]) - 48) < 24
-S-  Applied substitution rule converttimes_rules(5).
     This was achieved by replacing all occurrences of maxdaysinamonth by:
          31.
<S>  New H51:  day <= 31
-S-  Applied substitution rule converttimes_rules(6).
     This was achieved by replacing all occurrences of monthsinayear by:
          12.
<S>  New H50:  month <= 12
-S-  Applied substitution rule converttimes_rules(10).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H27:  10 * hour >= - 2147483648
-S-  Applied substitution rule converttimes_rules(11).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H28:  10 * hour <= 2147483647
-S-  Applied substitution rule converttimes_rules(13).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
-S-  Applied substitution rule converttimes_rules(14).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= 255)
-S-  Applied substitution rule converttimes_rules(18).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H13:  element(timestring, [loop__1__i]) >= 48
<S>  New H21:  hour >= 0
<S>  New H25:  10 * hour + (element(timestring, [loop__1__i]) - 48) >= 0
<S>  New H29:  year >= 0
<S>  New H31:  month >= 0
<S>  New H33:  day >= 0
<S>  New H37:  minute >= 0
<S>  New H39:  second >= 0
-S-  Applied substitution rule converttimes_rules(19).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H14:  element(timestring, [loop__1__i]) <= 2147483695
<S>  New H22:  hour <= 2147483647
<S>  New H26:  10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
          2147483647
<S>  New H30:  year <= 2147483647
<S>  New H32:  month <= 2147483647
<S>  New H34:  day <= 2147483647
<S>  New H38:  minute <= 2147483647
<S>  New H40:  second <= 2147483647
-S-  Applied substitution rule converttimes_rules(34).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__first by:
          1.
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
          timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H9:  loop__1__i >= 1
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <= 
          element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
%%%  Hypotheses H10 & H42 together imply that
          loop__1__i < 14.
     H10 & H42 have therefore been deleted and a new H52 added to this effect.
***  Proved C4:  10 * hour + (element(timestring, [loop__1__i]) - 48) <= 23
     using hypothesis H49.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_6.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H27).
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified C8 on reading formula in, to give:
     %%%  C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
***  Proved C1:  year <= rr_type__rrsig_record_type__max_year
     using hypothesis H1.
***  Proved C2:  month <= 12
     using hypothesis H2.
***  Proved C3:  day <= 31
     using hypothesis H3.
***  Proved C4:  hour <= 23
     using hypothesis H4.
***  Proved C6:  second <= 59
     using hypothesis H6.
***  Proved C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
     using hypothesis H7.
***  Proved C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
     using hypothesis H8.
***  Proved C9:  loop__1__i + 1 >= 
          rr_type__rrsig_record_type__timestringtypeindex__first
     using hypothesis H9.
***  Proved C11:  loop__1__i + 1 >= 
          rr_type__rrsig_record_type__timestringtypeindex__first
     using hypothesis H9.
-S-  Applied substitution rule converttimes_rules(35).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__last by:
          14.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> character__first <= element(timestring, [i___1]) and 
          element(timestring, [i___1]) <= character__last)
<S>  New H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= 14 -> 48 <= element(timestring, [i_]) and element(timestring, [i_])
           <= 57)
<S>  New H10:  loop__1__i <= 14
<S>  New H43:  not loop__1__i = 14
<S>  New C10:  loop__1__i <= 13
<S>  New C12:  loop__1__i <= 13
***  Proved C10:  loop__1__i <= 13
     using hypotheses H10 & H43.
***  Proved C12:  loop__1__i <= 13
     using hypotheses H10 & H43.
>>>  Restructured hypothesis H17 into:
     >>>  H17:  4 < loop__1__i
>>>  Restructured hypothesis H18 into:
     >>>  H18:  6 < loop__1__i
>>>  Restructured hypothesis H19 into:
     >>>  H19:  8 < loop__1__i
>>>  Restructured hypothesis H20 into:
     >>>  H20:  10 < loop__1__i
>>>  Restructured hypothesis H42 into:
     >>>  H42:  year <= rr_type__rrsig_record_type__max_year and (month <= 
          monthsinayear and day <= maxdaysinamonth and hour < hoursinaday and 
          10 * minute + (element(timestring, [loop__1__i]) - 48) < 
          minutesinanhour and second < secondsinaminute)
>>>  Restructured hypothesis H43 into:
     >>>  H43:  loop__1__i <> 14
---  Attempted addition of new hypothesis:
          year <= rr_type__rrsig_record_type__max_year
     eliminated: this already exists (as H1).
>>>  Hypothesis H42 has now been split into two, giving:
     >>>  H1:  year <= rr_type__rrsig_record_type__max_year
     >>>  H44:  month <= monthsinayear and day <= maxdaysinamonth and hour < 
          hoursinaday and 10 * minute + (element(timestring, [loop__1__i]) - 48)
           < minutesinanhour and second < secondsinaminute
>>>  Hypothesis H44 has now been split into two, giving:
     >>>  H45:  month <= monthsinayear and day <= maxdaysinamonth and hour < 
          hoursinaday and 10 * minute + (element(timestring, [loop__1__i]) - 48)
           < minutesinanhour
     >>>  H46:  second < secondsinaminute
>>>  Hypothesis H45 has now been split into two, giving:
     >>>  H47:  month <= monthsinayear and day <= maxdaysinamonth and hour < 
          hoursinaday
     >>>  H48:  10 * minute + (element(timestring, [loop__1__i]) - 48) < 
          minutesinanhour
>>>  Hypothesis H47 has now been split into two, giving:
     >>>  H49:  month <= monthsinayear and day <= maxdaysinamonth
     >>>  H50:  hour < hoursinaday
>>>  Hypothesis H49 has now been split into two, giving:
     >>>  H51:  month <= monthsinayear
     >>>  H52:  day <= maxdaysinamonth
-S-  Applied substitution rule converttimes_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__max_year by:
          2020.
<S>  New H1:  year <= 2020
-S-  Applied substitution rule converttimes_rules(2).
     This was achieved by replacing all occurrences of secondsinaminute by:
          60.
<S>  New H46:  second < 60
-S-  Applied substitution rule converttimes_rules(3).
     This was achieved by replacing all occurrences of minutesinanhour by:
          60.
<S>  New H48:  10 * minute + (element(timestring, [loop__1__i]) - 48) < 60
-S-  Applied substitution rule converttimes_rules(4).
     This was achieved by replacing all occurrences of hoursinaday by:
          24.
<S>  New H50:  hour < 24
-S-  Applied substitution rule converttimes_rules(5).
     This was achieved by replacing all occurrences of maxdaysinamonth by:
          31.
<S>  New H52:  day <= 31
-S-  Applied substitution rule converttimes_rules(6).
     This was achieved by replacing all occurrences of monthsinayear by:
          12.
<S>  New H51:  month <= 12
-S-  Applied substitution rule converttimes_rules(10).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H28:  10 * minute >= - 2147483648
-S-  Applied substitution rule converttimes_rules(11).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H29:  10 * minute <= 2147483647
-S-  Applied substitution rule converttimes_rules(13).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
-S-  Applied substitution rule converttimes_rules(14).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= 255)
-S-  Applied substitution rule converttimes_rules(18).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H13:  element(timestring, [loop__1__i]) >= 48
<S>  New H22:  minute >= 0
<S>  New H26:  10 * minute + (element(timestring, [loop__1__i]) - 48) >= 0
<S>  New H30:  year >= 0
<S>  New H32:  month >= 0
<S>  New H34:  day >= 0
<S>  New H36:  hour >= 0
<S>  New H40:  second >= 0
-S-  Applied substitution rule converttimes_rules(19).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H14:  element(timestring, [loop__1__i]) <= 2147483695
<S>  New H23:  minute <= 2147483647
<S>  New H27:  10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
          2147483647
<S>  New H31:  year <= 2147483647
<S>  New H33:  month <= 2147483647
<S>  New H35:  day <= 2147483647
<S>  New H37:  hour <= 2147483647
<S>  New H41:  second <= 2147483647
-S-  Applied substitution rule converttimes_rules(34).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__first by:
          1.
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
          timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H9:  loop__1__i >= 1
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <= 
          element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
%%%  Hypotheses H10 & H43 together imply that
          loop__1__i < 14.
     H10 & H43 have therefore been deleted and a new H53 added to this effect.
***  Proved C5:  10 * minute + (element(timestring, [loop__1__i]) - 48) <= 59
     using hypothesis H48.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_7.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified C8 on reading formula in, to give:
     %%%  C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
***  Proved C1:  year <= rr_type__rrsig_record_type__max_year
     using hypothesis H1.
***  Proved C2:  month <= 12
     using hypothesis H2.
***  Proved C3:  day <= 31
     using hypothesis H3.
***  Proved C4:  hour <= 23
     using hypothesis H4.
***  Proved C5:  minute <= 59
     using hypothesis H5.
***  Proved C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
     using hypothesis H7.
***  Proved C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
     using hypothesis H8.
***  Proved C9:  loop__1__i + 1 >= 
          rr_type__rrsig_record_type__timestringtypeindex__first
     using hypothesis H9.
***  Proved C11:  loop__1__i + 1 >= 
          rr_type__rrsig_record_type__timestringtypeindex__first
     using hypothesis H9.
-S-  Applied substitution rule converttimes_rules(35).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__last by:
          14.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> character__first <= element(timestring, [i___1]) and 
          element(timestring, [i___1]) <= character__last)
<S>  New H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= 14 -> 48 <= element(timestring, [i_]) and element(timestring, [i_])
           <= 57)
<S>  New H10:  loop__1__i <= 14
<S>  New H44:  not loop__1__i = 14
<S>  New C10:  loop__1__i <= 13
<S>  New C12:  loop__1__i <= 13
***  Proved C10:  loop__1__i <= 13
     using hypotheses H22 & H44.
***  Proved C12:  loop__1__i <= 13
     using hypotheses H22 & H44.
>>>  Restructured hypothesis H17 into:
     >>>  H17:  4 < loop__1__i
>>>  Restructured hypothesis H18 into:
     >>>  H18:  6 < loop__1__i
>>>  Restructured hypothesis H19 into:
     >>>  H19:  8 < loop__1__i
>>>  Restructured hypothesis H20 into:
     >>>  H20:  10 < loop__1__i
>>>  Restructured hypothesis H21 into:
     >>>  H21:  12 < loop__1__i
>>>  Restructured hypothesis H43 into:
     >>>  H43:  year <= rr_type__rrsig_record_type__max_year and (month <= 
          monthsinayear and day <= maxdaysinamonth and hour < hoursinaday and 
          minute < minutesinanhour and 10 * second + (element(timestring, [
          loop__1__i]) - 48) < secondsinaminute)
>>>  Restructured hypothesis H44 into:
     >>>  H44:  loop__1__i <> 14
---  Attempted addition of new hypothesis:
          year <= rr_type__rrsig_record_type__max_year
     eliminated: this already exists (as H1).
>>>  Hypothesis H43 has now been split into two, giving:
     >>>  H1:  year <= rr_type__rrsig_record_type__max_year
     >>>  H45:  month <= monthsinayear and day <= maxdaysinamonth and hour < 
          hoursinaday and minute < minutesinanhour and 10 * second + (element(
          timestring, [loop__1__i]) - 48) < secondsinaminute
>>>  Hypothesis H45 has now been split into two, giving:
     >>>  H46:  month <= monthsinayear and day <= maxdaysinamonth and hour < 
          hoursinaday and minute < minutesinanhour
     >>>  H47:  10 * second + (element(timestring, [loop__1__i]) - 48) < 
          secondsinaminute
>>>  Hypothesis H46 has now been split into two, giving:
     >>>  H48:  month <= monthsinayear and day <= maxdaysinamonth and hour < 
          hoursinaday
     >>>  H49:  minute < minutesinanhour
>>>  Hypothesis H48 has now been split into two, giving:
     >>>  H50:  month <= monthsinayear and day <= maxdaysinamonth
     >>>  H51:  hour < hoursinaday
>>>  Hypothesis H50 has now been split into two, giving:
     >>>  H52:  month <= monthsinayear
     >>>  H53:  day <= maxdaysinamonth
-S-  Applied substitution rule converttimes_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__max_year by:
          2020.
<S>  New H1:  year <= 2020
-S-  Applied substitution rule converttimes_rules(2).
     This was achieved by replacing all occurrences of secondsinaminute by:
          60.
<S>  New H47:  10 * second + (element(timestring, [loop__1__i]) - 48) < 60
-S-  Applied substitution rule converttimes_rules(3).
     This was achieved by replacing all occurrences of minutesinanhour by:
          60.
<S>  New H49:  minute < 60
-S-  Applied substitution rule converttimes_rules(4).
     This was achieved by replacing all occurrences of hoursinaday by:
          24.
<S>  New H51:  hour < 24
-S-  Applied substitution rule converttimes_rules(5).
     This was achieved by replacing all occurrences of maxdaysinamonth by:
          31.
<S>  New H53:  day <= 31
-S-  Applied substitution rule converttimes_rules(6).
     This was achieved by replacing all occurrences of monthsinayear by:
          12.
<S>  New H52:  month <= 12
-S-  Applied substitution rule converttimes_rules(10).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H29:  10 * second >= - 2147483648
-S-  Applied substitution rule converttimes_rules(11).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H30:  10 * second <= 2147483647
-S-  Applied substitution rule converttimes_rules(13).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
-S-  Applied substitution rule converttimes_rules(14).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= 255)
-S-  Applied substitution rule converttimes_rules(18).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H13:  element(timestring, [loop__1__i]) >= 48
<S>  New H23:  second >= 0
<S>  New H27:  10 * second + (element(timestring, [loop__1__i]) - 48) >= 0
<S>  New H31:  year >= 0
<S>  New H33:  month >= 0
<S>  New H35:  day >= 0
<S>  New H37:  hour >= 0
<S>  New H39:  minute >= 0
-S-  Applied substitution rule converttimes_rules(19).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H14:  element(timestring, [loop__1__i]) <= 2147483695
<S>  New H24:  second <= 2147483647
<S>  New H28:  10 * second + (element(timestring, [loop__1__i]) - 48) <= 
          2147483647
<S>  New H32:  year <= 2147483647
<S>  New H34:  month <= 2147483647
<S>  New H36:  day <= 2147483647
<S>  New H38:  hour <= 2147483647
<S>  New H40:  minute <= 2147483647
-S-  Applied substitution rule converttimes_rules(34).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__first by:
          1.
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
          timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H9:  loop__1__i >= 1
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <= 
          element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
%%%  Hypotheses H10 & H44 together imply that
          loop__1__i < 14.
     H10 & H44 have therefore been deleted and a new H54 added to this effect.
***  Proved C6:  10 * second + (element(timestring, [loop__1__i]) - 48) <= 59
     using hypothesis H47.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_8.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified C8 on reading formula in, to give:
     %%%  C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
***  Proved C1:  year <= rr_type__rrsig_record_type__max_year
     using hypothesis H1.
***  Proved C2:  month <= 12
     using hypothesis H2.
***  Proved C3:  day <= 31
     using hypothesis H3.
***  Proved C4:  hour <= 23
     using hypothesis H4.
***  Proved C5:  minute <= 59
     using hypothesis H5.
***  Proved C6:  second <= 59
     using hypothesis H6.
***  Proved C7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
     using hypothesis H7.
***  Proved C8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
     using hypothesis H8.
***  Proved C9:  loop__1__i + 1 >= 
          rr_type__rrsig_record_type__timestringtypeindex__first
     using hypothesis H9.
***  Proved C11:  loop__1__i + 1 >= 
          rr_type__rrsig_record_type__timestringtypeindex__first
     using hypothesis H9.
-S-  Applied substitution rule converttimes_rules(35).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__last by:
          14.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= 14 -> character__first <= element(timestring, [i___1]) and 
          element(timestring, [i___1]) <= character__last)
<S>  New H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= 14 -> 48 <= element(timestring, [i_]) and element(timestring, [i_])
           <= 57)
<S>  New H10:  loop__1__i <= 14
<S>  New H36:  not loop__1__i = 14
<S>  New C10:  loop__1__i <= 13
<S>  New C12:  loop__1__i <= 13
***  Proved C10:  loop__1__i <= 13
     using hypotheses H10 & H36.
***  Proved C12:  loop__1__i <= 13
     using hypotheses H10 & H36.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_9.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
***  Proved C3:  loop__1__i >= 
          rr_type__rrsig_record_type__timestringtypeindex__first
     using hypothesis H9.
***  Proved C4:  loop__1__i <= 
          rr_type__rrsig_record_type__timestringtypeindex__last
     using hypothesis H10.
-S-  Applied substitution rule converttimes_rules(18).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New C1:  element(timestring, [loop__1__i]) >= 48
-S-  Applied substitution rule converttimes_rules(19).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New C2:  element(timestring, [loop__1__i]) <= 2147483695
***  Proved C1:  element(timestring, [loop__1__i]) >= 48
     using hypotheses H8, H9 & H10.
***  Proved C2:  element(timestring, [loop__1__i]) <= 2147483695
     using hypotheses H8, H9 & H10.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_10.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H14).
-S-  Applied substitution rule converttimes_rules(18).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H13:  element(timestring, [loop__1__i]) >= 48
<S>  New H18:  year >= 0
<S>  New C1:  10 * year + (element(timestring, [loop__1__i]) - 48) >= 0
-S-  Applied substitution rule converttimes_rules(19).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H14:  element(timestring, [loop__1__i]) <= 2147483695
<S>  New H19:  year <= 2147483647
<S>  New C2:  10 * year + (element(timestring, [loop__1__i]) - 48) <= 2147483647
-S-  Applied substitution rule converttimes_rules(10).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C3:  10 * year >= - 2147483648
-S-  Applied substitution rule converttimes_rules(11).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C4:  10 * year <= 2147483647
***  Proved C3:  10 * year >= - 2147483648
     using hypothesis H18.
-S-  Applied substitution rule converttimes_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__max_year by:
          2020.
<S>  New H1:  year <= 2020
-S-  Applied substitution rule converttimes_rules(13).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0 
          <= element(timestring, [i___1]) and element(timestring, [i___1]) <= 
          character__last)
-S-  Applied substitution rule converttimes_rules(14).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0 
          <= element(timestring, [i___1]) and element(timestring, [i___1]) <= 
          255)
-S-  Applied substitution rule converttimes_rules(34).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__first by:
          1.
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 
          rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H9:  loop__1__i >= 1
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__rrsig_record_type__timestringtypeindex__last -> 0 <= element(
          timestring, [i___1]) and element(timestring, [i___1]) <= 255)
-S-  Applied substitution rule converttimes_rules(35).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__last by:
          14.
<S>  New H10:  loop__1__i <= 14
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
          timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <= 
          element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
***  Proved C1:  10 * year + (element(timestring, [loop__1__i]) - 48) >= 0
     via its standard form, which is:
     Std.Fm C1:  - 48 + (10 * year + element(timestring, [loop__1__i])) >= 0
     using hypotheses H13 & H18.
***  Proved C4:  10 * year <= 2147483647
     using hypothesis H1.
---  Eliminated hypothesis H11 (true-hypothesis).
---  Eliminated hypothesis H12 (true-hypothesis).
---  Eliminated hypothesis H15 (true-hypothesis).
---  Eliminated hypothesis H16 (true-hypothesis).
---  Eliminated hypothesis H20 (true-hypothesis).
---  Eliminated hypothesis H21 (true-hypothesis).
---  Eliminated hypothesis H10 (redundant, given H17).
---  Eliminated hypothesis H19 (redundant, given H1).
***  Proved C2:  10 * year + (element(timestring, [loop__1__i]) - 48) <= 
          2147483647
     using hypotheses H1, H8, H9 & H10.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_11.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H14).
-S-  Applied substitution rule converttimes_rules(18).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H13:  element(timestring, [loop__1__i]) >= 48
<S>  New H19:  month >= 0
<S>  New C1:  10 * month + (element(timestring, [loop__1__i]) - 48) >= 0
-S-  Applied substitution rule converttimes_rules(19).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H14:  element(timestring, [loop__1__i]) <= 2147483695
<S>  New H20:  month <= 2147483647
<S>  New C2:  10 * month + (element(timestring, [loop__1__i]) - 48) <= 
          2147483647
-S-  Applied substitution rule converttimes_rules(10).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C3:  10 * month >= - 2147483648
-S-  Applied substitution rule converttimes_rules(11).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C4:  10 * month <= 2147483647
***  Proved C3:  10 * month >= - 2147483648
     using hypothesis H19.
***  Proved C4:  10 * month <= 2147483647
     using hypothesis H2.
>>>  Restructured hypothesis H17 into:
     >>>  H17:  4 < loop__1__i
-S-  Applied substitution rule converttimes_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__max_year by:
          2020.
<S>  New H1:  year <= 2020
-S-  Applied substitution rule converttimes_rules(13).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0 
          <= element(timestring, [i___1]) and element(timestring, [i___1]) <= 
          character__last)
-S-  Applied substitution rule converttimes_rules(14).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0 
          <= element(timestring, [i___1]) and element(timestring, [i___1]) <= 
          255)
-S-  Applied substitution rule converttimes_rules(34).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__first by:
          1.
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 
          rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H9:  loop__1__i >= 1
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__rrsig_record_type__timestringtypeindex__last -> 0 <= element(
          timestring, [i___1]) and element(timestring, [i___1]) <= 255)
-S-  Applied substitution rule converttimes_rules(35).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__last by:
          14.
<S>  New H10:  loop__1__i <= 14
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
          timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <= 
          element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
***  Proved C1:  10 * month + (element(timestring, [loop__1__i]) - 48) >= 0
     via its standard form, which is:
     Std.Fm C1:  - 48 + (10 * month + element(timestring, [loop__1__i])) >= 0
     using hypotheses H13 & H19.
---  Eliminated hypothesis H11 (true-hypothesis).
---  Eliminated hypothesis H12 (true-hypothesis).
---  Eliminated hypothesis H15 (true-hypothesis).
---  Eliminated hypothesis H16 (true-hypothesis).
---  Eliminated hypothesis H21 (true-hypothesis).
---  Eliminated hypothesis H22 (true-hypothesis).
---  Eliminated hypothesis H9 (redundant, given H17).
---  Eliminated hypothesis H10 (redundant, given H18).
---  Eliminated hypothesis H20 (redundant, given H2).
***  Proved C2:  10 * month + (element(timestring, [loop__1__i]) - 48) <= 
          2147483647
     using hypotheses H2, H8, H9 & H10.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_12.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H14).
-S-  Applied substitution rule converttimes_rules(18).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H13:  element(timestring, [loop__1__i]) >= 48
<S>  New H20:  day >= 0
<S>  New C1:  10 * day + (element(timestring, [loop__1__i]) - 48) >= 0
-S-  Applied substitution rule converttimes_rules(19).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H14:  element(timestring, [loop__1__i]) <= 2147483695
<S>  New H21:  day <= 2147483647
<S>  New C2:  10 * day + (element(timestring, [loop__1__i]) - 48) <= 2147483647
-S-  Applied substitution rule converttimes_rules(10).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C3:  10 * day >= - 2147483648
-S-  Applied substitution rule converttimes_rules(11).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C4:  10 * day <= 2147483647
***  Proved C3:  10 * day >= - 2147483648
     using hypothesis H20.
***  Proved C4:  10 * day <= 2147483647
     using hypothesis H3.
>>>  Restructured hypothesis H17 into:
     >>>  H17:  4 < loop__1__i
>>>  Restructured hypothesis H18 into:
     >>>  H18:  6 < loop__1__i
-S-  Applied substitution rule converttimes_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__max_year by:
          2020.
<S>  New H1:  year <= 2020
-S-  Applied substitution rule converttimes_rules(13).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0 
          <= element(timestring, [i___1]) and element(timestring, [i___1]) <= 
          character__last)
-S-  Applied substitution rule converttimes_rules(14).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0 
          <= element(timestring, [i___1]) and element(timestring, [i___1]) <= 
          255)
-S-  Applied substitution rule converttimes_rules(34).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__first by:
          1.
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 
          rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H9:  loop__1__i >= 1
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__rrsig_record_type__timestringtypeindex__last -> 0 <= element(
          timestring, [i___1]) and element(timestring, [i___1]) <= 255)
-S-  Applied substitution rule converttimes_rules(35).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__last by:
          14.
<S>  New H10:  loop__1__i <= 14
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
          timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <= 
          element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
***  Proved C1:  10 * day + (element(timestring, [loop__1__i]) - 48) >= 0
     via its standard form, which is:
     Std.Fm C1:  - 48 + (10 * day + element(timestring, [loop__1__i])) >= 0
     using hypotheses H13 & H20.
---  Eliminated hypothesis H11 (true-hypothesis).
---  Eliminated hypothesis H12 (true-hypothesis).
---  Eliminated hypothesis H15 (true-hypothesis).
---  Eliminated hypothesis H16 (true-hypothesis).
---  Eliminated hypothesis H22 (true-hypothesis).
---  Eliminated hypothesis H23 (true-hypothesis).
---  Eliminated hypothesis H9 (redundant, given H17).
---  Eliminated hypothesis H10 (redundant, given H19).
---  Eliminated hypothesis H17 (redundant, given H18).
---  Eliminated hypothesis H21 (redundant, given H3).
***  Proved C2:  10 * day + (element(timestring, [loop__1__i]) - 48) <= 
          2147483647
     using hypotheses H3, H8, H9 & H10.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_13.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H14).
-S-  Applied substitution rule converttimes_rules(18).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H13:  element(timestring, [loop__1__i]) >= 48
<S>  New H21:  hour >= 0
<S>  New C1:  10 * hour + (element(timestring, [loop__1__i]) - 48) >= 0
-S-  Applied substitution rule converttimes_rules(19).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H14:  element(timestring, [loop__1__i]) <= 2147483695
<S>  New H22:  hour <= 2147483647
<S>  New C2:  10 * hour + (element(timestring, [loop__1__i]) - 48) <= 2147483647
-S-  Applied substitution rule converttimes_rules(10).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C3:  10 * hour >= - 2147483648
-S-  Applied substitution rule converttimes_rules(11).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C4:  10 * hour <= 2147483647
***  Proved C3:  10 * hour >= - 2147483648
     using hypothesis H21.
***  Proved C4:  10 * hour <= 2147483647
     using hypothesis H4.
>>>  Restructured hypothesis H17 into:
     >>>  H17:  4 < loop__1__i
>>>  Restructured hypothesis H18 into:
     >>>  H18:  6 < loop__1__i
>>>  Restructured hypothesis H19 into:
     >>>  H19:  8 < loop__1__i
-S-  Applied substitution rule converttimes_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__max_year by:
          2020.
<S>  New H1:  year <= 2020
-S-  Applied substitution rule converttimes_rules(13).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0 
          <= element(timestring, [i___1]) and element(timestring, [i___1]) <= 
          character__last)
-S-  Applied substitution rule converttimes_rules(14).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0 
          <= element(timestring, [i___1]) and element(timestring, [i___1]) <= 
          255)
-S-  Applied substitution rule converttimes_rules(34).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__first by:
          1.
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 
          rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H9:  loop__1__i >= 1
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__rrsig_record_type__timestringtypeindex__last -> 0 <= element(
          timestring, [i___1]) and element(timestring, [i___1]) <= 255)
-S-  Applied substitution rule converttimes_rules(35).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__last by:
          14.
<S>  New H10:  loop__1__i <= 14
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
          timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <= 
          element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
***  Proved C1:  10 * hour + (element(timestring, [loop__1__i]) - 48) >= 0
     via its standard form, which is:
     Std.Fm C1:  - 48 + (10 * hour + element(timestring, [loop__1__i])) >= 0
     using hypotheses H13 & H21.
---  Eliminated hypothesis H11 (true-hypothesis).
---  Eliminated hypothesis H12 (true-hypothesis).
---  Eliminated hypothesis H15 (true-hypothesis).
---  Eliminated hypothesis H16 (true-hypothesis).
---  Eliminated hypothesis H23 (true-hypothesis).
---  Eliminated hypothesis H24 (true-hypothesis).
---  Eliminated hypothesis H9 (redundant, given H17).
---  Eliminated hypothesis H10 (redundant, given H20).
---  Eliminated hypothesis H17 (redundant, given H18).
---  Eliminated hypothesis H18 (redundant, given H19).
---  Eliminated hypothesis H22 (redundant, given H4).
***  Proved C2:  10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
          2147483647
     using hypotheses H4, H8, H9 & H10.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_14.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H14).
-S-  Applied substitution rule converttimes_rules(18).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H13:  element(timestring, [loop__1__i]) >= 48
<S>  New H22:  minute >= 0
<S>  New C1:  10 * minute + (element(timestring, [loop__1__i]) - 48) >= 0
-S-  Applied substitution rule converttimes_rules(19).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H14:  element(timestring, [loop__1__i]) <= 2147483695
<S>  New H23:  minute <= 2147483647
<S>  New C2:  10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
          2147483647
-S-  Applied substitution rule converttimes_rules(10).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C3:  10 * minute >= - 2147483648
-S-  Applied substitution rule converttimes_rules(11).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C4:  10 * minute <= 2147483647
***  Proved C3:  10 * minute >= - 2147483648
     using hypothesis H22.
***  Proved C4:  10 * minute <= 2147483647
     using hypothesis H5.
>>>  Restructured hypothesis H17 into:
     >>>  H17:  4 < loop__1__i
>>>  Restructured hypothesis H18 into:
     >>>  H18:  6 < loop__1__i
>>>  Restructured hypothesis H19 into:
     >>>  H19:  8 < loop__1__i
>>>  Restructured hypothesis H20 into:
     >>>  H20:  10 < loop__1__i
-S-  Applied substitution rule converttimes_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__max_year by:
          2020.
<S>  New H1:  year <= 2020
-S-  Applied substitution rule converttimes_rules(13).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0 
          <= element(timestring, [i___1]) and element(timestring, [i___1]) <= 
          character__last)
-S-  Applied substitution rule converttimes_rules(14).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0 
          <= element(timestring, [i___1]) and element(timestring, [i___1]) <= 
          255)
-S-  Applied substitution rule converttimes_rules(34).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__first by:
          1.
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 
          rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H9:  loop__1__i >= 1
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__rrsig_record_type__timestringtypeindex__last -> 0 <= element(
          timestring, [i___1]) and element(timestring, [i___1]) <= 255)
-S-  Applied substitution rule converttimes_rules(35).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__last by:
          14.
<S>  New H10:  loop__1__i <= 14
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
          timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <= 
          element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
***  Proved C1:  10 * minute + (element(timestring, [loop__1__i]) - 48) >= 0
     via its standard form, which is:
     Std.Fm C1:  - 48 + (10 * minute + element(timestring, [loop__1__i])) >= 0
     using hypotheses H13 & H22.
---  Eliminated hypothesis H11 (true-hypothesis).
---  Eliminated hypothesis H12 (true-hypothesis).
---  Eliminated hypothesis H15 (true-hypothesis).
---  Eliminated hypothesis H16 (true-hypothesis).
---  Eliminated hypothesis H24 (true-hypothesis).
---  Eliminated hypothesis H25 (true-hypothesis).
---  Eliminated hypothesis H9 (redundant, given H17).
---  Eliminated hypothesis H10 (redundant, given H21).
---  Eliminated hypothesis H17 (redundant, given H18).
---  Eliminated hypothesis H18 (redundant, given H19).
---  Eliminated hypothesis H19 (redundant, given H20).
---  Eliminated hypothesis H23 (redundant, given H5).
***  Proved C2:  10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
          2147483647
     using hypotheses H5, H8, H9 & H10.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_15.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H14).
-S-  Applied substitution rule converttimes_rules(18).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H13:  element(timestring, [loop__1__i]) >= 48
<S>  New H23:  second >= 0
<S>  New C1:  10 * second + (element(timestring, [loop__1__i]) - 48) >= 0
-S-  Applied substitution rule converttimes_rules(19).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H14:  element(timestring, [loop__1__i]) <= 2147483695
<S>  New H24:  second <= 2147483647
<S>  New C2:  10 * second + (element(timestring, [loop__1__i]) - 48) <= 
          2147483647
-S-  Applied substitution rule converttimes_rules(10).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C3:  10 * second >= - 2147483648
-S-  Applied substitution rule converttimes_rules(11).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C4:  10 * second <= 2147483647
***  Proved C3:  10 * second >= - 2147483648
     using hypothesis H23.
***  Proved C4:  10 * second <= 2147483647
     using hypothesis H6.
>>>  Restructured hypothesis H17 into:
     >>>  H17:  4 < loop__1__i
>>>  Restructured hypothesis H18 into:
     >>>  H18:  6 < loop__1__i
>>>  Restructured hypothesis H19 into:
     >>>  H19:  8 < loop__1__i
>>>  Restructured hypothesis H20 into:
     >>>  H20:  10 < loop__1__i
>>>  Restructured hypothesis H21 into:
     >>>  H21:  12 < loop__1__i
-S-  Applied substitution rule converttimes_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__max_year by:
          2020.
<S>  New H1:  year <= 2020
-S-  Applied substitution rule converttimes_rules(13).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0 
          <= element(timestring, [i___1]) and element(timestring, [i___1]) <= 
          character__last)
-S-  Applied substitution rule converttimes_rules(14).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0 
          <= element(timestring, [i___1]) and element(timestring, [i___1]) <= 
          255)
-S-  Applied substitution rule converttimes_rules(34).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__first by:
          1.
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 
          rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H9:  loop__1__i >= 1
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__rrsig_record_type__timestringtypeindex__last -> 0 <= element(
          timestring, [i___1]) and element(timestring, [i___1]) <= 255)
-S-  Applied substitution rule converttimes_rules(35).
     This was achieved by replacing all occurrences of 
          rr_type__rrsig_record_type__timestringtypeindex__last by:
          14.
<S>  New H10:  loop__1__i <= 14
<S>  New H8:  for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
          timestring, [i_]) and element(timestring, [i_]) <= 57)
<S>  New H7:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <= 
          element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
***  Proved C1:  10 * second + (element(timestring, [loop__1__i]) - 48) >= 0
     via its standard form, which is:
     Std.Fm C1:  - 48 + (10 * second + element(timestring, [loop__1__i])) >= 0
     using hypotheses H13 & H23.
---  Eliminated hypothesis H11 (true-hypothesis).
---  Eliminated hypothesis H12 (true-hypothesis).
---  Eliminated hypothesis H15 (true-hypothesis).
---  Eliminated hypothesis H16 (true-hypothesis).
---  Eliminated hypothesis H25 (true-hypothesis).
---  Eliminated hypothesis H26 (true-hypothesis).
---  Eliminated hypothesis H22 (duplicate of H10).
---  Eliminated hypothesis H9 (redundant, given H17).
---  Eliminated hypothesis H17 (redundant, given H18).
---  Eliminated hypothesis H18 (redundant, given H19).
---  Eliminated hypothesis H19 (redundant, given H20).
---  Eliminated hypothesis H20 (redundant, given H21).
---  Eliminated hypothesis H24 (redundant, given H6).
***  Proved C2:  10 * second + (element(timestring, [loop__1__i]) - 48) <= 
          2147483647
     using hypotheses H6, H8, H9 & H22.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_16.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H38).
-S-  Applied substitution rule converttimes_rules(28).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule converttimes_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_17.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H39).
-S-  Applied substitution rule converttimes_rules(28).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule converttimes_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_18.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H40).
-S-  Applied substitution rule converttimes_rules(28).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule converttimes_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_19.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H41).
-S-  Applied substitution rule converttimes_rules(28).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule converttimes_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_20.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H42).
-S-  Applied substitution rule converttimes_rules(28).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule converttimes_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_21.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H43).
-S-  Applied substitution rule converttimes_rules(28).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule converttimes_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_22.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
-S-  Applied substitution rule converttimes_rules(28).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule converttimes_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_23.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
-S-  Applied substitution rule converttimes_rules(28).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule converttimes_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_24.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H38).
-S-  Applied substitution rule converttimes_rules(28).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule converttimes_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_25.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H39).
-S-  Applied substitution rule converttimes_rules(28).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule converttimes_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_26.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H40).
-S-  Applied substitution rule converttimes_rules(28).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule converttimes_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_27.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H41).
-S-  Applied substitution rule converttimes_rules(28).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule converttimes_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_28.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H28).
-S-  Applied substitution rule converttimes_rules(28).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule converttimes_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_29.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
-S-  Applied substitution rule converttimes_rules(28).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule converttimes_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_30.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H37).
***  Proved C1:  second >= natural__first
     using hypothesis H36.
***  Proved C2:  second <= natural__last
     using hypothesis H37.
***  Proved C3:  minute >= natural__first
     using hypothesis H34.
***  Proved C4:  minute <= natural__last
     using hypothesis H35.
***  Proved C5:  hour >= natural__first
     using hypothesis H32.
***  Proved C6:  hour <= natural__last
     using hypothesis H33.
***  Proved C7:  day >= natural__first
     using hypothesis H30.
***  Proved C8:  day <= natural__last
     using hypothesis H31.
***  Proved C9:  month >= natural__first
     using hypothesis H28.
***  Proved C10:  month <= natural__last
     using hypothesis H29.
***  Proved C11:  10 * year + (element(timestring, [loop__1__i]) - 48) >= 
          natural__first
     using hypothesis H22.
***  Proved C12:  10 * year + (element(timestring, [loop__1__i]) - 48) <= 
          natural__last
     using hypothesis H23.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_31.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H38).
***  Proved C1:  second >= natural__first
     using hypothesis H37.
***  Proved C2:  second <= natural__last
     using hypothesis H38.
***  Proved C3:  minute >= natural__first
     using hypothesis H35.
***  Proved C4:  minute <= natural__last
     using hypothesis H36.
***  Proved C5:  hour >= natural__first
     using hypothesis H33.
***  Proved C6:  hour <= natural__last
     using hypothesis H34.
***  Proved C7:  day >= natural__first
     using hypothesis H31.
***  Proved C8:  day <= natural__last
     using hypothesis H32.
***  Proved C9:  10 * month + (element(timestring, [loop__1__i]) - 48) >= 
          natural__first
     using hypothesis H23.
***  Proved C10:  10 * month + (element(timestring, [loop__1__i]) - 48) <= 
          natural__last
     using hypothesis H24.
***  Proved C11:  year >= natural__first
     using hypothesis H27.
***  Proved C12:  year <= natural__last
     using hypothesis H28.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_32.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H39).
***  Proved C1:  second >= natural__first
     using hypothesis H38.
***  Proved C2:  second <= natural__last
     using hypothesis H39.
***  Proved C3:  minute >= natural__first
     using hypothesis H36.
***  Proved C4:  minute <= natural__last
     using hypothesis H37.
***  Proved C5:  hour >= natural__first
     using hypothesis H34.
***  Proved C6:  hour <= natural__last
     using hypothesis H35.
***  Proved C7:  10 * day + (element(timestring, [loop__1__i]) - 48) >= 
          natural__first
     using hypothesis H24.
***  Proved C8:  10 * day + (element(timestring, [loop__1__i]) - 48) <= 
          natural__last
     using hypothesis H25.
***  Proved C9:  month >= natural__first
     using hypothesis H30.
***  Proved C10:  month <= natural__last
     using hypothesis H31.
***  Proved C11:  year >= natural__first
     using hypothesis H28.
***  Proved C12:  year <= natural__last
     using hypothesis H29.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_33.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H40).
***  Proved C1:  second >= natural__first
     using hypothesis H39.
***  Proved C2:  second <= natural__last
     using hypothesis H40.
***  Proved C3:  minute >= natural__first
     using hypothesis H37.
***  Proved C4:  minute <= natural__last
     using hypothesis H38.
***  Proved C5:  10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
          natural__first
     using hypothesis H25.
***  Proved C6:  10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
          natural__last
     using hypothesis H26.
***  Proved C7:  day >= natural__first
     using hypothesis H33.
***  Proved C8:  day <= natural__last
     using hypothesis H34.
***  Proved C9:  month >= natural__first
     using hypothesis H31.
***  Proved C10:  month <= natural__last
     using hypothesis H32.
***  Proved C11:  year >= natural__first
     using hypothesis H29.
***  Proved C12:  year <= natural__last
     using hypothesis H30.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_34.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H41).
***  Proved C1:  second >= natural__first
     using hypothesis H40.
***  Proved C2:  second <= natural__last
     using hypothesis H41.
***  Proved C3:  10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
          natural__first
     using hypothesis H26.
***  Proved C4:  10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
          natural__last
     using hypothesis H27.
***  Proved C5:  hour >= natural__first
     using hypothesis H36.
***  Proved C6:  hour <= natural__last
     using hypothesis H37.
***  Proved C7:  day >= natural__first
     using hypothesis H34.
***  Proved C8:  day <= natural__last
     using hypothesis H35.
***  Proved C9:  month >= natural__first
     using hypothesis H32.
***  Proved C10:  month <= natural__last
     using hypothesis H33.
***  Proved C11:  year >= natural__first
     using hypothesis H30.
***  Proved C12:  year <= natural__last
     using hypothesis H31.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_35.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H28).
***  Proved C1:  10 * second + (element(timestring, [loop__1__i]) - 48) >= 
          natural__first
     using hypothesis H27.
***  Proved C2:  10 * second + (element(timestring, [loop__1__i]) - 48) <= 
          natural__last
     using hypothesis H28.
***  Proved C3:  minute >= natural__first
     using hypothesis H39.
***  Proved C4:  minute <= natural__last
     using hypothesis H40.
***  Proved C5:  hour >= natural__first
     using hypothesis H37.
***  Proved C6:  hour <= natural__last
     using hypothesis H38.
***  Proved C7:  day >= natural__first
     using hypothesis H35.
***  Proved C8:  day <= natural__last
     using hypothesis H36.
***  Proved C9:  month >= natural__first
     using hypothesis H33.
***  Proved C10:  month <= natural__last
     using hypothesis H34.
***  Proved C11:  year >= natural__first
     using hypothesis H31.
***  Proved C12:  year <= natural__last
     using hypothesis H32.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_36.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H34).
***  Proved C1:  second >= natural__first
     using hypothesis H33.
***  Proved C2:  second <= natural__last
     using hypothesis H34.
***  Proved C3:  minute >= natural__first
     using hypothesis H31.
***  Proved C4:  minute <= natural__last
     using hypothesis H32.
***  Proved C5:  hour >= natural__first
     using hypothesis H29.
***  Proved C6:  hour <= natural__last
     using hypothesis H30.
***  Proved C7:  day >= natural__first
     using hypothesis H27.
***  Proved C8:  day <= natural__last
     using hypothesis H28.
***  Proved C9:  month >= natural__first
     using hypothesis H25.
***  Proved C10:  month <= natural__last
     using hypothesis H26.
***  Proved C11:  year >= natural__first
     using hypothesis H23.
***  Proved C12:  year <= natural__last
     using hypothesis H24.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_37.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H37).
***  Proved C1:  second >= natural__first
     using hypothesis H36.
***  Proved C2:  second <= natural__last
     using hypothesis H37.
***  Proved C3:  minute >= natural__first
     using hypothesis H34.
***  Proved C4:  minute <= natural__last
     using hypothesis H35.
***  Proved C5:  hour >= natural__first
     using hypothesis H32.
***  Proved C6:  hour <= natural__last
     using hypothesis H33.
***  Proved C7:  day >= natural__first
     using hypothesis H30.
***  Proved C8:  day <= natural__last
     using hypothesis H31.
***  Proved C9:  month >= natural__first
     using hypothesis H28.
***  Proved C10:  month <= natural__last
     using hypothesis H29.
***  Proved C11:  10 * year + (element(timestring, [loop__1__i]) - 48) >= 
          natural__first
     using hypothesis H22.
***  Proved C12:  10 * year + (element(timestring, [loop__1__i]) - 48) <= 
          natural__last
     using hypothesis H23.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_38.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H38).
***  Proved C1:  second >= natural__first
     using hypothesis H37.
***  Proved C2:  second <= natural__last
     using hypothesis H38.
***  Proved C3:  minute >= natural__first
     using hypothesis H35.
***  Proved C4:  minute <= natural__last
     using hypothesis H36.
***  Proved C5:  hour >= natural__first
     using hypothesis H33.
***  Proved C6:  hour <= natural__last
     using hypothesis H34.
***  Proved C7:  day >= natural__first
     using hypothesis H31.
***  Proved C8:  day <= natural__last
     using hypothesis H32.
***  Proved C9:  10 * month + (element(timestring, [loop__1__i]) - 48) >= 
          natural__first
     using hypothesis H23.
***  Proved C10:  10 * month + (element(timestring, [loop__1__i]) - 48) <= 
          natural__last
     using hypothesis H24.
***  Proved C11:  year >= natural__first
     using hypothesis H27.
***  Proved C12:  year <= natural__last
     using hypothesis H28.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_39.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H39).
***  Proved C1:  second >= natural__first
     using hypothesis H38.
***  Proved C2:  second <= natural__last
     using hypothesis H39.
***  Proved C3:  minute >= natural__first
     using hypothesis H36.
***  Proved C4:  minute <= natural__last
     using hypothesis H37.
***  Proved C5:  hour >= natural__first
     using hypothesis H34.
***  Proved C6:  hour <= natural__last
     using hypothesis H35.
***  Proved C7:  10 * day + (element(timestring, [loop__1__i]) - 48) >= 
          natural__first
     using hypothesis H24.
***  Proved C8:  10 * day + (element(timestring, [loop__1__i]) - 48) <= 
          natural__last
     using hypothesis H25.
***  Proved C9:  month >= natural__first
     using hypothesis H30.
***  Proved C10:  month <= natural__last
     using hypothesis H31.
***  Proved C11:  year >= natural__first
     using hypothesis H28.
***  Proved C12:  year <= natural__last
     using hypothesis H29.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_40.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H40).
***  Proved C1:  second >= natural__first
     using hypothesis H39.
***  Proved C2:  second <= natural__last
     using hypothesis H40.
***  Proved C3:  minute >= natural__first
     using hypothesis H37.
***  Proved C4:  minute <= natural__last
     using hypothesis H38.
***  Proved C5:  10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
          natural__first
     using hypothesis H25.
***  Proved C6:  10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
          natural__last
     using hypothesis H26.
***  Proved C7:  day >= natural__first
     using hypothesis H33.
***  Proved C8:  day <= natural__last
     using hypothesis H34.
***  Proved C9:  month >= natural__first
     using hypothesis H31.
***  Proved C10:  month <= natural__last
     using hypothesis H32.
***  Proved C11:  year >= natural__first
     using hypothesis H29.
***  Proved C12:  year <= natural__last
     using hypothesis H30.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_41.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H42).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H41).
***  Proved C1:  second >= natural__first
     using hypothesis H40.
***  Proved C2:  second <= natural__last
     using hypothesis H41.
***  Proved C3:  10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
          natural__first
     using hypothesis H26.
***  Proved C4:  10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
          natural__last
     using hypothesis H27.
***  Proved C5:  hour >= natural__first
     using hypothesis H36.
***  Proved C6:  hour <= natural__last
     using hypothesis H37.
***  Proved C7:  day >= natural__first
     using hypothesis H34.
***  Proved C8:  day <= natural__last
     using hypothesis H35.
***  Proved C9:  month >= natural__first
     using hypothesis H32.
***  Proved C10:  month <= natural__last
     using hypothesis H33.
***  Proved C11:  year >= natural__first
     using hypothesis H30.
***  Proved C12:  year <= natural__last
     using hypothesis H31.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_42.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H43).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H28).
***  Proved C1:  10 * second + (element(timestring, [loop__1__i]) - 48) >= 
          natural__first
     using hypothesis H27.
***  Proved C2:  10 * second + (element(timestring, [loop__1__i]) - 48) <= 
          natural__last
     using hypothesis H28.
***  Proved C3:  minute >= natural__first
     using hypothesis H39.
***  Proved C4:  minute <= natural__last
     using hypothesis H40.
***  Proved C5:  hour >= natural__first
     using hypothesis H37.
***  Proved C6:  hour <= natural__last
     using hypothesis H38.
***  Proved C7:  day >= natural__first
     using hypothesis H35.
***  Proved C8:  day <= natural__last
     using hypothesis H36.
***  Proved C9:  month >= natural__first
     using hypothesis H33.
***  Proved C10:  month <= natural__last
     using hypothesis H34.
***  Proved C11:  year >= natural__first
     using hypothesis H31.
***  Proved C12:  year <= natural__last
     using hypothesis H32.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_43.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H34).
***  Proved C1:  second >= natural__first
     using hypothesis H33.
***  Proved C2:  second <= natural__last
     using hypothesis H34.
***  Proved C3:  minute >= natural__first
     using hypothesis H31.
***  Proved C4:  minute <= natural__last
     using hypothesis H32.
***  Proved C5:  hour >= natural__first
     using hypothesis H29.
***  Proved C6:  hour <= natural__last
     using hypothesis H30.
***  Proved C7:  day >= natural__first
     using hypothesis H27.
***  Proved C8:  day <= natural__last
     using hypothesis H28.
***  Proved C9:  month >= natural__first
     using hypothesis H25.
***  Proved C10:  month <= natural__last
     using hypothesis H26.
***  Proved C11:  year >= natural__first
     using hypothesis H23.
***  Proved C12:  year <= natural__last
     using hypothesis H24.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_44.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H23).
***  Proved C1:  non_spark_stuff__time_of(10 * year + (element(timestring, [
          loop__1__i]) - 48), month, day, hour, minute, second) >= 
          unsigned_types__unsigned32__first
     using hypothesis H76.
***  Proved C2:  non_spark_stuff__time_of(10 * year + (element(timestring, [
          loop__1__i]) - 48), month, day, hour, minute, second) <= 
          unsigned_types__unsigned32__last
     using hypothesis H77.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_45.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H28).
***  Proved C1:  non_spark_stuff__time_of(year, 10 * month + (element(
          timestring, [loop__1__i]) - 48), day, hour, minute, second) >= 
          unsigned_types__unsigned32__first
     using hypothesis H77.
***  Proved C2:  non_spark_stuff__time_of(year, 10 * month + (element(
          timestring, [loop__1__i]) - 48), day, hour, minute, second) <= 
          unsigned_types__unsigned32__last
     using hypothesis H78.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_46.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H29).
***  Proved C1:  non_spark_stuff__time_of(year, month, 10 * day + (element(
          timestring, [loop__1__i]) - 48), hour, minute, second) >= 
          unsigned_types__unsigned32__first
     using hypothesis H78.
***  Proved C2:  non_spark_stuff__time_of(year, month, 10 * day + (element(
          timestring, [loop__1__i]) - 48), hour, minute, second) <= 
          unsigned_types__unsigned32__last
     using hypothesis H79.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_47.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H30).
***  Proved C1:  non_spark_stuff__time_of(year, month, day, 10 * hour + (
          element(timestring, [loop__1__i]) - 48), minute, second) >= 
          unsigned_types__unsigned32__first
     using hypothesis H79.
***  Proved C2:  non_spark_stuff__time_of(year, month, day, 10 * hour + (
          element(timestring, [loop__1__i]) - 48), minute, second) <= 
          unsigned_types__unsigned32__last
     using hypothesis H80.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_48.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H79 has been replaced by "true".  (It is already present, as 
          H31).
***  Proved C1:  non_spark_stuff__time_of(year, month, day, hour, 10 * minute + 
          (element(timestring, [loop__1__i]) - 48), second) >= 
          unsigned_types__unsigned32__first
     using hypothesis H80.
***  Proved C2:  non_spark_stuff__time_of(year, month, day, hour, 10 * minute + 
          (element(timestring, [loop__1__i]) - 48), second) <= 
          unsigned_types__unsigned32__last
     using hypothesis H81.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_49.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H79 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H80 has been replaced by "true".  (It is already present, as 
          H32).
***  Proved C1:  non_spark_stuff__time_of(year, month, day, hour, minute, 10 * 
          second + (element(timestring, [loop__1__i]) - 48)) >= 
          unsigned_types__unsigned32__first
     using hypothesis H81.
***  Proved C2:  non_spark_stuff__time_of(year, month, day, hour, minute, 10 * 
          second + (element(timestring, [loop__1__i]) - 48)) <= 
          unsigned_types__unsigned32__last
     using hypothesis H82.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_50.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H24).
***  Proved C1:  non_spark_stuff__time_of(year, month, day, hour, minute, 
          second) >= unsigned_types__unsigned32__first
     using hypothesis H73.
***  Proved C2:  non_spark_stuff__time_of(year, month, day, hour, minute, 
          second) <= unsigned_types__unsigned32__last
     using hypothesis H74.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_51.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H23).
***  Proved C1:  non_spark_stuff__time_of(10 * year + (element(timestring, [
          loop__1__i]) - 48), month, day, hour, minute, second) >= 
          unsigned_types__unsigned32__first
     using hypothesis H77.
***  Proved C2:  non_spark_stuff__time_of(10 * year + (element(timestring, [
          loop__1__i]) - 48), month, day, hour, minute, second) <= 
          unsigned_types__unsigned32__last
     using hypothesis H78.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_52.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H28).
***  Proved C1:  non_spark_stuff__time_of(year, 10 * month + (element(
          timestring, [loop__1__i]) - 48), day, hour, minute, second) >= 
          unsigned_types__unsigned32__first
     using hypothesis H78.
***  Proved C2:  non_spark_stuff__time_of(year, 10 * month + (element(
          timestring, [loop__1__i]) - 48), day, hour, minute, second) <= 
          unsigned_types__unsigned32__last
     using hypothesis H79.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_53.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H29).
***  Proved C1:  non_spark_stuff__time_of(year, month, 10 * day + (element(
          timestring, [loop__1__i]) - 48), hour, minute, second) >= 
          unsigned_types__unsigned32__first
     using hypothesis H79.
***  Proved C2:  non_spark_stuff__time_of(year, month, 10 * day + (element(
          timestring, [loop__1__i]) - 48), hour, minute, second) <= 
          unsigned_types__unsigned32__last
     using hypothesis H80.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_54.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H79 has been replaced by "true".  (It is already present, as 
          H30).
***  Proved C1:  non_spark_stuff__time_of(year, month, day, 10 * hour + (
          element(timestring, [loop__1__i]) - 48), minute, second) >= 
          unsigned_types__unsigned32__first
     using hypothesis H80.
***  Proved C2:  non_spark_stuff__time_of(year, month, day, 10 * hour + (
          element(timestring, [loop__1__i]) - 48), minute, second) <= 
          unsigned_types__unsigned32__last
     using hypothesis H81.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_55.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H42).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H79 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H80 has been replaced by "true".  (It is already present, as 
          H31).
***  Proved C1:  non_spark_stuff__time_of(year, month, day, hour, 10 * minute + 
          (element(timestring, [loop__1__i]) - 48), second) >= 
          unsigned_types__unsigned32__first
     using hypothesis H81.
***  Proved C2:  non_spark_stuff__time_of(year, month, day, hour, 10 * minute + 
          (element(timestring, [loop__1__i]) - 48), second) <= 
          unsigned_types__unsigned32__last
     using hypothesis H82.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_56.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H43).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H39).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H40).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H36).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H79 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H80 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H81 has been replaced by "true".  (It is already present, as 
          H32).
***  Proved C1:  non_spark_stuff__time_of(year, month, day, hour, minute, 10 * 
          second + (element(timestring, [loop__1__i]) - 48)) >= 
          unsigned_types__unsigned32__first
     using hypothesis H82.
***  Proved C2:  non_spark_stuff__time_of(year, month, day, hour, minute, 10 * 
          second + (element(timestring, [loop__1__i]) - 48)) <= 
          unsigned_types__unsigned32__last
     using hypothesis H83.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_57.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  for_all(i___1 : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and 
          i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 
          character__first <= element(timestring, [i___1]) and element(
          timestring, [i___1]) <= character__last)
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i_ : integer, 
          rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_ 
          <= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <= 
          element(timestring, [i_]) and element(timestring, [i_]) <= 57)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H24).
***  Proved C1:  non_spark_stuff__time_of(year, month, day, hour, minute, 
          second) >= unsigned_types__unsigned32__first
     using hypothesis H74.
***  Proved C2:  non_spark_stuff__time_of(year, month, day, hour, minute, 
          second) <= unsigned_types__unsigned32__last
     using hypothesis H75.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_58.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_59.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_60.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_61.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_62.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_63.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_64.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_65.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_66.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_67.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_68.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_69.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_70.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_71.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_72.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_73.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_74.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_75.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_76.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_77.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_78.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_79.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_80.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_81.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_82.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_83.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_84.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_converttimestring_85.  @@@@@@@@@@
***  Proved C1:  true
***  PROVED VC.

