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

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


                procedure Parser_Utilities.ConvertTimeString




For path(s) from start to assertion of line 693:

procedure_converttimestring_1.
H1:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H2:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
        ->
C1:    0 <= rr_type__rrsig_record_type__max_year .
C2:    0 <= 12 .
C3:    0 <= 31 .
C4:    0 <= 23 .
C5:    0 <= 59 .
C6:    0 <= 59 .
C7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
C8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
C9:    rr_type__rrsig_record_type__timestringtypeindex__first >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C10:   rr_type__rrsig_record_type__timestringtypeindex__first <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
C11:   rr_type__rrsig_record_type__timestringtypeindex__first >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C12:   rr_type__rrsig_record_type__timestringtypeindex__first <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
 

For path(s) from assertion of line 693 to assertion of line 693:

procedure_converttimestring_2.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   loop__1__i <= 4 .
H18:   year >= natural__first .
H19:   year <= natural__last .
H20:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H21:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H22:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H23:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H24:   10 * year >= integer__base__first .
H25:   10 * year <= integer__base__last .
H26:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H27:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H28:   month >= natural__first .
H29:   month <= natural__last .
H30:   day >= natural__first .
H31:   day <= natural__last .
H32:   hour >= natural__first .
H33:   hour <= natural__last .
H34:   minute >= natural__first .
H35:   minute <= natural__last .
H36:   second >= natural__first .
H37:   second <= natural__last .
H38:   not ((10 * year + (element(timestring, [loop__1__i]) - 48) > 
           rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H39:   not (loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last) .
        ->
C1:    10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           rr_type__rrsig_record_type__max_year .
C2:    month <= 12 .
C3:    day <= 31 .
C4:    hour <= 23 .
C5:    minute <= 59 .
C6:    second <= 59 .
C7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
C8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
C9:    loop__1__i + 1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C10:   loop__1__i + 1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
C11:   loop__1__i + 1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C12:   loop__1__i + 1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
 

procedure_converttimestring_3.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   loop__1__i <= 6 .
H19:   month >= natural__first .
H20:   month <= natural__last .
H21:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H22:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H23:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H24:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H25:   10 * month >= integer__base__first .
H26:   10 * month <= integer__base__last .
H27:   year >= natural__first .
H28:   year <= natural__last .
H29:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H30:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H31:   day >= natural__first .
H32:   day <= natural__last .
H33:   hour >= natural__first .
H34:   hour <= natural__last .
H35:   minute >= natural__first .
H36:   minute <= natural__last .
H37:   second >= natural__first .
H38:   second <= natural__last .
H39:   not ((year > rr_type__rrsig_record_type__max_year) or (((((10 * 
           month + (element(timestring, [loop__1__i]) - 48) > 
           monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H40:   not (loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last) .
        ->
C1:    year <= rr_type__rrsig_record_type__max_year .
C2:    10 * month + (element(timestring, [loop__1__i]) - 48) <= 12 .
C3:    day <= 31 .
C4:    hour <= 23 .
C5:    minute <= 59 .
C6:    second <= 59 .
C7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
C8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
C9:    loop__1__i + 1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C10:   loop__1__i + 1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
C11:   loop__1__i + 1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C12:   loop__1__i + 1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
 

procedure_converttimestring_4.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   loop__1__i <= 8 .
H20:   day >= natural__first .
H21:   day <= natural__last .
H22:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H23:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H24:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H25:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H26:   10 * day >= integer__base__first .
H27:   10 * day <= integer__base__last .
H28:   year >= natural__first .
H29:   year <= natural__last .
H30:   month >= natural__first .
H31:   month <= natural__last .
H32:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H33:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H34:   hour >= natural__first .
H35:   hour <= natural__last .
H36:   minute >= natural__first .
H37:   minute <= natural__last .
H38:   second >= natural__first .
H39:   second <= natural__last .
H40:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (10 * day + (element(
           timestring, [loop__1__i]) - 48) > 
           maxdaysinamonth)) or (hour >= hoursinaday)) or (
           minute >= minutesinanhour)) or (second >= 
           secondsinaminute))) .
H41:   not (loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last) .
        ->
C1:    year <= rr_type__rrsig_record_type__max_year .
C2:    month <= 12 .
C3:    10 * day + (element(timestring, [loop__1__i]) - 48) <= 31 .
C4:    hour <= 23 .
C5:    minute <= 59 .
C6:    second <= 59 .
C7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
C8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
C9:    loop__1__i + 1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C10:   loop__1__i + 1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
C11:   loop__1__i + 1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C12:   loop__1__i + 1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
 

procedure_converttimestring_5.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   loop__1__i <= 10 .
H21:   hour >= natural__first .
H22:   hour <= natural__last .
H23:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H24:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H25:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H26:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H27:   10 * hour >= integer__base__first .
H28:   10 * hour <= integer__base__last .
H29:   year >= natural__first .
H30:   year <= natural__last .
H31:   month >= natural__first .
H32:   month <= natural__last .
H33:   day >= natural__first .
H34:   day <= natural__last .
H35:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H36:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H37:   minute >= natural__first .
H38:   minute <= natural__last .
H39:   second >= natural__first .
H40:   second <= natural__last .
H41:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (10 * 
           hour + (element(timestring, [loop__1__i]) - 48) >= 
           hoursinaday)) or (minute >= minutesinanhour)) or (
           second >= secondsinaminute))) .
H42:   not (loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last) .
        ->
C1:    year <= rr_type__rrsig_record_type__max_year .
C2:    month <= 12 .
C3:    day <= 31 .
C4:    10 * hour + (element(timestring, [loop__1__i]) - 48) <= 23 .
C5:    minute <= 59 .
C6:    second <= 59 .
C7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
C8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
C9:    loop__1__i + 1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C10:   loop__1__i + 1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
C11:   loop__1__i + 1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C12:   loop__1__i + 1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
 

procedure_converttimestring_6.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   loop__1__i <= 12 .
H22:   minute >= natural__first .
H23:   minute <= natural__last .
H24:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H25:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H26:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H27:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H28:   10 * minute >= integer__base__first .
H29:   10 * minute <= integer__base__last .
H30:   year >= natural__first .
H31:   year <= natural__last .
H32:   month >= natural__first .
H33:   month <= natural__last .
H34:   day >= natural__first .
H35:   day <= natural__last .
H36:   hour >= natural__first .
H37:   hour <= natural__last .
H38:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H39:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H40:   second >= natural__first .
H41:   second <= natural__last .
H42:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (10 * minute + (element(
           timestring, [loop__1__i]) - 48) >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H43:   not (loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last) .
        ->
C1:    year <= rr_type__rrsig_record_type__max_year .
C2:    month <= 12 .
C3:    day <= 31 .
C4:    hour <= 23 .
C5:    10 * minute + (element(timestring, [loop__1__i]) - 48) <= 59 .
C6:    second <= 59 .
C7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
C8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
C9:    loop__1__i + 1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C10:   loop__1__i + 1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
C11:   loop__1__i + 1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C12:   loop__1__i + 1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
 

procedure_converttimestring_7.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   not (loop__1__i <= 12) .
H22:   loop__1__i <= 14 .
H23:   second >= natural__first .
H24:   second <= natural__last .
H25:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H26:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H27:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H28:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H29:   10 * second >= integer__base__first .
H30:   10 * second <= integer__base__last .
H31:   year >= natural__first .
H32:   year <= natural__last .
H33:   month >= natural__first .
H34:   month <= natural__last .
H35:   day >= natural__first .
H36:   day <= natural__last .
H37:   hour >= natural__first .
H38:   hour <= natural__last .
H39:   minute >= natural__first .
H40:   minute <= natural__last .
H41:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H42:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H43:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (10 * second + (element(
           timestring, [loop__1__i]) - 48) >= 
           secondsinaminute))) .
H44:   not (loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last) .
        ->
C1:    year <= rr_type__rrsig_record_type__max_year .
C2:    month <= 12 .
C3:    day <= 31 .
C4:    hour <= 23 .
C5:    minute <= 59 .
C6:    10 * second + (element(timestring, [loop__1__i]) - 48) <= 59 .
C7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
C8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
C9:    loop__1__i + 1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C10:   loop__1__i + 1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
C11:   loop__1__i + 1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C12:   loop__1__i + 1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
 

procedure_converttimestring_8.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   not (loop__1__i <= 12) .
H22:   not (loop__1__i <= 14) .
H23:   year >= natural__first .
H24:   year <= natural__last .
H25:   month >= natural__first .
H26:   month <= natural__last .
H27:   day >= natural__first .
H28:   day <= natural__last .
H29:   hour >= natural__first .
H30:   hour <= natural__last .
H31:   minute >= natural__first .
H32:   minute <= natural__last .
H33:   second >= natural__first .
H34:   second <= natural__last .
H35:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H36:   not (loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last) .
        ->
C1:    year <= rr_type__rrsig_record_type__max_year .
C2:    month <= 12 .
C3:    day <= 31 .
C4:    hour <= 23 .
C5:    minute <= 59 .
C6:    second <= 59 .
C7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
C8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
C9:    loop__1__i + 1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C10:   loop__1__i + 1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
C11:   loop__1__i + 1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C12:   loop__1__i + 1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
 

For path(s) from assertion of line 693 to run-time check associated with statement of line 695:

procedure_converttimestring_9.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
        ->
C1:    element(timestring, [loop__1__i]) - 48 >= natural__first .
C2:    element(timestring, [loop__1__i]) - 48 <= natural__last .
C3:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
C4:    loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
 

For path(s) from assertion of line 693 to run-time check associated with statement of line 697:

procedure_converttimestring_10.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   loop__1__i <= 4 .
H18:   year >= natural__first .
H19:   year <= natural__last .
H20:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H21:   element(timestring, [loop__1__i]) - 48 <= natural__last .
        ->
C1:    10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C2:    10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C3:    10 * year >= integer__base__first .
C4:    10 * year <= integer__base__last .
 

For path(s) from assertion of line 693 to run-time check associated with statement of line 699:

procedure_converttimestring_11.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   loop__1__i <= 6 .
H19:   month >= natural__first .
H20:   month <= natural__last .
H21:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H22:   element(timestring, [loop__1__i]) - 48 <= natural__last .
        ->
C1:    10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C2:    10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C3:    10 * month >= integer__base__first .
C4:    10 * month <= integer__base__last .
 

For path(s) from assertion of line 693 to run-time check associated with statement of line 701:

procedure_converttimestring_12.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   loop__1__i <= 8 .
H20:   day >= natural__first .
H21:   day <= natural__last .
H22:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H23:   element(timestring, [loop__1__i]) - 48 <= natural__last .
        ->
C1:    10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C2:    10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C3:    10 * day >= integer__base__first .
C4:    10 * day <= integer__base__last .
 

For path(s) from assertion of line 693 to run-time check associated with statement of line 703:

procedure_converttimestring_13.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   loop__1__i <= 10 .
H21:   hour >= natural__first .
H22:   hour <= natural__last .
H23:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H24:   element(timestring, [loop__1__i]) - 48 <= natural__last .
        ->
C1:    10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C2:    10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C3:    10 * hour >= integer__base__first .
C4:    10 * hour <= integer__base__last .
 

For path(s) from assertion of line 693 to run-time check associated with statement of line 705:

procedure_converttimestring_14.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   loop__1__i <= 12 .
H22:   minute >= natural__first .
H23:   minute <= natural__last .
H24:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H25:   element(timestring, [loop__1__i]) - 48 <= natural__last .
        ->
C1:    10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C2:    10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C3:    10 * minute >= integer__base__first .
C4:    10 * minute <= integer__base__last .
 

For path(s) from assertion of line 693 to run-time check associated with statement of line 707:

procedure_converttimestring_15.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   not (loop__1__i <= 12) .
H22:   loop__1__i <= 14 .
H23:   second >= natural__first .
H24:   second <= natural__last .
H25:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H26:   element(timestring, [loop__1__i]) - 48 <= natural__last .
        ->
