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

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


          procedure dns_table_pkg.DNS_Table_Type.insertNSECRecord




For path(s) from start to run-time check associated with statement of line 571:

procedure_insertnsecrecord_1.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           key, [i___1]) >= character__first) and (element(
           key, [i___1]) <= character__last))) .
H2:    fld_ttlinseconds(fld_inherit(therecord)) >= 
           unsigned_types__unsigned32__first .
H3:    fld_ttlinseconds(fld_inherit(therecord)) <= 
           unsigned_types__unsigned32__last .
H4:    fld_class(fld_inherit(therecord)) >= 
           rr_type__classtype__first .
H5:    fld_class(fld_inherit(therecord)) <= 
           rr_type__classtype__last .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(therecord), [i___1]) >= 
           character__first) and (element(fld_nextdomainname(
           therecord), [i___1]) <= character__last))) .
H7:    for_all(i___2: integer, ((i___2 >= 
           rr_type__linelengthindex__first) and (i___2 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(
           therecord), [i___2]) >= character__first) and (element(
           fld_recordlist(therecord), [i___2]) <= character__last))) .
H8:    fld_numberofrecordtypes(therecord) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H9:    fld_numberofrecordtypes(therecord) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H10:   for_all(i___3: integer, ((i___3 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___3 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(therecord), [i___3]) >= 
           dns_types__query_type__first) and (element(fld_recordtypes(
           therecord), [i___3]) <= dns_types__query_type__last))) .
H11:   fld_numberofblocks(therecord) >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H12:   fld_numberofblocks(therecord) <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H13:   for_all(i___4: integer, ((i___4 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___4 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(therecord), [i___4]) >= 
           dns_types__byte__first) and (element(fld_blocknumbers(
           therecord), [i___4]) <= dns_types__byte__last))) .
H14:   for_all(i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(therecord), [i___5]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(therecord), [i___5]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H15:   for_all(i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___7 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(therecord), [i___6]), [i___7]) >= 
           dns_types__byte__first) and (element(element(fld_bitmaps(
           therecord), [i___6]), [i___7]) <= dns_types__byte__last))))) .
H16:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= unsigned_types__unsigned32__last))))) .
H17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= rr_type__classtype__last))))) .
H18:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) >= character__first) and (element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) <= character__last))))))) .
H19:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___4: integer, ((i___4 >= 
           rr_type__linelengthindex__first) and (i___4 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) >= character__first) and (element(
           fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) <= character__last))))))) .
H20:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first) and (
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last))))) .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) >= dns_types__query_type__first) and (element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) <= dns_types__query_type__last))))))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__blocknumbervalue__first) and (
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__blocknumbervalue__last))))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) >= dns_types__byte__first) and (element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) <= dns_types__byte__last))))))) .
H24:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___7 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))))))) .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___8: integer, ((i___8 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___8 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___9: integer, ((i___9 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___9 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) >= dns_types__byte__first) and (element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) <= dns_types__byte__last))))))))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) >= character__first) and (element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) <= character__last))))))) .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           to_lower(key), [i___1]) >= character__first) and (element(
           to_lower(key), [i___1]) <= character__last))) .
H28:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           to_lower(key), [i___1]) >= character__first) and (element(
           to_lower(key), [i___1]) <= character__last))) .
H29:   hash(to_lower(key)) >= rr_type__numbucketsindextype__first .
H30:   hash(to_lower(key)) <= rr_type__numbucketsindextype__last .
        ->
C1:    hash(to_lower(key)) >= rr_type__numbucketsindextype__first .
C2:    hash(to_lower(key)) <= rr_type__numbucketsindextype__last .
 

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

procedure_insertnsecrecord_2.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           key, [i___1]) >= character__first) and (element(
           key, [i___1]) <= character__last))) .
H2:    fld_ttlinseconds(fld_inherit(therecord)) >= 
           unsigned_types__unsigned32__first .
H3:    fld_ttlinseconds(fld_inherit(therecord)) <= 
           unsigned_types__unsigned32__last .
H4:    fld_class(fld_inherit(therecord)) >= 
           rr_type__classtype__first .
H5:    fld_class(fld_inherit(therecord)) <= 
           rr_type__classtype__last .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(therecord), [i___1]) >= 
           character__first) and (element(fld_nextdomainname(
           therecord), [i___1]) <= character__last))) .
H7:    for_all(i___2: integer, ((i___2 >= 
           rr_type__linelengthindex__first) and (i___2 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(
           therecord), [i___2]) >= character__first) and (element(
           fld_recordlist(therecord), [i___2]) <= character__last))) .
H8:    fld_numberofrecordtypes(therecord) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H9:    fld_numberofrecordtypes(therecord) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H10:   for_all(i___3: integer, ((i___3 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___3 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(therecord), [i___3]) >= 
           dns_types__query_type__first) and (element(fld_recordtypes(
           therecord), [i___3]) <= dns_types__query_type__last))) .