C1:    10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C2:    10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C3:    10 * second >= integer__base__first .
C4:    10 * second <= integer__base__last .
 

For path(s) from assertion of line 693 to run-time check associated with statement of line 717:

procedure_converttimestring_16.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   loop__1__i <= 4 .
H18:   year >= natural__first .
H19:   year <= natural__last .
H20:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H21:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H22:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H23:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H24:   10 * year >= integer__base__first .
H25:   10 * year <= integer__base__last .
H26:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H27:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H28:   month >= natural__first .
H29:   month <= natural__last .
H30:   day >= natural__first .
H31:   day <= natural__last .
H32:   hour >= natural__first .
H33:   hour <= natural__last .
H34:   minute >= natural__first .
H35:   minute <= natural__last .
H36:   second >= natural__first .
H37:   second <= natural__last .
H38:   (10 * year + (element(timestring, [loop__1__i]) - 48) > 
           rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
H39:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H40:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H41:   month >= natural__first .
H42:   month <= natural__last .
H43:   day >= natural__first .
H44:   day <= natural__last .
H45:   hour >= natural__first .
H46:   hour <= natural__last .
H47:   minute >= natural__first .
H48:   minute <= natural__last .
H49:   second >= natural__first .
H50:   second <= natural__last .
H51:   (10 * year + (element(timestring, [loop__1__i]) - 48) > 
           rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_17.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   loop__1__i <= 6 .
H19:   month >= natural__first .
H20:   month <= natural__last .
H21:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H22:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H23:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H24:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H25:   10 * month >= integer__base__first .
H26:   10 * month <= integer__base__last .
H27:   year >= natural__first .
H28:   year <= natural__last .
H29:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H30:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H31:   day >= natural__first .
H32:   day <= natural__last .
H33:   hour >= natural__first .
H34:   hour <= natural__last .
H35:   minute >= natural__first .
H36:   minute <= natural__last .
H37:   second >= natural__first .
H38:   second <= natural__last .
H39:   (year > rr_type__rrsig_record_type__max_year) or (((((10 * 
           month + (element(timestring, [loop__1__i]) - 48) > 
           monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
H40:   year >= natural__first .
H41:   year <= natural__last .
H42:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H43:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H44:   day >= natural__first .
H45:   day <= natural__last .
H46:   hour >= natural__first .
H47:   hour <= natural__last .
H48:   minute >= natural__first .
H49:   minute <= natural__last .
H50:   second >= natural__first .
H51:   second <= natural__last .
H52:   (year > rr_type__rrsig_record_type__max_year) or (((((10 * 
           month + (element(timestring, [loop__1__i]) - 48) > 
           monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_18.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   loop__1__i <= 8 .
H20:   day >= natural__first .
H21:   day <= natural__last .
H22:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H23:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H24:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H25:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H26:   10 * day >= integer__base__first .
H27:   10 * day <= integer__base__last .
H28:   year >= natural__first .
H29:   year <= natural__last .
H30:   month >= natural__first .
H31:   month <= natural__last .
H32:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H33:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H34:   hour >= natural__first .
H35:   hour <= natural__last .
H36:   minute >= natural__first .
H37:   minute <= natural__last .
H38:   second >= natural__first .
H39:   second <= natural__last .
H40:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (10 * day + (element(
           timestring, [loop__1__i]) - 48) > 
           maxdaysinamonth)) or (hour >= hoursinaday)) or (
           minute >= minutesinanhour)) or (second >= 
           secondsinaminute)) .
H41:   year >= natural__first .
H42:   year <= natural__last .
H43:   month >= natural__first .
H44:   month <= natural__last .
H45:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H46:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H47:   hour >= natural__first .
H48:   hour <= natural__last .
H49:   minute >= natural__first .
H50:   minute <= natural__last .
H51:   second >= natural__first .
H52:   second <= natural__last .
H53:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (10 * day + (element(
           timestring, [loop__1__i]) - 48) > 
           maxdaysinamonth)) or (hour >= hoursinaday)) or (
           minute >= minutesinanhour)) or (second >= 
           secondsinaminute)) .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_19.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   loop__1__i <= 10 .
H21:   hour >= natural__first .
H22:   hour <= natural__last .
H23:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H24:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H25:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H26:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H27:   10 * hour >= integer__base__first .
H28:   10 * hour <= integer__base__last .
H29:   year >= natural__first .
H30:   year <= natural__last .
H31:   month >= natural__first .
H32:   month <= natural__last .
H33:   day >= natural__first .
H34:   day <= natural__last .
H35:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H36:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H37:   minute >= natural__first .
H38:   minute <= natural__last .
H39:   second >= natural__first .
H40:   second <= natural__last .
H41:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (10 * 
           hour + (element(timestring, [loop__1__i]) - 48) >= 
           hoursinaday)) or (minute >= minutesinanhour)) or (
           second >= secondsinaminute)) .
H42:   year >= natural__first .
H43:   year <= natural__last .
H44:   month >= natural__first .
H45:   month <= natural__last .
H46:   day >= natural__first .
H47:   day <= natural__last .
H48:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H49:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H50:   minute >= natural__first .
H51:   minute <= natural__last .
H52:   second >= natural__first .
H53:   second <= natural__last .
H54:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (10 * 
           hour + (element(timestring, [loop__1__i]) - 48) >= 
           hoursinaday)) or (minute >= minutesinanhour)) or (
           second >= secondsinaminute)) .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_20.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   loop__1__i <= 12 .
H22:   minute >= natural__first .
H23:   minute <= natural__last .
H24:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H25:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H26:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H27:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H28:   10 * minute >= integer__base__first .
H29:   10 * minute <= integer__base__last .
H30:   year >= natural__first .
H31:   year <= natural__last .
H32:   month >= natural__first .
H33:   month <= natural__last .
H34:   day >= natural__first .
H35:   day <= natural__last .
H36:   hour >= natural__first .
H37:   hour <= natural__last .
H38:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H39:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H40:   second >= natural__first .
H41:   second <= natural__last .
H42:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (10 * minute + (element(
           timestring, [loop__1__i]) - 48) >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
H43:   year >= natural__first .
H44:   year <= natural__last .
H45:   month >= natural__first .
H46:   month <= natural__last .
H47:   day >= natural__first .
H48:   day <= natural__last .
H49:   hour >= natural__first .
H50:   hour <= natural__last .
H51:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H52:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H53:   second >= natural__first .
H54:   second <= natural__last .
H55:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (10 * minute + (element(
           timestring, [loop__1__i]) - 48) >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_21.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   not (loop__1__i <= 12) .
H22:   loop__1__i <= 14 .
H23:   second >= natural__first .
H24:   second <= natural__last .
H25:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H26:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H27:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H28:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H29:   10 * second >= integer__base__first .
H30:   10 * second <= integer__base__last .
H31:   year >= natural__first .
H32:   year <= natural__last .
H33:   month >= natural__first .
H34:   month <= natural__last .
H35:   day >= natural__first .
H36:   day <= natural__last .
H37:   hour >= natural__first .
H38:   hour <= natural__last .
H39:   minute >= natural__first .
H40:   minute <= natural__last .
H41:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H42:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H43:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (10 * second + (element(
           timestring, [loop__1__i]) - 48) >= 
           secondsinaminute)) .
H44:   year >= natural__first .
H45:   year <= natural__last .
H46:   month >= natural__first .
H47:   month <= natural__last .
H48:   day >= natural__first .
H49:   day <= natural__last .
H50:   hour >= natural__first .
H51:   hour <= natural__last .
H52:   minute >= natural__first .
H53:   minute <= natural__last .
H54:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H55:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H56:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (10 * second + (element(
           timestring, [loop__1__i]) - 48) >= 
           secondsinaminute)) .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_22.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   not (loop__1__i <= 12) .
H22:   not (loop__1__i <= 14) .
H23:   year >= natural__first .
H24:   year <= natural__last .
H25:   month >= natural__first .
H26:   month <= natural__last .
H27:   day >= natural__first .
H28:   day <= natural__last .
H29:   hour >= natural__first .
H30:   hour <= natural__last .
H31:   minute >= natural__first .
H32:   minute <= natural__last .
H33:   second >= natural__first .
H34:   second <= natural__last .
H35:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
H36:   year >= natural__first .
H37:   year <= natural__last .
H38:   month >= natural__first .
H39:   month <= natural__last .
H40:   day >= natural__first .
H41:   day <= natural__last .
H42:   hour >= natural__first .
H43:   hour <= natural__last .
H44:   minute >= natural__first .
H45:   minute <= natural__last .
H46:   second >= natural__first .
H47:   second <= natural__last .
H48:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_23.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   loop__1__i <= 4 .
H18:   year >= natural__first .
H19:   year <= natural__last .
H20:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H21:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H22:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H23:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H24:   10 * year >= integer__base__first .
H25:   10 * year <= integer__base__last .
H26:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H27:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H28:   month >= natural__first .
H29:   month <= natural__last .
H30:   day >= natural__first .
H31:   day <= natural__last .
H32:   hour >= natural__first .
H33:   hour <= natural__last .
H34:   minute >= natural__first .
H35:   minute <= natural__last .
H36:   second >= natural__first .
H37:   second <= natural__last .
H38:   not ((10 * year + (element(timestring, [loop__1__i]) - 48) > 
           rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H39:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H40:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H41:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H42:   month >= natural__first .
H43:   month <= natural__last .
H44:   day >= natural__first .
H45:   day <= natural__last .
H46:   hour >= natural__first .
H47:   hour <= natural__last .
H48:   minute >= natural__first .
H49:   minute <= natural__last .
H50:   second >= natural__first .
H51:   second <= natural__last .
H52:   (10 * year + (element(timestring, [loop__1__i]) - 48) > 
           rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_24.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   loop__1__i <= 6 .
H19:   month >= natural__first .
H20:   month <= natural__last .
H21:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H22:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H23:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H24:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H25:   10 * month >= integer__base__first .
H26:   10 * month <= integer__base__last .
H27:   year >= natural__first .
H28:   year <= natural__last .
H29:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H30:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H31:   day >= natural__first .
H32:   day <= natural__last .
H33:   hour >= natural__first .
H34:   hour <= natural__last .
H35:   minute >= natural__first .
H36:   minute <= natural__last .
H37:   second >= natural__first .
H38:   second <= natural__last .
H39:   not ((year > rr_type__rrsig_record_type__max_year) or (((((10 * 
           month + (element(timestring, [loop__1__i]) - 48) > 
           monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H40:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H41:   year >= natural__first .
H42:   year <= natural__last .
H43:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H44:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H45:   day >= natural__first .
H46:   day <= natural__last .
H47:   hour >= natural__first .
H48:   hour <= natural__last .
H49:   minute >= natural__first .
H50:   minute <= natural__last .
H51:   second >= natural__first .
H52:   second <= natural__last .
H53:   (year > rr_type__rrsig_record_type__max_year) or (((((10 * 
           month + (element(timestring, [loop__1__i]) - 48) > 
           monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_25.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   loop__1__i <= 8 .
H20:   day >= natural__first .
H21:   day <= natural__last .
H22:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H23:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H24:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H25:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H26:   10 * day >= integer__base__first .
H27:   10 * day <= integer__base__last .
H28:   year >= natural__first .
H29:   year <= natural__last .
H30:   month >= natural__first .
H31:   month <= natural__last .
H32:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H33:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H34:   hour >= natural__first .
H35:   hour <= natural__last .
H36:   minute >= natural__first .
H37:   minute <= natural__last .
H38:   second >= natural__first .
H39:   second <= natural__last .
H40:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (10 * day + (element(
           timestring, [loop__1__i]) - 48) > 
           maxdaysinamonth)) or (hour >= hoursinaday)) or (
           minute >= minutesinanhour)) or (second >= 
           secondsinaminute))) .
H41:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H42:   year >= natural__first .
H43:   year <= natural__last .
H44:   month >= natural__first .
H45:   month <= natural__last .
H46:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H47:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H48:   hour >= natural__first .
H49:   hour <= natural__last .
H50:   minute >= natural__first .
H51:   minute <= natural__last .
H52:   second >= natural__first .
H53:   second <= natural__last .
H54:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (10 * day + (element(
           timestring, [loop__1__i]) - 48) > 
           maxdaysinamonth)) or (hour >= hoursinaday)) or (
           minute >= minutesinanhour)) or (second >= 
           secondsinaminute)) .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_26.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   loop__1__i <= 10 .
H21:   hour >= natural__first .
H22:   hour <= natural__last .
H23:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H24:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H25:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H26:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H27:   10 * hour >= integer__base__first .
H28:   10 * hour <= integer__base__last .
H29:   year >= natural__first .
H30:   year <= natural__last .
H31:   month >= natural__first .
H32:   month <= natural__last .
H33:   day >= natural__first .
H34:   day <= natural__last .
H35:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H36:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H37:   minute >= natural__first .
H38:   minute <= natural__last .
H39:   second >= natural__first .
H40:   second <= natural__last .
H41:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (10 * 
           hour + (element(timestring, [loop__1__i]) - 48) >= 
           hoursinaday)) or (minute >= minutesinanhour)) or (
           second >= secondsinaminute))) .
H42:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H43:   year >= natural__first .
H44:   year <= natural__last .
H45:   month >= natural__first .
H46:   month <= natural__last .
H47:   day >= natural__first .
H48:   day <= natural__last .
H49:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H50:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H51:   minute >= natural__first .
H52:   minute <= natural__last .
H53:   second >= natural__first .
H54:   second <= natural__last .
H55:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (10 * 
           hour + (element(timestring, [loop__1__i]) - 48) >= 
           hoursinaday)) or (minute >= minutesinanhour)) or (
           second >= secondsinaminute)) .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_27.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   loop__1__i <= 12 .
H22:   minute >= natural__first .
H23:   minute <= natural__last .
H24:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H25:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H26:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H27:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H28:   10 * minute >= integer__base__first .
H29:   10 * minute <= integer__base__last .
H30:   year >= natural__first .
H31:   year <= natural__last .
H32:   month >= natural__first .
H33:   month <= natural__last .
H34:   day >= natural__first .
H35:   day <= natural__last .
H36:   hour >= natural__first .
H37:   hour <= natural__last .
H38:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H39:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H40:   second >= natural__first .
H41:   second <= natural__last .
H42:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (10 * minute + (element(
           timestring, [loop__1__i]) - 48) >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H43:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H44:   year >= natural__first .
H45:   year <= natural__last .
H46:   month >= natural__first .
H47:   month <= natural__last .
H48:   day >= natural__first .
H49:   day <= natural__last .
H50:   hour >= natural__first .
H51:   hour <= natural__last .
H52:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H53:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H54:   second >= natural__first .
H55:   second <= natural__last .
H56:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (10 * minute + (element(
           timestring, [loop__1__i]) - 48) >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_28.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   not (loop__1__i <= 12) .
H22:   loop__1__i <= 14 .
H23:   second >= natural__first .
H24:   second <= natural__last .
H25:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H26:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H27:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H28:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H29:   10 * second >= integer__base__first .
H30:   10 * second <= integer__base__last .
H31:   year >= natural__first .
H32:   year <= natural__last .
H33:   month >= natural__first .
H34:   month <= natural__last .
H35:   day >= natural__first .
H36:   day <= natural__last .
H37:   hour >= natural__first .
H38:   hour <= natural__last .
H39:   minute >= natural__first .
H40:   minute <= natural__last .
H41:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H42:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H43:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (10 * second + (element(
           timestring, [loop__1__i]) - 48) >= 
           secondsinaminute))) .
H44:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H45:   year >= natural__first .
H46:   year <= natural__last .
H47:   month >= natural__first .
H48:   month <= natural__last .
H49:   day >= natural__first .
H50:   day <= natural__last .
H51:   hour >= natural__first .
H52:   hour <= natural__last .
H53:   minute >= natural__first .
H54:   minute <= natural__last .
H55:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H56:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H57:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (10 * second + (element(
           timestring, [loop__1__i]) - 48) >= 
           secondsinaminute)) .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_29.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   not (loop__1__i <= 12) .
H22:   not (loop__1__i <= 14) .
H23:   year >= natural__first .
H24:   year <= natural__last .
H25:   month >= natural__first .
H26:   month <= natural__last .
H27:   day >= natural__first .
H28:   day <= natural__last .
H29:   hour >= natural__first .
H30:   hour <= natural__last .
H31:   minute >= natural__first .
H32:   minute <= natural__last .
H33:   second >= natural__first .
H34:   second <= natural__last .
H35:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H36:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H37:   year >= natural__first .
H38:   year <= natural__last .
H39:   month >= natural__first .
H40:   month <= natural__last .
H41:   day >= natural__first .
H42:   day <= natural__last .
H43:   hour >= natural__first .
H44:   hour <= natural__last .
H45:   minute >= natural__first .
H46:   minute <= natural__last .
H47:   second >= natural__first .
H48:   second <= natural__last .
H49:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
        ->
C1:    0 >= unsigned_types__unsigned32__first .
C2:    0 <= unsigned_types__unsigned32__last .
 

For path(s) from assertion of line 693 to run-time check associated with statement of line 719:

procedure_converttimestring_30.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   loop__1__i <= 4 .
H18:   year >= natural__first .
H19:   year <= natural__last .
H20:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H21:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H22:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H23:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H24:   10 * year >= integer__base__first .
H25:   10 * year <= integer__base__last .
H26:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H27:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H28:   month >= natural__first .
H29:   month <= natural__last .
H30:   day >= natural__first .
H31:   day <= natural__last .
H32:   hour >= natural__first .
H33:   hour <= natural__last .
H34:   minute >= natural__first .
H35:   minute <= natural__last .
H36:   second >= natural__first .
H37:   second <= natural__last .
H38:   (10 * year + (element(timestring, [loop__1__i]) - 48) > 
           rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
H39:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H40:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H41:   month >= natural__first .
H42:   month <= natural__last .
H43:   day >= natural__first .
H44:   day <= natural__last .
H45:   hour >= natural__first .
H46:   hour <= natural__last .
H47:   minute >= natural__first .
H48:   minute <= natural__last .
H49:   second >= natural__first .
H50:   second <= natural__last .
H51:   not ((10 * year + (element(timestring, [loop__1__i]) - 48) > 
           rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H52:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H53:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H54:   month >= natural__first .
H55:   month <= natural__last .
H56:   day >= natural__first .
H57:   day <= natural__last .
H58:   hour >= natural__first .
H59:   hour <= natural__last .
H60:   minute >= natural__first .
H61:   minute <= natural__last .
H62:   second >= natural__first .
H63:   second <= natural__last .
        ->
C1:    second >= natural__first .
C2:    second <= natural__last .
C3:    minute >= natural__first .
C4:    minute <= natural__last .
C5:    hour >= natural__first .
C6:    hour <= natural__last .
C7:    day >= natural__first .
C8:    day <= natural__last .
C9:    month >= natural__first .
C10:   month <= natural__last .
C11:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C12:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
 

procedure_converttimestring_31.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   loop__1__i <= 6 .
H19:   month >= natural__first .
H20:   month <= natural__last .
H21:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H22:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H23:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H24:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H25:   10 * month >= integer__base__first .
H26:   10 * month <= integer__base__last .
H27:   year >= natural__first .
H28:   year <= natural__last .
H29:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H30:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H31:   day >= natural__first .
H32:   day <= natural__last .
H33:   hour >= natural__first .
H34:   hour <= natural__last .
H35:   minute >= natural__first .
H36:   minute <= natural__last .
H37:   second >= natural__first .
H38:   second <= natural__last .
H39:   (year > rr_type__rrsig_record_type__max_year) or (((((10 * 
           month + (element(timestring, [loop__1__i]) - 48) > 
           monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
H40:   year >= natural__first .
H41:   year <= natural__last .
H42:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H43:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H44:   day >= natural__first .
H45:   day <= natural__last .
H46:   hour >= natural__first .
H47:   hour <= natural__last .
H48:   minute >= natural__first .
H49:   minute <= natural__last .
H50:   second >= natural__first .
H51:   second <= natural__last .
H52:   not ((year > rr_type__rrsig_record_type__max_year) or (((((10 * 
           month + (element(timestring, [loop__1__i]) - 48) > 
           monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H53:   year >= natural__first .
H54:   year <= natural__last .
H55:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H56:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H57:   day >= natural__first .
H58:   day <= natural__last .
H59:   hour >= natural__first .
H60:   hour <= natural__last .
H61:   minute >= natural__first .
H62:   minute <= natural__last .
H63:   second >= natural__first .
H64:   second <= natural__last .
        ->
C1:    second >= natural__first .
C2:    second <= natural__last .
C3:    minute >= natural__first .
C4:    minute <= natural__last .
C5:    hour >= natural__first .
C6:    hour <= natural__last .
C7:    day >= natural__first .
C8:    day <= natural__last .
C9:    10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C10:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C11:   year >= natural__first .
C12:   year <= natural__last .
 

procedure_converttimestring_32.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   loop__1__i <= 8 .
H20:   day >= natural__first .
H21:   day <= natural__last .
H22:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H23:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H24:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H25:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H26:   10 * day >= integer__base__first .
H27:   10 * day <= integer__base__last .
H28:   year >= natural__first .
H29:   year <= natural__last .
H30:   month >= natural__first .
H31:   month <= natural__last .
H32:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H33:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H34:   hour >= natural__first .
H35:   hour <= natural__last .
H36:   minute >= natural__first .
H37:   minute <= natural__last .
H38:   second >= natural__first .
H39:   second <= natural__last .
H40:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (10 * day + (element(
           timestring, [loop__1__i]) - 48) > 
           maxdaysinamonth)) or (hour >= hoursinaday)) or (
           minute >= minutesinanhour)) or (second >= 
           secondsinaminute)) .
H41:   year >= natural__first .
H42:   year <= natural__last .
H43:   month >= natural__first .
H44:   month <= natural__last .
H45:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H46:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H47:   hour >= natural__first .
H48:   hour <= natural__last .
H49:   minute >= natural__first .
H50:   minute <= natural__last .
H51:   second >= natural__first .
H52:   second <= natural__last .
H53:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (10 * day + (element(
           timestring, [loop__1__i]) - 48) > 
           maxdaysinamonth)) or (hour >= hoursinaday)) or (
           minute >= minutesinanhour)) or (second >= 
           secondsinaminute))) .
H54:   year >= natural__first .
H55:   year <= natural__last .
H56:   month >= natural__first .
H57:   month <= natural__last .
H58:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H59:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H60:   hour >= natural__first .
H61:   hour <= natural__last .
H62:   minute >= natural__first .
H63:   minute <= natural__last .
H64:   second >= natural__first .
H65:   second <= natural__last .
        ->
C1:    second >= natural__first .
C2:    second <= natural__last .
C3:    minute >= natural__first .
C4:    minute <= natural__last .
C5:    hour >= natural__first .
C6:    hour <= natural__last .
C7:    10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C8:    10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C9:    month >= natural__first .
C10:   month <= natural__last .
C11:   year >= natural__first .
C12:   year <= natural__last .
 

procedure_converttimestring_33.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   loop__1__i <= 10 .
H21:   hour >= natural__first .
H22:   hour <= natural__last .
H23:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H24:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H25:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H26:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H27:   10 * hour >= integer__base__first .
H28:   10 * hour <= integer__base__last .
H29:   year >= natural__first .
H30:   year <= natural__last .
H31:   month >= natural__first .
H32:   month <= natural__last .
H33:   day >= natural__first .
H34:   day <= natural__last .
H35:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H36:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H37:   minute >= natural__first .
H38:   minute <= natural__last .
H39:   second >= natural__first .
H40:   second <= natural__last .
H41:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (10 * 
           hour + (element(timestring, [loop__1__i]) - 48) >= 
           hoursinaday)) or (minute >= minutesinanhour)) or (
           second >= secondsinaminute)) .
H42:   year >= natural__first .
H43:   year <= natural__last .
H44:   month >= natural__first .
H45:   month <= natural__last .
H46:   day >= natural__first .
H47:   day <= natural__last .
H48:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H49:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H50:   minute >= natural__first .
H51:   minute <= natural__last .
H52:   second >= natural__first .
H53:   second <= natural__last .
H54:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (10 * 
           hour + (element(timestring, [loop__1__i]) - 48) >= 
           hoursinaday)) or (minute >= minutesinanhour)) or (
           second >= secondsinaminute))) .