H11:   fld_numberofblocks(therecord) >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H12:   fld_numberofblocks(therecord) <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H13:   for_all(i___4: integer, ((i___4 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___4 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(therecord), [i___4]) >= 
           dns_types__byte__first) and (element(fld_blocknumbers(
           therecord), [i___4]) <= dns_types__byte__last))) .
H14:   for_all(i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(therecord), [i___5]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(therecord), [i___5]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H15:   for_all(i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___7 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(therecord), [i___6]), [i___7]) >= 
           dns_types__byte__first) and (element(element(fld_bitmaps(
           therecord), [i___6]), [i___7]) <= dns_types__byte__last))))) .
H16:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= unsigned_types__unsigned32__last))))) .
H17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= rr_type__classtype__last))))) .
H18:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) >= character__first) and (element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) <= character__last))))))) .
H19:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___4: integer, ((i___4 >= 
           rr_type__linelengthindex__first) and (i___4 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) >= character__first) and (element(
           fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) <= character__last))))))) .
H20:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first) and (
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last))))) .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) >= dns_types__query_type__first) and (element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) <= dns_types__query_type__last))))))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__blocknumbervalue__first) and (
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__blocknumbervalue__last))))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) >= dns_types__byte__first) and (element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) <= dns_types__byte__last))))))) .
H24:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___7 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))))))) .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___8: integer, ((i___8 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___8 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___9: integer, ((i___9 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___9 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) >= dns_types__byte__first) and (element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) <= dns_types__byte__last))))))))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) >= character__first) and (element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) <= character__last))))))) .
H27:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           to_lower(key), [i___1]) >= character__first) and (element(
           to_lower(key), [i___1]) <= character__last))) .
H28:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           to_lower(key), [i___1]) >= character__first) and (element(
           to_lower(key), [i___1]) <= character__last))) .
H29:   hash(to_lower(key)) >= rr_type__numbucketsindextype__first .
H30:   hash(to_lower(key)) <= rr_type__numbucketsindextype__last .
H31:   hash(to_lower(key)) >= rr_type__numbucketsindextype__first .
H32:   hash(to_lower(key)) <= rr_type__numbucketsindextype__last .
        ->
C1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           key, [i___1]) >= character__first) and (element(
           key, [i___1]) <= character__last))) .
C2:    fld_ttlinseconds(fld_inherit(therecord)) >= 
           unsigned_types__unsigned32__first .
C3:    fld_ttlinseconds(fld_inherit(therecord)) <= 
           unsigned_types__unsigned32__last .
C4:    fld_class(fld_inherit(therecord)) >= 
           rr_type__classtype__first .
C5:    fld_class(fld_inherit(therecord)) <= 
           rr_type__classtype__last .
C6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(therecord), [i___1]) >= 
           character__first) and (element(fld_nextdomainname(
           therecord), [i___1]) <= character__last))) .
C7:    for_all(i___2: integer, ((i___2 >= 
           rr_type__linelengthindex__first) and (i___2 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(
           therecord), [i___2]) >= character__first) and (element(
           fld_recordlist(therecord), [i___2]) <= character__last))) .
C8:    fld_numberofrecordtypes(therecord) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
C9:    fld_numberofrecordtypes(therecord) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
C10:   for_all(i___3: integer, ((i___3 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___3 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(therecord), [i___3]) >= 
           dns_types__query_type__first) and (element(fld_recordtypes(
           therecord), [i___3]) <= dns_types__query_type__last))) .
C11:   fld_numberofblocks(therecord) >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
C12:   fld_numberofblocks(therecord) <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
C13:   for_all(i___4: integer, ((i___4 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___4 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(therecord), [i___4]) >= 
           dns_types__byte__first) and (element(fld_blocknumbers(
           therecord), [i___4]) <= dns_types__byte__last))) .
C14:   for_all(i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(therecord), [i___5]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(therecord), [i___5]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
C15:   for_all(i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___7 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(therecord), [i___6]), [i___7]) >= 
           dns_types__byte__first) and (element(element(fld_bitmaps(
           therecord), [i___6]), [i___7]) <= dns_types__byte__last))))) .
C16:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= unsigned_types__unsigned32__last))))) .
C17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= rr_type__classtype__last))))) .
C18:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) >= character__first) and (element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) <= character__last))))))) .
C19:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___4: integer, ((i___4 >= 
           rr_type__linelengthindex__first) and (i___4 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) >= character__first) and (element(
           fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) <= character__last))))))) .
C20:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first) and (
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last))))) .
C21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) >= dns_types__query_type__first) and (element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) <= dns_types__query_type__last))))))) .
C22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__blocknumbervalue__first) and (
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__blocknumbervalue__last))))) .
C23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) >= dns_types__byte__first) and (element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) <= dns_types__byte__last))))))) .
C24:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___7 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))))))) .
C25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___8: integer, ((i___8 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___8 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___9: integer, ((i___9 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___9 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) >= dns_types__byte__first) and (element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) <= dns_types__byte__last))))))))) .
C26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) >= character__first) and (element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) <= character__last))))))) .
C27:   rr_type__returnedrecordsindextype__first >= 
           rr_type__returnedrecordsindextype__first .
C28:   rr_type__returnedrecordsindextype__first <= 
           rr_type__returnedrecordsindextype__last .
C29:   rr_type__returnedrecordsindextype__first >= 
           rr_type__returnedrecordsindextype__first .
C30:   rr_type__returnedrecordsindextype__first <= 
           rr_type__returnedrecordsindextype__last .
 

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

procedure_insertnsecrecord_3.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           key, [i___1]) >= character__first) and (element(
           key, [i___1]) <= character__last))) .
H2:    fld_ttlinseconds(fld_inherit(therecord)) >= 
           unsigned_types__unsigned32__first .
H3:    fld_ttlinseconds(fld_inherit(therecord)) <= 
           unsigned_types__unsigned32__last .
H4:    fld_class(fld_inherit(therecord)) >= 
           rr_type__classtype__first .
H5:    fld_class(fld_inherit(therecord)) <= 
           rr_type__classtype__last .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(therecord), [i___1]) >= 
           character__first) and (element(fld_nextdomainname(
           therecord), [i___1]) <= character__last))) .
H7:    for_all(i___2: integer, ((i___2 >= 
           rr_type__linelengthindex__first) and (i___2 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(
           therecord), [i___2]) >= character__first) and (element(
           fld_recordlist(therecord), [i___2]) <= character__last))) .
H8:    fld_numberofrecordtypes(therecord) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H9:    fld_numberofrecordtypes(therecord) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H10:   for_all(i___3: integer, ((i___3 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___3 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(therecord), [i___3]) >= 
           dns_types__query_type__first) and (element(fld_recordtypes(
           therecord), [i___3]) <= dns_types__query_type__last))) .
H11:   fld_numberofblocks(therecord) >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H12:   fld_numberofblocks(therecord) <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H13:   for_all(i___4: integer, ((i___4 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___4 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(therecord), [i___4]) >= 
           dns_types__byte__first) and (element(fld_blocknumbers(
           therecord), [i___4]) <= dns_types__byte__last))) .
H14:   for_all(i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(therecord), [i___5]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(therecord), [i___5]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H15:   for_all(i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___7 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(therecord), [i___6]), [i___7]) >= 
           dns_types__byte__first) and (element(element(fld_bitmaps(
           therecord), [i___6]), [i___7]) <= dns_types__byte__last))))) .
H16:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= unsigned_types__unsigned32__last))))) .
H17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= rr_type__classtype__last))))) .
H18:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) >= character__first) and (element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) <= character__last))))))) .
H19:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___4: integer, ((i___4 >= 
           rr_type__linelengthindex__first) and (i___4 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) >= character__first) and (element(
           fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) <= character__last))))))) .
H20:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first) and (
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last))))) .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) >= dns_types__query_type__first) and (element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) <= dns_types__query_type__last))))))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__blocknumbervalue__first) and (
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__blocknumbervalue__last))))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) >= dns_types__byte__first) and (element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) <= dns_types__byte__last))))))) .
H24:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___7 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))))))) .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___8: integer, ((i___8 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___8 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___9: integer, ((i___9 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___9 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) >= dns_types__byte__first) and (element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) <= dns_types__byte__last))))))))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) >= character__first) and (element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) <= character__last))))))) .
H27:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H28:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H29:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H30:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H31:   bucket >= rr_type__numbucketsindextype__first .
H32:   bucket <= rr_type__numbucketsindextype__last .
H33:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H34:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H35:   bucket >= rr_type__numbucketsindextype__first .
H36:   bucket <= rr_type__numbucketsindextype__last .
H37:   element(element(dns_table_type__nsecrecordkeys, [
           bucket]), [loop__1__i]) = rr_type__blankowner .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           lower_key, [i___1]) >= character__first) and (element(
           lower_key, [i___1]) <= character__last))) .
H39:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H40:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H41:   bucket >= rr_type__numbucketsindextype__first .
H42:   bucket <= rr_type__numbucketsindextype__last .
H43:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H44:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H45:   bucket >= rr_type__numbucketsindextype__first .
H46:   bucket <= rr_type__numbucketsindextype__last .
H47:   true .
H48:   not true .
H49:   not (loop__1__i = rr_type__returnedrecordsindextype__last) .
        ->
C1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           key, [i___1]) >= character__first) and (element(
           key, [i___1]) <= character__last))) .
C2:    fld_ttlinseconds(fld_inherit(therecord)) >= 
           unsigned_types__unsigned32__first .
C3:    fld_ttlinseconds(fld_inherit(therecord)) <= 
           unsigned_types__unsigned32__last .
C4:    fld_class(fld_inherit(therecord)) >= 
           rr_type__classtype__first .
C5:    fld_class(fld_inherit(therecord)) <= 
           rr_type__classtype__last .