H55:   year >= natural__first .
H56:   year <= natural__last .
H57:   month >= natural__first .
H58:   month <= natural__last .
H59:   day >= natural__first .
H60:   day <= natural__last .
H61:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H62:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H63:   minute >= natural__first .
H64:   minute <= natural__last .
H65:   second >= natural__first .
H66:   second <= natural__last .
        ->
C1:    second >= natural__first .
C2:    second <= natural__last .
C3:    minute >= natural__first .
C4:    minute <= natural__last .
C5:    10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C6:    10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C7:    day >= natural__first .
C8:    day <= natural__last .
C9:    month >= natural__first .
C10:   month <= natural__last .
C11:   year >= natural__first .
C12:   year <= natural__last .
 

procedure_converttimestring_34.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   loop__1__i <= 12 .
H22:   minute >= natural__first .
H23:   minute <= natural__last .
H24:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H25:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H26:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H27:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H28:   10 * minute >= integer__base__first .
H29:   10 * minute <= integer__base__last .
H30:   year >= natural__first .
H31:   year <= natural__last .
H32:   month >= natural__first .
H33:   month <= natural__last .
H34:   day >= natural__first .
H35:   day <= natural__last .
H36:   hour >= natural__first .
H37:   hour <= natural__last .
H38:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H39:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H40:   second >= natural__first .
H41:   second <= natural__last .
H42:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (10 * minute + (element(
           timestring, [loop__1__i]) - 48) >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
H43:   year >= natural__first .
H44:   year <= natural__last .
H45:   month >= natural__first .
H46:   month <= natural__last .
H47:   day >= natural__first .
H48:   day <= natural__last .
H49:   hour >= natural__first .
H50:   hour <= natural__last .
H51:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H52:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H53:   second >= natural__first .
H54:   second <= natural__last .
H55:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (10 * minute + (element(
           timestring, [loop__1__i]) - 48) >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H56:   year >= natural__first .
H57:   year <= natural__last .
H58:   month >= natural__first .
H59:   month <= natural__last .
H60:   day >= natural__first .
H61:   day <= natural__last .
H62:   hour >= natural__first .
H63:   hour <= natural__last .
H64:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H65:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H66:   second >= natural__first .
H67:   second <= natural__last .
        ->
C1:    second >= natural__first .
C2:    second <= natural__last .
C3:    10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C4:    10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C5:    hour >= natural__first .
C6:    hour <= natural__last .
C7:    day >= natural__first .
C8:    day <= natural__last .
C9:    month >= natural__first .
C10:   month <= natural__last .
C11:   year >= natural__first .
C12:   year <= natural__last .
 

procedure_converttimestring_35.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   not (loop__1__i <= 12) .
H22:   loop__1__i <= 14 .
H23:   second >= natural__first .
H24:   second <= natural__last .
H25:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H26:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H27:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H28:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H29:   10 * second >= integer__base__first .
H30:   10 * second <= integer__base__last .
H31:   year >= natural__first .
H32:   year <= natural__last .
H33:   month >= natural__first .
H34:   month <= natural__last .
H35:   day >= natural__first .
H36:   day <= natural__last .
H37:   hour >= natural__first .
H38:   hour <= natural__last .
H39:   minute >= natural__first .
H40:   minute <= natural__last .
H41:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H42:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H43:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (10 * second + (element(
           timestring, [loop__1__i]) - 48) >= 
           secondsinaminute)) .
H44:   year >= natural__first .
H45:   year <= natural__last .
H46:   month >= natural__first .
H47:   month <= natural__last .
H48:   day >= natural__first .
H49:   day <= natural__last .
H50:   hour >= natural__first .
H51:   hour <= natural__last .
H52:   minute >= natural__first .
H53:   minute <= natural__last .
H54:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H55:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H56:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (10 * second + (element(
           timestring, [loop__1__i]) - 48) >= 
           secondsinaminute))) .
H57:   year >= natural__first .
H58:   year <= natural__last .
H59:   month >= natural__first .
H60:   month <= natural__last .
H61:   day >= natural__first .
H62:   day <= natural__last .
H63:   hour >= natural__first .
H64:   hour <= natural__last .
H65:   minute >= natural__first .
H66:   minute <= natural__last .
H67:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H68:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
        ->
C1:    10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C2:    10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C3:    minute >= natural__first .
C4:    minute <= natural__last .
C5:    hour >= natural__first .
C6:    hour <= natural__last .
C7:    day >= natural__first .
C8:    day <= natural__last .
C9:    month >= natural__first .
C10:   month <= natural__last .
C11:   year >= natural__first .
C12:   year <= natural__last .
 

procedure_converttimestring_36.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   not (loop__1__i <= 12) .
H22:   not (loop__1__i <= 14) .
H23:   year >= natural__first .
H24:   year <= natural__last .
H25:   month >= natural__first .
H26:   month <= natural__last .
H27:   day >= natural__first .
H28:   day <= natural__last .
H29:   hour >= natural__first .
H30:   hour <= natural__last .
H31:   minute >= natural__first .
H32:   minute <= natural__last .
H33:   second >= natural__first .
H34:   second <= natural__last .
H35:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
H36:   year >= natural__first .
H37:   year <= natural__last .
H38:   month >= natural__first .
H39:   month <= natural__last .
H40:   day >= natural__first .
H41:   day <= natural__last .
H42:   hour >= natural__first .
H43:   hour <= natural__last .
H44:   minute >= natural__first .
H45:   minute <= natural__last .
H46:   second >= natural__first .
H47:   second <= natural__last .
H48:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H49:   year >= natural__first .
H50:   year <= natural__last .
H51:   month >= natural__first .
H52:   month <= natural__last .
H53:   day >= natural__first .
H54:   day <= natural__last .
H55:   hour >= natural__first .
H56:   hour <= natural__last .
H57:   minute >= natural__first .
H58:   minute <= natural__last .
H59:   second >= natural__first .
H60:   second <= natural__last .
        ->
C1:    second >= natural__first .
C2:    second <= natural__last .
C3:    minute >= natural__first .
C4:    minute <= natural__last .
C5:    hour >= natural__first .
C6:    hour <= natural__last .
C7:    day >= natural__first .
C8:    day <= natural__last .
C9:    month >= natural__first .
C10:   month <= natural__last .
C11:   year >= natural__first .
C12:   year <= natural__last .
 

procedure_converttimestring_37.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   loop__1__i <= 4 .
H18:   year >= natural__first .
H19:   year <= natural__last .
H20:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H21:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H22:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H23:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H24:   10 * year >= integer__base__first .
H25:   10 * year <= integer__base__last .
H26:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H27:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H28:   month >= natural__first .
H29:   month <= natural__last .
H30:   day >= natural__first .
H31:   day <= natural__last .
H32:   hour >= natural__first .
H33:   hour <= natural__last .
H34:   minute >= natural__first .
H35:   minute <= natural__last .
H36:   second >= natural__first .
H37:   second <= natural__last .
H38:   not ((10 * year + (element(timestring, [loop__1__i]) - 48) > 
           rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H39:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H40:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H41:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H42:   month >= natural__first .
H43:   month <= natural__last .
H44:   day >= natural__first .
H45:   day <= natural__last .
H46:   hour >= natural__first .
H47:   hour <= natural__last .
H48:   minute >= natural__first .
H49:   minute <= natural__last .
H50:   second >= natural__first .
H51:   second <= natural__last .
H52:   not ((10 * year + (element(timestring, [loop__1__i]) - 48) > 
           rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H53:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H54:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H55:   month >= natural__first .
H56:   month <= natural__last .
H57:   day >= natural__first .
H58:   day <= natural__last .
H59:   hour >= natural__first .
H60:   hour <= natural__last .
H61:   minute >= natural__first .
H62:   minute <= natural__last .
H63:   second >= natural__first .
H64:   second <= natural__last .
        ->
C1:    second >= natural__first .
C2:    second <= natural__last .
C3:    minute >= natural__first .
C4:    minute <= natural__last .
C5:    hour >= natural__first .
C6:    hour <= natural__last .
C7:    day >= natural__first .
C8:    day <= natural__last .
C9:    month >= natural__first .
C10:   month <= natural__last .
C11:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C12:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
 

procedure_converttimestring_38.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   loop__1__i <= 6 .
H19:   month >= natural__first .
H20:   month <= natural__last .
H21:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H22:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H23:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H24:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H25:   10 * month >= integer__base__first .
H26:   10 * month <= integer__base__last .
H27:   year >= natural__first .
H28:   year <= natural__last .
H29:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H30:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H31:   day >= natural__first .
H32:   day <= natural__last .
H33:   hour >= natural__first .
H34:   hour <= natural__last .
H35:   minute >= natural__first .
H36:   minute <= natural__last .
H37:   second >= natural__first .
H38:   second <= natural__last .
H39:   not ((year > rr_type__rrsig_record_type__max_year) or (((((10 * 
           month + (element(timestring, [loop__1__i]) - 48) > 
           monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H40:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H41:   year >= natural__first .
H42:   year <= natural__last .
H43:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H44:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H45:   day >= natural__first .
H46:   day <= natural__last .
H47:   hour >= natural__first .
H48:   hour <= natural__last .
H49:   minute >= natural__first .
H50:   minute <= natural__last .
H51:   second >= natural__first .
H52:   second <= natural__last .
H53:   not ((year > rr_type__rrsig_record_type__max_year) or (((((10 * 
           month + (element(timestring, [loop__1__i]) - 48) > 
           monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H54:   year >= natural__first .
H55:   year <= natural__last .
H56:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H57:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H58:   day >= natural__first .
H59:   day <= natural__last .
H60:   hour >= natural__first .
H61:   hour <= natural__last .
H62:   minute >= natural__first .
H63:   minute <= natural__last .
H64:   second >= natural__first .
H65:   second <= natural__last .
        ->
C1:    second >= natural__first .
C2:    second <= natural__last .
C3:    minute >= natural__first .
C4:    minute <= natural__last .
C5:    hour >= natural__first .
C6:    hour <= natural__last .
C7:    day >= natural__first .
C8:    day <= natural__last .
C9:    10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C10:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C11:   year >= natural__first .
C12:   year <= natural__last .
 

procedure_converttimestring_39.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   loop__1__i <= 8 .
H20:   day >= natural__first .
H21:   day <= natural__last .
H22:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H23:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H24:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H25:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H26:   10 * day >= integer__base__first .
H27:   10 * day <= integer__base__last .
H28:   year >= natural__first .
H29:   year <= natural__last .
H30:   month >= natural__first .
H31:   month <= natural__last .
H32:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H33:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H34:   hour >= natural__first .
H35:   hour <= natural__last .
H36:   minute >= natural__first .
H37:   minute <= natural__last .
H38:   second >= natural__first .
H39:   second <= natural__last .
H40:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (10 * day + (element(
           timestring, [loop__1__i]) - 48) > 
           maxdaysinamonth)) or (hour >= hoursinaday)) or (
           minute >= minutesinanhour)) or (second >= 
           secondsinaminute))) .
H41:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H42:   year >= natural__first .
H43:   year <= natural__last .
H44:   month >= natural__first .
H45:   month <= natural__last .
H46:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H47:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H48:   hour >= natural__first .
H49:   hour <= natural__last .
H50:   minute >= natural__first .
H51:   minute <= natural__last .
H52:   second >= natural__first .
H53:   second <= natural__last .
H54:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (10 * day + (element(
           timestring, [loop__1__i]) - 48) > 
           maxdaysinamonth)) or (hour >= hoursinaday)) or (
           minute >= minutesinanhour)) or (second >= 
           secondsinaminute))) .
H55:   year >= natural__first .
H56:   year <= natural__last .
H57:   month >= natural__first .
H58:   month <= natural__last .
H59:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H60:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H61:   hour >= natural__first .
H62:   hour <= natural__last .
H63:   minute >= natural__first .
H64:   minute <= natural__last .
H65:   second >= natural__first .
H66:   second <= natural__last .
        ->
C1:    second >= natural__first .
C2:    second <= natural__last .
C3:    minute >= natural__first .
C4:    minute <= natural__last .
C5:    hour >= natural__first .
C6:    hour <= natural__last .
C7:    10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C8:    10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C9:    month >= natural__first .
C10:   month <= natural__last .
C11:   year >= natural__first .
C12:   year <= natural__last .
 

procedure_converttimestring_40.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   loop__1__i <= 10 .
H21:   hour >= natural__first .
H22:   hour <= natural__last .
H23:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H24:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H25:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H26:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H27:   10 * hour >= integer__base__first .
H28:   10 * hour <= integer__base__last .
H29:   year >= natural__first .
H30:   year <= natural__last .
H31:   month >= natural__first .
H32:   month <= natural__last .
H33:   day >= natural__first .
H34:   day <= natural__last .
H35:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H36:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H37:   minute >= natural__first .
H38:   minute <= natural__last .
H39:   second >= natural__first .
H40:   second <= natural__last .
H41:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (10 * 
           hour + (element(timestring, [loop__1__i]) - 48) >= 
           hoursinaday)) or (minute >= minutesinanhour)) or (
           second >= secondsinaminute))) .
H42:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H43:   year >= natural__first .
H44:   year <= natural__last .
H45:   month >= natural__first .
H46:   month <= natural__last .
H47:   day >= natural__first .
H48:   day <= natural__last .
H49:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H50:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H51:   minute >= natural__first .
H52:   minute <= natural__last .
H53:   second >= natural__first .
H54:   second <= natural__last .
H55:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (10 * 
           hour + (element(timestring, [loop__1__i]) - 48) >= 
           hoursinaday)) or (minute >= minutesinanhour)) or (
           second >= secondsinaminute))) .