C6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(therecord), [i___1]) >= 
           character__first) and (element(fld_nextdomainname(
           therecord), [i___1]) <= character__last))) .
C7:    for_all(i___2: integer, ((i___2 >= 
           rr_type__linelengthindex__first) and (i___2 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(
           therecord), [i___2]) >= character__first) and (element(
           fld_recordlist(therecord), [i___2]) <= character__last))) .
C8:    fld_numberofrecordtypes(therecord) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
C9:    fld_numberofrecordtypes(therecord) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
C10:   for_all(i___3: integer, ((i___3 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___3 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(therecord), [i___3]) >= 
           dns_types__query_type__first) and (element(fld_recordtypes(
           therecord), [i___3]) <= dns_types__query_type__last))) .
C11:   fld_numberofblocks(therecord) >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
C12:   fld_numberofblocks(therecord) <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
C13:   for_all(i___4: integer, ((i___4 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___4 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(therecord), [i___4]) >= 
           dns_types__byte__first) and (element(fld_blocknumbers(
           therecord), [i___4]) <= dns_types__byte__last))) .
C14:   for_all(i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(therecord), [i___5]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(therecord), [i___5]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
C15:   for_all(i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___7 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(therecord), [i___6]), [i___7]) >= 
           dns_types__byte__first) and (element(element(fld_bitmaps(
           therecord), [i___6]), [i___7]) <= dns_types__byte__last))))) .
C16:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2]))) >= 
           unsigned_types__unsigned32__first) and (fld_ttlinseconds(
           fld_inherit(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2]))) <= 
           unsigned_types__unsigned32__last))))) .
C17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2]))) >= 
           rr_type__classtype__first) and (fld_class(fld_inherit(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2]))) <= 
           rr_type__classtype__last))))) .
C18:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])), [
           i___3]) >= character__first) and (element(fld_nextdomainname(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])), [
           i___3]) <= character__last))))))) .
C19:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___4: integer, ((i___4 >= 
           rr_type__linelengthindex__first) and (i___4 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])), [
           i___4]) >= character__first) and (element(fld_recordlist(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])), [
           i___4]) <= character__last))))))) .
C20:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofrecordtypes(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first) and (
           fld_numberofrecordtypes(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last))))) .
C21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])), [
           i___5]) >= dns_types__query_type__first) and (element(
           fld_recordtypes(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])), [
           i___5]) <= dns_types__query_type__last))))))) .
C22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofblocks(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])) >= 
           rr_type__nsec_record_type__blocknumbervalue__first) and (
           fld_numberofblocks(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])) <= 
           rr_type__nsec_record_type__blocknumbervalue__last))))) .
C23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])), [
           i___6]) >= dns_types__byte__first) and (element(
           fld_blocknumbers(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])), [
           i___6]) <= dns_types__byte__last))))))) .
C24:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___7 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])), [
           i___7]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])), [
           i___7]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))))))) .
C25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___8: integer, ((i___8 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___8 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___9: integer, ((i___9 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___9 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])), [
           i___8]), [i___9]) >= dns_types__byte__first) and (element(element(
           fld_bitmaps(element(element(update(
           dns_table_type__nsecrecordtable, [bucket], update(element(
           dns_table_type__nsecrecordtable, [bucket]), [
           loop__1__i], therecord)), [i___1]), [i___2])), [
           i___8]), [i___9]) <= dns_types__byte__last))))))))) .
C26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(element(element(update(
           dns_table_type__nsecrecordkeys, [bucket], update(element(
           dns_table_type__nsecrecordkeys, [bucket]), [
           loop__1__i], lower_key)), [i___1]), [i___2]), [
           i___3]) >= character__first) and (element(element(element(update(
           dns_table_type__nsecrecordkeys, [bucket], update(element(
           dns_table_type__nsecrecordkeys, [bucket]), [
           loop__1__i], lower_key)), [i___1]), [i___2]), [
           i___3]) <= character__last))))))) .
C27:   loop__1__i + 1 >= rr_type__returnedrecordsindextype__first .
C28:   loop__1__i + 1 <= rr_type__returnedrecordsindextype__last .
C29:   loop__1__i + 1 >= rr_type__returnedrecordsindextype__first .
C30:   loop__1__i + 1 <= rr_type__returnedrecordsindextype__last .
 

procedure_insertnsecrecord_4.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           key, [i___1]) >= character__first) and (element(
           key, [i___1]) <= character__last))) .
H2:    fld_ttlinseconds(fld_inherit(therecord)) >= 
           unsigned_types__unsigned32__first .
H3:    fld_ttlinseconds(fld_inherit(therecord)) <= 
           unsigned_types__unsigned32__last .
H4:    fld_class(fld_inherit(therecord)) >= 
           rr_type__classtype__first .
H5:    fld_class(fld_inherit(therecord)) <= 
           rr_type__classtype__last .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(therecord), [i___1]) >= 
           character__first) and (element(fld_nextdomainname(
           therecord), [i___1]) <= character__last))) .