H56:   year >= natural__first .
H57:   year <= natural__last .
H58:   month >= natural__first .
H59:   month <= natural__last .
H60:   day >= natural__first .
H61:   day <= natural__last .
H62:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H63:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H64:   minute >= natural__first .
H65:   minute <= natural__last .
H66:   second >= natural__first .
H67:   second <= natural__last .
        ->
C1:    second >= natural__first .
C2:    second <= natural__last .
C3:    minute >= natural__first .
C4:    minute <= natural__last .
C5:    10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C6:    10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C7:    day >= natural__first .
C8:    day <= natural__last .
C9:    month >= natural__first .
C10:   month <= natural__last .
C11:   year >= natural__first .
C12:   year <= natural__last .
 

procedure_converttimestring_41.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   loop__1__i <= 12 .
H22:   minute >= natural__first .
H23:   minute <= natural__last .
H24:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H25:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H26:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H27:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H28:   10 * minute >= integer__base__first .
H29:   10 * minute <= integer__base__last .
H30:   year >= natural__first .
H31:   year <= natural__last .
H32:   month >= natural__first .
H33:   month <= natural__last .
H34:   day >= natural__first .
H35:   day <= natural__last .
H36:   hour >= natural__first .
H37:   hour <= natural__last .
H38:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H39:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H40:   second >= natural__first .
H41:   second <= natural__last .
H42:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (10 * minute + (element(
           timestring, [loop__1__i]) - 48) >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H43:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H44:   year >= natural__first .
H45:   year <= natural__last .
H46:   month >= natural__first .
H47:   month <= natural__last .
H48:   day >= natural__first .
H49:   day <= natural__last .
H50:   hour >= natural__first .
H51:   hour <= natural__last .
H52:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H53:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H54:   second >= natural__first .
H55:   second <= natural__last .
H56:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (10 * minute + (element(
           timestring, [loop__1__i]) - 48) >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H57:   year >= natural__first .
H58:   year <= natural__last .
H59:   month >= natural__first .
H60:   month <= natural__last .
H61:   day >= natural__first .
H62:   day <= natural__last .
H63:   hour >= natural__first .
H64:   hour <= natural__last .
H65:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H66:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H67:   second >= natural__first .
H68:   second <= natural__last .
        ->
C1:    second >= natural__first .
C2:    second <= natural__last .
C3:    10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C4:    10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C5:    hour >= natural__first .
C6:    hour <= natural__last .
C7:    day >= natural__first .
C8:    day <= natural__last .
C9:    month >= natural__first .
C10:   month <= natural__last .
C11:   year >= natural__first .
C12:   year <= natural__last .
 

procedure_converttimestring_42.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   not (loop__1__i <= 12) .
H22:   loop__1__i <= 14 .
H23:   second >= natural__first .
H24:   second <= natural__last .
H25:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H26:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H27:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H28:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H29:   10 * second >= integer__base__first .
H30:   10 * second <= integer__base__last .
H31:   year >= natural__first .
H32:   year <= natural__last .
H33:   month >= natural__first .
H34:   month <= natural__last .
H35:   day >= natural__first .
H36:   day <= natural__last .
H37:   hour >= natural__first .
H38:   hour <= natural__last .
H39:   minute >= natural__first .
H40:   minute <= natural__last .
H41:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H42:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H43:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (10 * second + (element(
           timestring, [loop__1__i]) - 48) >= 
           secondsinaminute))) .
H44:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H45:   year >= natural__first .
H46:   year <= natural__last .
H47:   month >= natural__first .
H48:   month <= natural__last .
H49:   day >= natural__first .
H50:   day <= natural__last .
H51:   hour >= natural__first .
H52:   hour <= natural__last .
H53:   minute >= natural__first .
H54:   minute <= natural__last .
H55:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H56:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H57:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (10 * second + (element(
           timestring, [loop__1__i]) - 48) >= 
           secondsinaminute))) .
H58:   year >= natural__first .
H59:   year <= natural__last .
H60:   month >= natural__first .
H61:   month <= natural__last .
H62:   day >= natural__first .
H63:   day <= natural__last .
H64:   hour >= natural__first .
H65:   hour <= natural__last .
H66:   minute >= natural__first .
H67:   minute <= natural__last .
H68:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H69:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
        ->
C1:    10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
C2:    10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
C3:    minute >= natural__first .
C4:    minute <= natural__last .
C5:    hour >= natural__first .
C6:    hour <= natural__last .
C7:    day >= natural__first .
C8:    day <= natural__last .
C9:    month >= natural__first .
C10:   month <= natural__last .
C11:   year >= natural__first .
C12:   year <= natural__last .
 

procedure_converttimestring_43.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   not (loop__1__i <= 12) .
H22:   not (loop__1__i <= 14) .
H23:   year >= natural__first .
H24:   year <= natural__last .
H25:   month >= natural__first .
H26:   month <= natural__last .
H27:   day >= natural__first .
H28:   day <= natural__last .
H29:   hour >= natural__first .
H30:   hour <= natural__last .
H31:   minute >= natural__first .
H32:   minute <= natural__last .
H33:   second >= natural__first .
H34:   second <= natural__last .
H35:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H36:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H37:   year >= natural__first .
H38:   year <= natural__last .
H39:   month >= natural__first .
H40:   month <= natural__last .
H41:   day >= natural__first .
H42:   day <= natural__last .
H43:   hour >= natural__first .
H44:   hour <= natural__last .
H45:   minute >= natural__first .
H46:   minute <= natural__last .
H47:   second >= natural__first .
H48:   second <= natural__last .
H49:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H50:   year >= natural__first .
H51:   year <= natural__last .
H52:   month >= natural__first .
H53:   month <= natural__last .
H54:   day >= natural__first .
H55:   day <= natural__last .
H56:   hour >= natural__first .
H57:   hour <= natural__last .
H58:   minute >= natural__first .
H59:   minute <= natural__last .
H60:   second >= natural__first .
H61:   second <= natural__last .
        ->
C1:    second >= natural__first .
C2:    second <= natural__last .
C3:    minute >= natural__first .
C4:    minute <= natural__last .
C5:    hour >= natural__first .
C6:    hour <= natural__last .
C7:    day >= natural__first .
C8:    day <= natural__last .
C9:    month >= natural__first .
C10:   month <= natural__last .
C11:   year >= natural__first .
C12:   year <= natural__last .
 

For path(s) from assertion of line 693 to run-time check associated with statement of line 719:

procedure_converttimestring_44.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   loop__1__i <= 4 .
H18:   year >= natural__first .
H19:   year <= natural__last .
H20:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H21:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H22:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H23:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H24:   10 * year >= integer__base__first .
H25:   10 * year <= integer__base__last .
H26:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H27:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H28:   month >= natural__first .
H29:   month <= natural__last .
H30:   day >= natural__first .
H31:   day <= natural__last .
H32:   hour >= natural__first .
H33:   hour <= natural__last .
H34:   minute >= natural__first .
H35:   minute <= natural__last .
H36:   second >= natural__first .
H37:   second <= natural__last .
H38:   (10 * year + (element(timestring, [loop__1__i]) - 48) > 
           rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
H39:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H40:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H41:   month >= natural__first .
H42:   month <= natural__last .
H43:   day >= natural__first .
H44:   day <= natural__last .
H45:   hour >= natural__first .
H46:   hour <= natural__last .
H47:   minute >= natural__first .
H48:   minute <= natural__last .
H49:   second >= natural__first .
H50:   second <= natural__last .
H51:   not ((10 * year + (element(timestring, [loop__1__i]) - 48) > 
           rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H52:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H53:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H54:   month >= natural__first .
H55:   month <= natural__last .
H56:   day >= natural__first .
H57:   day <= natural__last .
H58:   hour >= natural__first .
H59:   hour <= natural__last .
H60:   minute >= natural__first .
H61:   minute <= natural__last .
H62:   second >= natural__first .
H63:   second <= natural__last .
H64:   second >= natural__first .
H65:   second <= natural__last .
H66:   minute >= natural__first .
H67:   minute <= natural__last .
H68:   hour >= natural__first .
H69:   hour <= natural__last .
H70:   day >= natural__first .
H71:   day <= natural__last .
H72:   month >= natural__first .
H73:   month <= natural__last .
H74:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H75:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H76:   non_spark_stuff__time_of(10 * year + (element(
           timestring, [loop__1__i]) - 48), month, day, 
           hour, minute, second) >= 
           unsigned_types__unsigned32__first .
H77:   non_spark_stuff__time_of(10 * year + (element(
           timestring, [loop__1__i]) - 48), month, day, 
           hour, minute, second) <= 
           unsigned_types__unsigned32__last .
        ->
C1:    non_spark_stuff__time_of(10 * year + (element(
           timestring, [loop__1__i]) - 48), month, day, 
           hour, minute, second) >= 
           unsigned_types__unsigned32__first .
C2:    non_spark_stuff__time_of(10 * year + (element(
           timestring, [loop__1__i]) - 48), month, day, 
           hour, minute, second) <= 
           unsigned_types__unsigned32__last .
 

procedure_converttimestring_45.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   loop__1__i <= 6 .
H19:   month >= natural__first .
H20:   month <= natural__last .
H21:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H22:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H23:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H24:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H25:   10 * month >= integer__base__first .
H26:   10 * month <= integer__base__last .
H27:   year >= natural__first .
H28:   year <= natural__last .
H29:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H30:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H31:   day >= natural__first .
H32:   day <= natural__last .
H33:   hour >= natural__first .
H34:   hour <= natural__last .
H35:   minute >= natural__first .
H36:   minute <= natural__last .
H37:   second >= natural__first .
H38:   second <= natural__last .
H39:   (year > rr_type__rrsig_record_type__max_year) or (((((10 * 
           month + (element(timestring, [loop__1__i]) - 48) > 
           monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
H40:   year >= natural__first .
H41:   year <= natural__last .
H42:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H43:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H44:   day >= natural__first .
H45:   day <= natural__last .
H46:   hour >= natural__first .
H47:   hour <= natural__last .
H48:   minute >= natural__first .
H49:   minute <= natural__last .
H50:   second >= natural__first .
H51:   second <= natural__last .
H52:   not ((year > rr_type__rrsig_record_type__max_year) or (((((10 * 
           month + (element(timestring, [loop__1__i]) - 48) > 
           monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H53:   year >= natural__first .
H54:   year <= natural__last .
H55:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H56:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H57:   day >= natural__first .
H58:   day <= natural__last .
H59:   hour >= natural__first .
H60:   hour <= natural__last .
H61:   minute >= natural__first .
H62:   minute <= natural__last .
H63:   second >= natural__first .
H64:   second <= natural__last .
H65:   second >= natural__first .
H66:   second <= natural__last .
H67:   minute >= natural__first .
H68:   minute <= natural__last .
H69:   hour >= natural__first .
H70:   hour <= natural__last .
H71:   day >= natural__first .
H72:   day <= natural__last .
H73:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H74:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H75:   year >= natural__first .
H76:   year <= natural__last .
H77:   non_spark_stuff__time_of(year, 10 * month + (element(
           timestring, [loop__1__i]) - 48), day, hour, 
           minute, second) >= unsigned_types__unsigned32__first .
H78:   non_spark_stuff__time_of(year, 10 * month + (element(
           timestring, [loop__1__i]) - 48), day, hour, 
           minute, second) <= unsigned_types__unsigned32__last .
        ->
C1:    non_spark_stuff__time_of(year, 10 * month + (element(
           timestring, [loop__1__i]) - 48), day, hour, 
           minute, second) >= unsigned_types__unsigned32__first .
C2:    non_spark_stuff__time_of(year, 10 * month + (element(
           timestring, [loop__1__i]) - 48), day, hour, 
           minute, second) <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_46.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   loop__1__i <= 8 .
H20:   day >= natural__first .
H21:   day <= natural__last .
H22:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H23:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H24:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H25:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H26:   10 * day >= integer__base__first .
H27:   10 * day <= integer__base__last .
H28:   year >= natural__first .
H29:   year <= natural__last .
H30:   month >= natural__first .
H31:   month <= natural__last .
H32:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H33:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H34:   hour >= natural__first .
H35:   hour <= natural__last .
H36:   minute >= natural__first .
H37:   minute <= natural__last .
H38:   second >= natural__first .
H39:   second <= natural__last .
H40:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (10 * day + (element(
           timestring, [loop__1__i]) - 48) > 
           maxdaysinamonth)) or (hour >= hoursinaday)) or (
           minute >= minutesinanhour)) or (second >= 
           secondsinaminute)) .
H41:   year >= natural__first .
H42:   year <= natural__last .
H43:   month >= natural__first .
H44:   month <= natural__last .
H45:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H46:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H47:   hour >= natural__first .
H48:   hour <= natural__last .
H49:   minute >= natural__first .
H50:   minute <= natural__last .
H51:   second >= natural__first .
H52:   second <= natural__last .
H53:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (10 * day + (element(
           timestring, [loop__1__i]) - 48) > 
           maxdaysinamonth)) or (hour >= hoursinaday)) or (
           minute >= minutesinanhour)) or (second >= 
           secondsinaminute))) .
H54:   year >= natural__first .
H55:   year <= natural__last .
H56:   month >= natural__first .
H57:   month <= natural__last .
H58:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H59:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H60:   hour >= natural__first .
H61:   hour <= natural__last .
H62:   minute >= natural__first .
H63:   minute <= natural__last .
H64:   second >= natural__first .
H65:   second <= natural__last .
H66:   second >= natural__first .
H67:   second <= natural__last .
H68:   minute >= natural__first .
H69:   minute <= natural__last .
H70:   hour >= natural__first .
H71:   hour <= natural__last .
H72:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H73:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H74:   month >= natural__first .
H75:   month <= natural__last .
H76:   year >= natural__first .
H77:   year <= natural__last .
H78:   non_spark_stuff__time_of(year, month, 10 * day + (element(
           timestring, [loop__1__i]) - 48), hour, minute, 
           second) >= unsigned_types__unsigned32__first .
H79:   non_spark_stuff__time_of(year, month, 10 * day + (element(
           timestring, [loop__1__i]) - 48), hour, minute, 
           second) <= unsigned_types__unsigned32__last .
        ->
C1:    non_spark_stuff__time_of(year, month, 10 * day + (element(
           timestring, [loop__1__i]) - 48), hour, minute, 
           second) >= unsigned_types__unsigned32__first .
C2:    non_spark_stuff__time_of(year, month, 10 * day + (element(
           timestring, [loop__1__i]) - 48), hour, minute, 
           second) <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_47.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   loop__1__i <= 10 .
H21:   hour >= natural__first .
H22:   hour <= natural__last .
H23:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H24:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H25:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H26:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H27:   10 * hour >= integer__base__first .
H28:   10 * hour <= integer__base__last .
H29:   year >= natural__first .
H30:   year <= natural__last .
H31:   month >= natural__first .
H32:   month <= natural__last .
H33:   day >= natural__first .
H34:   day <= natural__last .
H35:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H36:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H37:   minute >= natural__first .
H38:   minute <= natural__last .
H39:   second >= natural__first .
H40:   second <= natural__last .
H41:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (10 * 
           hour + (element(timestring, [loop__1__i]) - 48) >= 
           hoursinaday)) or (minute >= minutesinanhour)) or (
           second >= secondsinaminute)) .
H42:   year >= natural__first .
H43:   year <= natural__last .
H44:   month >= natural__first .
H45:   month <= natural__last .
H46:   day >= natural__first .
H47:   day <= natural__last .
H48:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H49:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H50:   minute >= natural__first .
H51:   minute <= natural__last .
H52:   second >= natural__first .
H53:   second <= natural__last .
H54:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (10 * 
           hour + (element(timestring, [loop__1__i]) - 48) >= 
           hoursinaday)) or (minute >= minutesinanhour)) or (
           second >= secondsinaminute))) .
H55:   year >= natural__first .
H56:   year <= natural__last .
H57:   month >= natural__first .
H58:   month <= natural__last .
H59:   day >= natural__first .
H60:   day <= natural__last .
H61:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H62:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H63:   minute >= natural__first .
H64:   minute <= natural__last .
H65:   second >= natural__first .
H66:   second <= natural__last .
H67:   second >= natural__first .
H68:   second <= natural__last .
H69:   minute >= natural__first .
H70:   minute <= natural__last .
H71:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H72:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H73:   day >= natural__first .
H74:   day <= natural__last .
H75:   month >= natural__first .
H76:   month <= natural__last .
H77:   year >= natural__first .
H78:   year <= natural__last .
H79:   non_spark_stuff__time_of(year, month, day, 10 * hour + (element(
           timestring, [loop__1__i]) - 48), minute, second) >= 
           unsigned_types__unsigned32__first .
H80:   non_spark_stuff__time_of(year, month, day, 10 * hour + (element(
           timestring, [loop__1__i]) - 48), minute, second) <= 
           unsigned_types__unsigned32__last .
        ->
C1:    non_spark_stuff__time_of(year, month, day, 10 * hour + (element(
           timestring, [loop__1__i]) - 48), minute, second) >= 
           unsigned_types__unsigned32__first .
C2:    non_spark_stuff__time_of(year, month, day, 10 * hour + (element(
           timestring, [loop__1__i]) - 48), minute, second) <= 
           unsigned_types__unsigned32__last .
 

procedure_converttimestring_48.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   loop__1__i <= 12 .
H22:   minute >= natural__first .
H23:   minute <= natural__last .
H24:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H25:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H26:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H27:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H28:   10 * minute >= integer__base__first .
H29:   10 * minute <= integer__base__last .
H30:   year >= natural__first .
H31:   year <= natural__last .
H32:   month >= natural__first .
H33:   month <= natural__last .
H34:   day >= natural__first .
H35:   day <= natural__last .
H36:   hour >= natural__first .
H37:   hour <= natural__last .
H38:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H39:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H40:   second >= natural__first .
H41:   second <= natural__last .
H42:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (10 * minute + (element(
           timestring, [loop__1__i]) - 48) >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
H43:   year >= natural__first .
H44:   year <= natural__last .
H45:   month >= natural__first .
H46:   month <= natural__last .
H47:   day >= natural__first .
H48:   day <= natural__last .
H49:   hour >= natural__first .
H50:   hour <= natural__last .
H51:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H52:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H53:   second >= natural__first .
H54:   second <= natural__last .
H55:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (10 * minute + (element(
           timestring, [loop__1__i]) - 48) >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H56:   year >= natural__first .
H57:   year <= natural__last .
H58:   month >= natural__first .
H59:   month <= natural__last .
H60:   day >= natural__first .
H61:   day <= natural__last .
H62:   hour >= natural__first .
H63:   hour <= natural__last .
H64:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H65:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H66:   second >= natural__first .
H67:   second <= natural__last .
H68:   second >= natural__first .
H69:   second <= natural__last .
H70:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H71:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H72:   hour >= natural__first .
H73:   hour <= natural__last .
H74:   day >= natural__first .
H75:   day <= natural__last .
H76:   month >= natural__first .
H77:   month <= natural__last .
H78:   year >= natural__first .
H79:   year <= natural__last .
H80:   non_spark_stuff__time_of(year, month, day, hour, 10 * 
           minute + (element(timestring, [loop__1__i]) - 48), 
           second) >= unsigned_types__unsigned32__first .
H81:   non_spark_stuff__time_of(year, month, day, hour, 10 * 
           minute + (element(timestring, [loop__1__i]) - 48), 
           second) <= unsigned_types__unsigned32__last .
        ->
C1:    non_spark_stuff__time_of(year, month, day, hour, 10 * 
           minute + (element(timestring, [loop__1__i]) - 48), 
           second) >= unsigned_types__unsigned32__first .
C2:    non_spark_stuff__time_of(year, month, day, hour, 10 * 
           minute + (element(timestring, [loop__1__i]) - 48), 
           second) <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_49.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   not (loop__1__i <= 12) .
H22:   loop__1__i <= 14 .
H23:   second >= natural__first .
H24:   second <= natural__last .
H25:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H26:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H27:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H28:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H29:   10 * second >= integer__base__first .
H30:   10 * second <= integer__base__last .
H31:   year >= natural__first .
H32:   year <= natural__last .
H33:   month >= natural__first .
H34:   month <= natural__last .
H35:   day >= natural__first .
H36:   day <= natural__last .
H37:   hour >= natural__first .
H38:   hour <= natural__last .
H39:   minute >= natural__first .
H40:   minute <= natural__last .
H41:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H42:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H43:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (10 * second + (element(
           timestring, [loop__1__i]) - 48) >= 
           secondsinaminute)) .
H44:   year >= natural__first .
H45:   year <= natural__last .
H46:   month >= natural__first .
H47:   month <= natural__last .
H48:   day >= natural__first .
H49:   day <= natural__last .
H50:   hour >= natural__first .
H51:   hour <= natural__last .
H52:   minute >= natural__first .
H53:   minute <= natural__last .
H54:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H55:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H56:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (10 * second + (element(
           timestring, [loop__1__i]) - 48) >= 
           secondsinaminute))) .
H57:   year >= natural__first .
H58:   year <= natural__last .
H59:   month >= natural__first .
H60:   month <= natural__last .
H61:   day >= natural__first .
H62:   day <= natural__last .
H63:   hour >= natural__first .
H64:   hour <= natural__last .
H65:   minute >= natural__first .
H66:   minute <= natural__last .
H67:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H68:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H69:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H70:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H71:   minute >= natural__first .
H72:   minute <= natural__last .
H73:   hour >= natural__first .
H74:   hour <= natural__last .
H75:   day >= natural__first .
H76:   day <= natural__last .
H77:   month >= natural__first .
H78:   month <= natural__last .
H79:   year >= natural__first .
H80:   year <= natural__last .
H81:   non_spark_stuff__time_of(year, month, day, hour, 
           minute, 10 * second + (element(timestring, [
           loop__1__i]) - 48)) >= unsigned_types__unsigned32__first .