H7:    for_all(i___2: integer, ((i___2 >= 
           rr_type__linelengthindex__first) and (i___2 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(
           therecord), [i___2]) >= character__first) and (element(
           fld_recordlist(therecord), [i___2]) <= character__last))) .
H8:    fld_numberofrecordtypes(therecord) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H9:    fld_numberofrecordtypes(therecord) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H10:   for_all(i___3: integer, ((i___3 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___3 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(therecord), [i___3]) >= 
           dns_types__query_type__first) and (element(fld_recordtypes(
           therecord), [i___3]) <= dns_types__query_type__last))) .
H11:   fld_numberofblocks(therecord) >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H12:   fld_numberofblocks(therecord) <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H13:   for_all(i___4: integer, ((i___4 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___4 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(therecord), [i___4]) >= 
           dns_types__byte__first) and (element(fld_blocknumbers(
           therecord), [i___4]) <= dns_types__byte__last))) .
H14:   for_all(i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(therecord), [i___5]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(therecord), [i___5]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H15:   for_all(i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___7 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(therecord), [i___6]), [i___7]) >= 
           dns_types__byte__first) and (element(element(fld_bitmaps(
           therecord), [i___6]), [i___7]) <= dns_types__byte__last))))) .
H16:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= unsigned_types__unsigned32__last))))) .
H17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= rr_type__classtype__last))))) .
H18:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) >= character__first) and (element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) <= character__last))))))) .
H19:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___4: integer, ((i___4 >= 
           rr_type__linelengthindex__first) and (i___4 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) >= character__first) and (element(
           fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) <= character__last))))))) .
H20:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first) and (
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last))))) .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) >= dns_types__query_type__first) and (element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) <= dns_types__query_type__last))))))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__blocknumbervalue__first) and (
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__blocknumbervalue__last))))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) >= dns_types__byte__first) and (element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) <= dns_types__byte__last))))))) .
H24:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___7 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))))))) .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___8: integer, ((i___8 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___8 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___9: integer, ((i___9 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___9 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) >= dns_types__byte__first) and (element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) <= dns_types__byte__last))))))))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) >= character__first) and (element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) <= character__last))))))) .
H27:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H28:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H29:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H30:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H31:   bucket >= rr_type__numbucketsindextype__first .
H32:   bucket <= rr_type__numbucketsindextype__last .
H33:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H34:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H35:   bucket >= rr_type__numbucketsindextype__first .
H36:   bucket <= rr_type__numbucketsindextype__last .
H37:   not (element(element(dns_table_type__nsecrecordkeys, [
           bucket]), [loop__1__i]) = rr_type__blankowner) .
H38:   true .
H39:   not success .
H40:   not (loop__1__i = rr_type__returnedrecordsindextype__last) .
        ->
C1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           key, [i___1]) >= character__first) and (element(
           key, [i___1]) <= character__last))) .
C2:    fld_ttlinseconds(fld_inherit(therecord)) >= 
           unsigned_types__unsigned32__first .
C3:    fld_ttlinseconds(fld_inherit(therecord)) <= 
           unsigned_types__unsigned32__last .
C4:    fld_class(fld_inherit(therecord)) >= 
           rr_type__classtype__first .
C5:    fld_class(fld_inherit(therecord)) <= 
           rr_type__classtype__last .
C6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(therecord), [i___1]) >= 
           character__first) and (element(fld_nextdomainname(
           therecord), [i___1]) <= character__last))) .
C7:    for_all(i___2: integer, ((i___2 >= 
           rr_type__linelengthindex__first) and (i___2 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(
           therecord), [i___2]) >= character__first) and (element(
           fld_recordlist(therecord), [i___2]) <= character__last))) .
C8:    fld_numberofrecordtypes(therecord) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
C9:    fld_numberofrecordtypes(therecord) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
C10:   for_all(i___3: integer, ((i___3 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___3 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(therecord), [i___3]) >= 
           dns_types__query_type__first) and (element(fld_recordtypes(
           therecord), [i___3]) <= dns_types__query_type__last))) .
C11:   fld_numberofblocks(therecord) >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
C12:   fld_numberofblocks(therecord) <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
C13:   for_all(i___4: integer, ((i___4 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___4 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(therecord), [i___4]) >= 
           dns_types__byte__first) and (element(fld_blocknumbers(
           therecord), [i___4]) <= dns_types__byte__last))) .
C14:   for_all(i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(therecord), [i___5]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(therecord), [i___5]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
C15:   for_all(i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___7 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(therecord), [i___6]), [i___7]) >= 
           dns_types__byte__first) and (element(element(fld_bitmaps(
           therecord), [i___6]), [i___7]) <= dns_types__byte__last))))) .
C16:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= unsigned_types__unsigned32__last))))) .
C17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= rr_type__classtype__last))))) .
C18:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) >= character__first) and (element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) <= character__last))))))) .
C19:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___4: integer, ((i___4 >= 
           rr_type__linelengthindex__first) and (i___4 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) >= character__first) and (element(
           fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) <= character__last))))))) .