H82:   non_spark_stuff__time_of(year, month, day, hour, 
           minute, 10 * second + (element(timestring, [
           loop__1__i]) - 48)) <= unsigned_types__unsigned32__last .
        ->
C1:    non_spark_stuff__time_of(year, month, day, hour, 
           minute, 10 * second + (element(timestring, [
           loop__1__i]) - 48)) >= unsigned_types__unsigned32__first .
C2:    non_spark_stuff__time_of(year, month, day, hour, 
           minute, 10 * second + (element(timestring, [
           loop__1__i]) - 48)) <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_50.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   not (loop__1__i <= 12) .
H22:   not (loop__1__i <= 14) .
H23:   year >= natural__first .
H24:   year <= natural__last .
H25:   month >= natural__first .
H26:   month <= natural__last .
H27:   day >= natural__first .
H28:   day <= natural__last .
H29:   hour >= natural__first .
H30:   hour <= natural__last .
H31:   minute >= natural__first .
H32:   minute <= natural__last .
H33:   second >= natural__first .
H34:   second <= natural__last .
H35:   (year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute)) .
H36:   year >= natural__first .
H37:   year <= natural__last .
H38:   month >= natural__first .
H39:   month <= natural__last .
H40:   day >= natural__first .
H41:   day <= natural__last .
H42:   hour >= natural__first .
H43:   hour <= natural__last .
H44:   minute >= natural__first .
H45:   minute <= natural__last .
H46:   second >= natural__first .
H47:   second <= natural__last .
H48:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H49:   year >= natural__first .
H50:   year <= natural__last .
H51:   month >= natural__first .
H52:   month <= natural__last .
H53:   day >= natural__first .
H54:   day <= natural__last .
H55:   hour >= natural__first .
H56:   hour <= natural__last .
H57:   minute >= natural__first .
H58:   minute <= natural__last .
H59:   second >= natural__first .
H60:   second <= natural__last .
H61:   second >= natural__first .
H62:   second <= natural__last .
H63:   minute >= natural__first .
H64:   minute <= natural__last .
H65:   hour >= natural__first .
H66:   hour <= natural__last .
H67:   day >= natural__first .
H68:   day <= natural__last .
H69:   month >= natural__first .
H70:   month <= natural__last .
H71:   year >= natural__first .
H72:   year <= natural__last .
H73:   non_spark_stuff__time_of(year, month, day, hour, 
           minute, second) >= unsigned_types__unsigned32__first .
H74:   non_spark_stuff__time_of(year, month, day, hour, 
           minute, second) <= unsigned_types__unsigned32__last .
        ->
C1:    non_spark_stuff__time_of(year, month, day, hour, 
           minute, second) >= unsigned_types__unsigned32__first .
C2:    non_spark_stuff__time_of(year, month, day, hour, 
           minute, second) <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_51.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   loop__1__i <= 4 .
H18:   year >= natural__first .
H19:   year <= natural__last .
H20:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H21:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H22:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H23:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H24:   10 * year >= integer__base__first .
H25:   10 * year <= integer__base__last .
H26:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H27:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H28:   month >= natural__first .
H29:   month <= natural__last .
H30:   day >= natural__first .
H31:   day <= natural__last .
H32:   hour >= natural__first .
H33:   hour <= natural__last .
H34:   minute >= natural__first .
H35:   minute <= natural__last .
H36:   second >= natural__first .
H37:   second <= natural__last .
H38:   not ((10 * year + (element(timestring, [loop__1__i]) - 48) > 
           rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H39:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H40:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H41:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H42:   month >= natural__first .
H43:   month <= natural__last .
H44:   day >= natural__first .
H45:   day <= natural__last .
H46:   hour >= natural__first .
H47:   hour <= natural__last .
H48:   minute >= natural__first .
H49:   minute <= natural__last .
H50:   second >= natural__first .
H51:   second <= natural__last .
H52:   not ((10 * year + (element(timestring, [loop__1__i]) - 48) > 
           rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H53:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H54:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H55:   month >= natural__first .
H56:   month <= natural__last .
H57:   day >= natural__first .
H58:   day <= natural__last .
H59:   hour >= natural__first .
H60:   hour <= natural__last .
H61:   minute >= natural__first .
H62:   minute <= natural__last .
H63:   second >= natural__first .
H64:   second <= natural__last .
H65:   second >= natural__first .
H66:   second <= natural__last .
H67:   minute >= natural__first .
H68:   minute <= natural__last .
H69:   hour >= natural__first .
H70:   hour <= natural__last .
H71:   day >= natural__first .
H72:   day <= natural__last .
H73:   month >= natural__first .
H74:   month <= natural__last .
H75:   10 * year + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H76:   10 * year + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H77:   non_spark_stuff__time_of(10 * year + (element(
           timestring, [loop__1__i]) - 48), month, day, 
           hour, minute, second) >= 
           unsigned_types__unsigned32__first .
H78:   non_spark_stuff__time_of(10 * year + (element(
           timestring, [loop__1__i]) - 48), month, day, 
           hour, minute, second) <= 
           unsigned_types__unsigned32__last .
        ->
C1:    non_spark_stuff__time_of(10 * year + (element(
           timestring, [loop__1__i]) - 48), month, day, 
           hour, minute, second) >= 
           unsigned_types__unsigned32__first .
C2:    non_spark_stuff__time_of(10 * year + (element(
           timestring, [loop__1__i]) - 48), month, day, 
           hour, minute, second) <= 
           unsigned_types__unsigned32__last .
 

procedure_converttimestring_52.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   loop__1__i <= 6 .
H19:   month >= natural__first .
H20:   month <= natural__last .
H21:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H22:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H23:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H24:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H25:   10 * month >= integer__base__first .
H26:   10 * month <= integer__base__last .
H27:   year >= natural__first .
H28:   year <= natural__last .
H29:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H30:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H31:   day >= natural__first .
H32:   day <= natural__last .
H33:   hour >= natural__first .
H34:   hour <= natural__last .
H35:   minute >= natural__first .
H36:   minute <= natural__last .
H37:   second >= natural__first .
H38:   second <= natural__last .
H39:   not ((year > rr_type__rrsig_record_type__max_year) or (((((10 * 
           month + (element(timestring, [loop__1__i]) - 48) > 
           monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H40:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H41:   year >= natural__first .
H42:   year <= natural__last .
H43:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H44:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H45:   day >= natural__first .
H46:   day <= natural__last .
H47:   hour >= natural__first .
H48:   hour <= natural__last .
H49:   minute >= natural__first .
H50:   minute <= natural__last .
H51:   second >= natural__first .
H52:   second <= natural__last .
H53:   not ((year > rr_type__rrsig_record_type__max_year) or (((((10 * 
           month + (element(timestring, [loop__1__i]) - 48) > 
           monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H54:   year >= natural__first .
H55:   year <= natural__last .
H56:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H57:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H58:   day >= natural__first .
H59:   day <= natural__last .
H60:   hour >= natural__first .
H61:   hour <= natural__last .
H62:   minute >= natural__first .
H63:   minute <= natural__last .
H64:   second >= natural__first .
H65:   second <= natural__last .
H66:   second >= natural__first .
H67:   second <= natural__last .
H68:   minute >= natural__first .
H69:   minute <= natural__last .
H70:   hour >= natural__first .
H71:   hour <= natural__last .
H72:   day >= natural__first .
H73:   day <= natural__last .
H74:   10 * month + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H75:   10 * month + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H76:   year >= natural__first .
H77:   year <= natural__last .
H78:   non_spark_stuff__time_of(year, 10 * month + (element(
           timestring, [loop__1__i]) - 48), day, hour, 
           minute, second) >= unsigned_types__unsigned32__first .
H79:   non_spark_stuff__time_of(year, 10 * month + (element(
           timestring, [loop__1__i]) - 48), day, hour, 
           minute, second) <= unsigned_types__unsigned32__last .
        ->
C1:    non_spark_stuff__time_of(year, 10 * month + (element(
           timestring, [loop__1__i]) - 48), day, hour, 
           minute, second) >= unsigned_types__unsigned32__first .
C2:    non_spark_stuff__time_of(year, 10 * month + (element(
           timestring, [loop__1__i]) - 48), day, hour, 
           minute, second) <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_53.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   loop__1__i <= 8 .
H20:   day >= natural__first .
H21:   day <= natural__last .
H22:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H23:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H24:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H25:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H26:   10 * day >= integer__base__first .
H27:   10 * day <= integer__base__last .
H28:   year >= natural__first .
H29:   year <= natural__last .
H30:   month >= natural__first .
H31:   month <= natural__last .
H32:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H33:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H34:   hour >= natural__first .
H35:   hour <= natural__last .
H36:   minute >= natural__first .
H37:   minute <= natural__last .
H38:   second >= natural__first .
H39:   second <= natural__last .
H40:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (10 * day + (element(
           timestring, [loop__1__i]) - 48) > 
           maxdaysinamonth)) or (hour >= hoursinaday)) or (
           minute >= minutesinanhour)) or (second >= 
           secondsinaminute))) .
H41:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H42:   year >= natural__first .
H43:   year <= natural__last .
H44:   month >= natural__first .
H45:   month <= natural__last .
H46:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H47:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H48:   hour >= natural__first .
H49:   hour <= natural__last .
H50:   minute >= natural__first .
H51:   minute <= natural__last .
H52:   second >= natural__first .
H53:   second <= natural__last .
H54:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (10 * day + (element(
           timestring, [loop__1__i]) - 48) > 
           maxdaysinamonth)) or (hour >= hoursinaday)) or (
           minute >= minutesinanhour)) or (second >= 
           secondsinaminute))) .
H55:   year >= natural__first .
H56:   year <= natural__last .
H57:   month >= natural__first .
H58:   month <= natural__last .
H59:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H60:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H61:   hour >= natural__first .
H62:   hour <= natural__last .
H63:   minute >= natural__first .
H64:   minute <= natural__last .
H65:   second >= natural__first .
H66:   second <= natural__last .
H67:   second >= natural__first .
H68:   second <= natural__last .
H69:   minute >= natural__first .
H70:   minute <= natural__last .
H71:   hour >= natural__first .
H72:   hour <= natural__last .
H73:   10 * day + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H74:   10 * day + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H75:   month >= natural__first .
H76:   month <= natural__last .
H77:   year >= natural__first .
H78:   year <= natural__last .
H79:   non_spark_stuff__time_of(year, month, 10 * day + (element(
           timestring, [loop__1__i]) - 48), hour, minute, 
           second) >= unsigned_types__unsigned32__first .
H80:   non_spark_stuff__time_of(year, month, 10 * day + (element(
           timestring, [loop__1__i]) - 48), hour, minute, 
           second) <= unsigned_types__unsigned32__last .
        ->
C1:    non_spark_stuff__time_of(year, month, 10 * day + (element(
           timestring, [loop__1__i]) - 48), hour, minute, 
           second) >= unsigned_types__unsigned32__first .
C2:    non_spark_stuff__time_of(year, month, 10 * day + (element(
           timestring, [loop__1__i]) - 48), hour, minute, 
           second) <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_54.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   loop__1__i <= 10 .
H21:   hour >= natural__first .
H22:   hour <= natural__last .
H23:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H24:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H25:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H26:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H27:   10 * hour >= integer__base__first .
H28:   10 * hour <= integer__base__last .
H29:   year >= natural__first .
H30:   year <= natural__last .
H31:   month >= natural__first .
H32:   month <= natural__last .
H33:   day >= natural__first .
H34:   day <= natural__last .
H35:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H36:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H37:   minute >= natural__first .
H38:   minute <= natural__last .
H39:   second >= natural__first .
H40:   second <= natural__last .
H41:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (10 * 
           hour + (element(timestring, [loop__1__i]) - 48) >= 
           hoursinaday)) or (minute >= minutesinanhour)) or (
           second >= secondsinaminute))) .
H42:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H43:   year >= natural__first .
H44:   year <= natural__last .
H45:   month >= natural__first .
H46:   month <= natural__last .
H47:   day >= natural__first .
H48:   day <= natural__last .
H49:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H50:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H51:   minute >= natural__first .
H52:   minute <= natural__last .
H53:   second >= natural__first .
H54:   second <= natural__last .
H55:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (10 * 
           hour + (element(timestring, [loop__1__i]) - 48) >= 
           hoursinaday)) or (minute >= minutesinanhour)) or (
           second >= secondsinaminute))) .