C20:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first) and (
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last))))) .
C21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) >= dns_types__query_type__first) and (element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) <= dns_types__query_type__last))))))) .
C22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__blocknumbervalue__first) and (
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__blocknumbervalue__last))))) .
C23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) >= dns_types__byte__first) and (element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) <= dns_types__byte__last))))))) .
C24:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___7 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))))))) .
C25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___8: integer, ((i___8 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___8 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___9: integer, ((i___9 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___9 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) >= dns_types__byte__first) and (element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) <= dns_types__byte__last))))))))) .
C26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) >= character__first) and (element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) <= character__last))))))) .
C27:   loop__1__i + 1 >= rr_type__returnedrecordsindextype__first .
C28:   loop__1__i + 1 <= rr_type__returnedrecordsindextype__last .
C29:   loop__1__i + 1 >= rr_type__returnedrecordsindextype__first .
C30:   loop__1__i + 1 <= rr_type__returnedrecordsindextype__last .
 

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

procedure_insertnsecrecord_5.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           key, [i___1]) >= character__first) and (element(
           key, [i___1]) <= character__last))) .
H2:    fld_ttlinseconds(fld_inherit(therecord)) >= 
           unsigned_types__unsigned32__first .
H3:    fld_ttlinseconds(fld_inherit(therecord)) <= 
           unsigned_types__unsigned32__last .
H4:    fld_class(fld_inherit(therecord)) >= 
           rr_type__classtype__first .
H5:    fld_class(fld_inherit(therecord)) <= 
           rr_type__classtype__last .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(therecord), [i___1]) >= 
           character__first) and (element(fld_nextdomainname(
           therecord), [i___1]) <= character__last))) .
H7:    for_all(i___2: integer, ((i___2 >= 
           rr_type__linelengthindex__first) and (i___2 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(
           therecord), [i___2]) >= character__first) and (element(
           fld_recordlist(therecord), [i___2]) <= character__last))) .
H8:    fld_numberofrecordtypes(therecord) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H9:    fld_numberofrecordtypes(therecord) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H10:   for_all(i___3: integer, ((i___3 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___3 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(therecord), [i___3]) >= 
           dns_types__query_type__first) and (element(fld_recordtypes(
           therecord), [i___3]) <= dns_types__query_type__last))) .
H11:   fld_numberofblocks(therecord) >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H12:   fld_numberofblocks(therecord) <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H13:   for_all(i___4: integer, ((i___4 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___4 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(therecord), [i___4]) >= 
           dns_types__byte__first) and (element(fld_blocknumbers(
           therecord), [i___4]) <= dns_types__byte__last))) .
H14:   for_all(i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(therecord), [i___5]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(therecord), [i___5]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H15:   for_all(i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___7 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(therecord), [i___6]), [i___7]) >= 
           dns_types__byte__first) and (element(element(fld_bitmaps(
           therecord), [i___6]), [i___7]) <= dns_types__byte__last))))) .
H16:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= unsigned_types__unsigned32__last))))) .
H17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= rr_type__classtype__last))))) .
H18:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) >= character__first) and (element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) <= character__last))))))) .
H19:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___4: integer, ((i___4 >= 
           rr_type__linelengthindex__first) and (i___4 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) >= character__first) and (element(
           fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) <= character__last))))))) .
H20:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first) and (
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last))))) .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) >= dns_types__query_type__first) and (element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) <= dns_types__query_type__last))))))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__blocknumbervalue__first) and (
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__blocknumbervalue__last))))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) >= dns_types__byte__first) and (element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) <= dns_types__byte__last))))))) .
H24:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___7 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))))))) .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___8: integer, ((i___8 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___8 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___9: integer, ((i___9 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___9 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) >= dns_types__byte__first) and (element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) <= dns_types__byte__last))))))))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) >= character__first) and (element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) <= character__last))))))) .
H27:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H28:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H29:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H30:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H31:   bucket >= rr_type__numbucketsindextype__first .
H32:   bucket <= rr_type__numbucketsindextype__last .
        ->
C1:    loop__1__i >= rr_type__returnedrecordsindextype__first .
C2:    loop__1__i <= rr_type__returnedrecordsindextype__last .
C3:    bucket >= rr_type__numbucketsindextype__first .
C4:    bucket <= rr_type__numbucketsindextype__last .
 

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

procedure_insertnsecrecord_6.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           key, [i___1]) >= character__first) and (element(
           key, [i___1]) <= character__last))) .
H2:    fld_ttlinseconds(fld_inherit(therecord)) >= 
           unsigned_types__unsigned32__first .
H3:    fld_ttlinseconds(fld_inherit(therecord)) <= 
           unsigned_types__unsigned32__last .
H4:    fld_class(fld_inherit(therecord)) >= 
           rr_type__classtype__first .
H5:    fld_class(fld_inherit(therecord)) <= 
           rr_type__classtype__last .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(therecord), [i___1]) >= 
           character__first) and (element(fld_nextdomainname(
           therecord), [i___1]) <= character__last))) .
H7:    for_all(i___2: integer, ((i___2 >= 
           rr_type__linelengthindex__first) and (i___2 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(
           therecord), [i___2]) >= character__first) and (element(
           fld_recordlist(therecord), [i___2]) <= character__last))) .
H8:    fld_numberofrecordtypes(therecord) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H9:    fld_numberofrecordtypes(therecord) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H10:   for_all(i___3: integer, ((i___3 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___3 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(therecord), [i___3]) >= 
           dns_types__query_type__first) and (element(fld_recordtypes(
           therecord), [i___3]) <= dns_types__query_type__last))) .
H11:   fld_numberofblocks(therecord) >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H12:   fld_numberofblocks(therecord) <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H13:   for_all(i___4: integer, ((i___4 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___4 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(therecord), [i___4]) >= 
           dns_types__byte__first) and (element(fld_blocknumbers(
           therecord), [i___4]) <= dns_types__byte__last))) .
H14:   for_all(i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(therecord), [i___5]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(therecord), [i___5]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H15:   for_all(i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___7 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(therecord), [i___6]), [i___7]) >= 
           dns_types__byte__first) and (element(element(fld_bitmaps(
           therecord), [i___6]), [i___7]) <= dns_types__byte__last))))) .
H16:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= unsigned_types__unsigned32__last))))) .
H17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= rr_type__classtype__last))))) .
H18:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) >= character__first) and (element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) <= character__last))))))) .
H19:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___4: integer, ((i___4 >= 
           rr_type__linelengthindex__first) and (i___4 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) >= character__first) and (element(
           fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) <= character__last))))))) .
H20:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first) and (
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last))))) .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) >= dns_types__query_type__first) and (element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) <= dns_types__query_type__last))))))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__blocknumbervalue__first) and (
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__blocknumbervalue__last))))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) >= dns_types__byte__first) and (element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) <= dns_types__byte__last))))))) .
H24:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___7 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))))))) .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___8: integer, ((i___8 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___8 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___9: integer, ((i___9 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___9 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) >= dns_types__byte__first) and (element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) <= dns_types__byte__last))))))))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) >= character__first) and (element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) <= character__last))))))) .
H27:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H28:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H29:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H30:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H31:   bucket >= rr_type__numbucketsindextype__first .
H32:   bucket <= rr_type__numbucketsindextype__last .
H33:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H34:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H35:   bucket >= rr_type__numbucketsindextype__first .
H36:   bucket <= rr_type__numbucketsindextype__last .
H37:   element(element(dns_table_type__nsecrecordkeys, [
           bucket]), [loop__1__i]) = rr_type__blankowner .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           lower_key, [i___1]) >= character__first) and (element(
           lower_key, [i___1]) <= character__last))) .
        ->
C1:    loop__1__i >= rr_type__returnedrecordsindextype__first .
C2:    loop__1__i <= rr_type__returnedrecordsindextype__last .
C3:    bucket >= rr_type__numbucketsindextype__first .
C4:    bucket <= rr_type__numbucketsindextype__last .
 

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

procedure_insertnsecrecord_7.
H1:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           key, [i___1]) >= character__first) and (element(
           key, [i___1]) <= character__last))) .
H2:    fld_ttlinseconds(fld_inherit(therecord)) >= 
           unsigned_types__unsigned32__first .
H3:    fld_ttlinseconds(fld_inherit(therecord)) <= 
           unsigned_types__unsigned32__last .
H4:    fld_class(fld_inherit(therecord)) >= 
           rr_type__classtype__first .
H5:    fld_class(fld_inherit(therecord)) <= 
           rr_type__classtype__last .
H6:    for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(therecord), [i___1]) >= 
           character__first) and (element(fld_nextdomainname(
           therecord), [i___1]) <= character__last))) .
H7:    for_all(i___2: integer, ((i___2 >= 
           rr_type__linelengthindex__first) and (i___2 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(
           therecord), [i___2]) >= character__first) and (element(
           fld_recordlist(therecord), [i___2]) <= character__last))) .
H8:    fld_numberofrecordtypes(therecord) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first .
H9:    fld_numberofrecordtypes(therecord) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last .
H10:   for_all(i___3: integer, ((i___3 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___3 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(therecord), [i___3]) >= 
           dns_types__query_type__first) and (element(fld_recordtypes(
           therecord), [i___3]) <= dns_types__query_type__last))) .
H11:   fld_numberofblocks(therecord) >= 
           rr_type__nsec_record_type__blocknumbervalue__first .
H12:   fld_numberofblocks(therecord) <= 
           rr_type__nsec_record_type__blocknumbervalue__last .
H13:   for_all(i___4: integer, ((i___4 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___4 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(therecord), [i___4]) >= 
           dns_types__byte__first) and (element(fld_blocknumbers(
           therecord), [i___4]) <= dns_types__byte__last))) .