H56:   year >= natural__first .
H57:   year <= natural__last .
H58:   month >= natural__first .
H59:   month <= natural__last .
H60:   day >= natural__first .
H61:   day <= natural__last .
H62:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H63:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H64:   minute >= natural__first .
H65:   minute <= natural__last .
H66:   second >= natural__first .
H67:   second <= natural__last .
H68:   second >= natural__first .
H69:   second <= natural__last .
H70:   minute >= natural__first .
H71:   minute <= natural__last .
H72:   10 * hour + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H73:   10 * hour + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H74:   day >= natural__first .
H75:   day <= natural__last .
H76:   month >= natural__first .
H77:   month <= natural__last .
H78:   year >= natural__first .
H79:   year <= natural__last .
H80:   non_spark_stuff__time_of(year, month, day, 10 * hour + (element(
           timestring, [loop__1__i]) - 48), minute, second) >= 
           unsigned_types__unsigned32__first .
H81:   non_spark_stuff__time_of(year, month, day, 10 * hour + (element(
           timestring, [loop__1__i]) - 48), minute, second) <= 
           unsigned_types__unsigned32__last .
        ->
C1:    non_spark_stuff__time_of(year, month, day, 10 * hour + (element(
           timestring, [loop__1__i]) - 48), minute, second) >= 
           unsigned_types__unsigned32__first .
C2:    non_spark_stuff__time_of(year, month, day, 10 * hour + (element(
           timestring, [loop__1__i]) - 48), minute, second) <= 
           unsigned_types__unsigned32__last .
 

procedure_converttimestring_55.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   loop__1__i <= 12 .
H22:   minute >= natural__first .
H23:   minute <= natural__last .
H24:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H25:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H26:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H27:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H28:   10 * minute >= integer__base__first .
H29:   10 * minute <= integer__base__last .
H30:   year >= natural__first .
H31:   year <= natural__last .
H32:   month >= natural__first .
H33:   month <= natural__last .
H34:   day >= natural__first .
H35:   day <= natural__last .
H36:   hour >= natural__first .
H37:   hour <= natural__last .
H38:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H39:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H40:   second >= natural__first .
H41:   second <= natural__last .
H42:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (10 * minute + (element(
           timestring, [loop__1__i]) - 48) >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H43:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H44:   year >= natural__first .
H45:   year <= natural__last .
H46:   month >= natural__first .
H47:   month <= natural__last .
H48:   day >= natural__first .
H49:   day <= natural__last .
H50:   hour >= natural__first .
H51:   hour <= natural__last .
H52:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H53:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H54:   second >= natural__first .
H55:   second <= natural__last .
H56:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (10 * minute + (element(
           timestring, [loop__1__i]) - 48) >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H57:   year >= natural__first .
H58:   year <= natural__last .
H59:   month >= natural__first .
H60:   month <= natural__last .
H61:   day >= natural__first .
H62:   day <= natural__last .
H63:   hour >= natural__first .
H64:   hour <= natural__last .
H65:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H66:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H67:   second >= natural__first .
H68:   second <= natural__last .
H69:   second >= natural__first .
H70:   second <= natural__last .
H71:   10 * minute + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H72:   10 * minute + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H73:   hour >= natural__first .
H74:   hour <= natural__last .
H75:   day >= natural__first .
H76:   day <= natural__last .
H77:   month >= natural__first .
H78:   month <= natural__last .
H79:   year >= natural__first .
H80:   year <= natural__last .
H81:   non_spark_stuff__time_of(year, month, day, hour, 10 * 
           minute + (element(timestring, [loop__1__i]) - 48), 
           second) >= unsigned_types__unsigned32__first .
H82:   non_spark_stuff__time_of(year, month, day, hour, 10 * 
           minute + (element(timestring, [loop__1__i]) - 48), 
           second) <= unsigned_types__unsigned32__last .
        ->
C1:    non_spark_stuff__time_of(year, month, day, hour, 10 * 
           minute + (element(timestring, [loop__1__i]) - 48), 
           second) >= unsigned_types__unsigned32__first .
C2:    non_spark_stuff__time_of(year, month, day, hour, 10 * 
           minute + (element(timestring, [loop__1__i]) - 48), 
           second) <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_56.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   not (loop__1__i <= 12) .
H22:   loop__1__i <= 14 .
H23:   second >= natural__first .
H24:   second <= natural__last .
H25:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H26:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H27:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H28:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H29:   10 * second >= integer__base__first .
H30:   10 * second <= integer__base__last .
H31:   year >= natural__first .
H32:   year <= natural__last .
H33:   month >= natural__first .
H34:   month <= natural__last .
H35:   day >= natural__first .
H36:   day <= natural__last .
H37:   hour >= natural__first .
H38:   hour <= natural__last .
H39:   minute >= natural__first .
H40:   minute <= natural__last .
H41:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H42:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H43:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (10 * second + (element(
           timestring, [loop__1__i]) - 48) >= 
           secondsinaminute))) .
H44:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H45:   year >= natural__first .
H46:   year <= natural__last .
H47:   month >= natural__first .
H48:   month <= natural__last .
H49:   day >= natural__first .
H50:   day <= natural__last .
H51:   hour >= natural__first .
H52:   hour <= natural__last .
H53:   minute >= natural__first .
H54:   minute <= natural__last .
H55:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H56:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H57:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (10 * second + (element(
           timestring, [loop__1__i]) - 48) >= 
           secondsinaminute))) .
H58:   year >= natural__first .
H59:   year <= natural__last .
H60:   month >= natural__first .
H61:   month <= natural__last .
H62:   day >= natural__first .
H63:   day <= natural__last .
H64:   hour >= natural__first .
H65:   hour <= natural__last .
H66:   minute >= natural__first .
H67:   minute <= natural__last .
H68:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H69:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H70:   10 * second + (element(timestring, [loop__1__i]) - 48) >= 
           natural__first .
H71:   10 * second + (element(timestring, [loop__1__i]) - 48) <= 
           natural__last .
H72:   minute >= natural__first .
H73:   minute <= natural__last .
H74:   hour >= natural__first .
H75:   hour <= natural__last .
H76:   day >= natural__first .
H77:   day <= natural__last .
H78:   month >= natural__first .
H79:   month <= natural__last .
H80:   year >= natural__first .
H81:   year <= natural__last .
H82:   non_spark_stuff__time_of(year, month, day, hour, 
           minute, 10 * second + (element(timestring, [
           loop__1__i]) - 48)) >= unsigned_types__unsigned32__first .
H83:   non_spark_stuff__time_of(year, month, day, hour, 
           minute, 10 * second + (element(timestring, [
           loop__1__i]) - 48)) <= unsigned_types__unsigned32__last .
        ->
C1:    non_spark_stuff__time_of(year, month, day, hour, 
           minute, 10 * second + (element(timestring, [
           loop__1__i]) - 48)) >= unsigned_types__unsigned32__first .
C2:    non_spark_stuff__time_of(year, month, day, hour, 
           minute, 10 * second + (element(timestring, [
           loop__1__i]) - 48)) <= unsigned_types__unsigned32__last .
 

procedure_converttimestring_57.
H1:    year <= rr_type__rrsig_record_type__max_year .
H2:    month <= 12 .
H3:    day <= 31 .
H4:    hour <= 23 .
H5:    minute <= 59 .
H6:    second <= 59 .
H7:    for_all(i___1: integer, ((i___1 >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i___1 <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i___1]) >= character__first) and (element(
           timestring, [i___1]) <= character__last))) .
H8:    for_all(i_: integer, ((i_ >= 
           rr_type__rrsig_record_type__timestringtypeindex__first) and (
           i_ <= 
           rr_type__rrsig_record_type__timestringtypeindex__last)) -> ((element(
           timestring, [i_]) >= 48) and (element(timestring, [
           i_]) <= 57))) .
H9:    loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H10:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H11:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H12:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H13:   element(timestring, [loop__1__i]) - 48 >= natural__first .
H14:   element(timestring, [loop__1__i]) - 48 <= natural__last .
H15:   loop__1__i >= 
           rr_type__rrsig_record_type__timestringtypeindex__first .
H16:   loop__1__i <= 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H17:   not (loop__1__i <= 4) .
H18:   not (loop__1__i <= 6) .
H19:   not (loop__1__i <= 8) .
H20:   not (loop__1__i <= 10) .
H21:   not (loop__1__i <= 12) .
H22:   not (loop__1__i <= 14) .
H23:   year >= natural__first .
H24:   year <= natural__last .
H25:   month >= natural__first .
H26:   month <= natural__last .
H27:   day >= natural__first .
H28:   day <= natural__last .
H29:   hour >= natural__first .
H30:   hour <= natural__last .
H31:   minute >= natural__first .
H32:   minute <= natural__last .
H33:   second >= natural__first .
H34:   second <= natural__last .
H35:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H36:   loop__1__i = 
           rr_type__rrsig_record_type__timestringtypeindex__last .
H37:   year >= natural__first .
H38:   year <= natural__last .
H39:   month >= natural__first .
H40:   month <= natural__last .
H41:   day >= natural__first .
H42:   day <= natural__last .
H43:   hour >= natural__first .
H44:   hour <= natural__last .
H45:   minute >= natural__first .
H46:   minute <= natural__last .
H47:   second >= natural__first .
H48:   second <= natural__last .
H49:   not ((year > rr_type__rrsig_record_type__max_year) or (((((
           month > monthsinayear) or (day > maxdaysinamonth)) or (
           hour >= hoursinaday)) or (minute >= 
           minutesinanhour)) or (second >= secondsinaminute))) .
H50:   year >= natural__first .
H51:   year <= natural__last .
H52:   month >= natural__first .
H53:   month <= natural__last .
H54:   day >= natural__first .
H55:   day <= natural__last .
H56:   hour >= natural__first .
H57:   hour <= natural__last .
H58:   minute >= natural__first .
H59:   minute <= natural__last .
H60:   second >= natural__first .
H61:   second <= natural__last .
H62:   second >= natural__first .
H63:   second <= natural__last .
H64:   minute >= natural__first .
H65:   minute <= natural__last .
H66:   hour >= natural__first .
H67:   hour <= natural__last .
H68:   day >= natural__first .
H69:   day <= natural__last .
H70:   month >= natural__first .
H71:   month <= natural__last .
H72:   year >= natural__first .
H73:   year <= natural__last .
H74:   non_spark_stuff__time_of(year, month, day, hour, 
           minute, second) >= unsigned_types__unsigned32__first .
H75:   non_spark_stuff__time_of(year, month, day, hour, 
           minute, second) <= unsigned_types__unsigned32__last .
        ->
C1:    non_spark_stuff__time_of(year, month, day, hour, 
           minute, second) >= unsigned_types__unsigned32__first .
C2:    non_spark_stuff__time_of(year, month, day, hour, 
           minute, second) <= unsigned_types__unsigned32__last .
 

For path(s) from assertion of line 693 to finish:

procedure_converttimestring_58.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_59.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_60.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_61.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_62.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_63.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_64.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_65.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_66.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_67.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_68.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_69.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_70.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_71.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_72.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_73.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_74.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_75.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_76.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_77.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_78.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_79.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_80.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_81.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_82.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_83.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_84.
*** true .          /* trivially true VC removed by Examiner */


procedure_converttimestring_85.
*** true .          /* trivially true VC removed by Examiner */