H14:   for_all(i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(therecord), [i___5]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(therecord), [i___5]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))) .
H15:   for_all(i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___7 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(therecord), [i___6]), [i___7]) >= 
           dns_types__byte__first) and (element(element(fld_bitmaps(
           therecord), [i___6]), [i___7]) <= dns_types__byte__last))))) .
H16:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= unsigned_types__unsigned32__first) and (
           fld_ttlinseconds(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= unsigned_types__unsigned32__last))))) .
H17:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_class(fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) >= rr_type__classtype__first) and (fld_class(
           fld_inherit(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2]))) <= rr_type__classtype__last))))) .
H18:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) >= character__first) and (element(
           fld_nextdomainname(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___3]) <= character__last))))))) .
H19:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___4: integer, ((i___4 >= 
           rr_type__linelengthindex__first) and (i___4 <= 
           rr_type__linelengthindex__last)) -> ((element(fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) >= character__first) and (element(
           fld_recordlist(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___4]) <= character__last))))))) .
H20:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__recordtypeindexvalue__first) and (
           fld_numberofrecordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__recordtypeindexvalue__last))))) .
H21:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___5: integer, ((i___5 >= 
           rr_type__nsec_record_type__recordtypearrayindex__first) and (
           i___5 <= 
           rr_type__nsec_record_type__recordtypearrayindex__last)) -> ((element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) >= dns_types__query_type__first) and (element(
           fld_recordtypes(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___5]) <= dns_types__query_type__last))))))) .
H22:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> ((
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) >= 
           rr_type__nsec_record_type__blocknumbervalue__first) and (
           fld_numberofblocks(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])) <= 
           rr_type__nsec_record_type__blocknumbervalue__last))))) .
H23:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___6: integer, ((i___6 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___6 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) >= dns_types__byte__first) and (element(
           fld_blocknumbers(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___6]) <= dns_types__byte__last))))))) .
H24:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___7: integer, ((i___7 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___7 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> ((element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) >= 
           rr_type__nsec_record_type__blocklengthvalue__first) and (element(
           fld_blocklengths(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___7]) <= 
           rr_type__nsec_record_type__blocklengthvalue__last))))))) .
H25:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___8: integer, ((i___8 >= 
           rr_type__nsec_record_type__blocknumberarrayindex__first) and (
           i___8 <= 
           rr_type__nsec_record_type__blocknumberarrayindex__last)) -> (for_all(
           i___9: integer, ((i___9 >= 
           rr_type__nsec_record_type__bitmapindex__first) and (
           i___9 <= rr_type__nsec_record_type__bitmapindex__last)) -> ((element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) >= dns_types__byte__first) and (element(element(
           fld_bitmaps(element(element(
           dns_table_type__nsecrecordtable, [i___1]), [
           i___2])), [i___8]), [i___9]) <= dns_types__byte__last))))))))) .
H26:   for_all(i___1: integer, ((i___1 >= 
           rr_type__numbucketsindextype__first) and (i___1 <= 
           rr_type__numbucketsindextype__last)) -> (for_all(
           i___2: integer, ((i___2 >= 
           rr_type__returnedrecordsindextype__first) and (
           i___2 <= rr_type__returnedrecordsindextype__last)) -> (for_all(
           i___3: integer, ((i___3 >= 
           rr_type__wirestringtypeindex__first) and (i___3 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) >= character__first) and (element(element(element(
           dns_table_type__nsecrecordkeys, [i___1]), [i___2]), [
           i___3]) <= character__last))))))) .
H27:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H28:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H29:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H30:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H31:   bucket >= rr_type__numbucketsindextype__first .
H32:   bucket <= rr_type__numbucketsindextype__last .
H33:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H34:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H35:   bucket >= rr_type__numbucketsindextype__first .
H36:   bucket <= rr_type__numbucketsindextype__last .
H37:   element(element(dns_table_type__nsecrecordkeys, [
           bucket]), [loop__1__i]) = rr_type__blankowner .
H38:   for_all(i___1: integer, ((i___1 >= 
           rr_type__wirestringtypeindex__first) and (i___1 <= 
           rr_type__wirestringtypeindex__last)) -> ((element(
           lower_key, [i___1]) >= character__first) and (element(
           lower_key, [i___1]) <= character__last))) .
H39:   loop__1__i >= rr_type__returnedrecordsindextype__first .
H40:   loop__1__i <= rr_type__returnedrecordsindextype__last .
H41:   bucket >= rr_type__numbucketsindextype__first .
H42:   bucket <= rr_type__numbucketsindextype__last .
        ->
C1:    loop__1__i >= rr_type__returnedrecordsindextype__first .
C2:    loop__1__i <= rr_type__returnedrecordsindextype__last .
C3:    bucket >= rr_type__numbucketsindextype__first .
C4:    bucket <= rr_type__numbucketsindextype__last .
 

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

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


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


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


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


For checks of refinement integrity: 

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


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


