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

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



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

procedure Process_Dns_Request.Create_NXDOMAIN_Response






@@@@@@@@@@  VC: procedure_create_nxdomain_response_1.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
***  Proved C1:  qname_location >= dns_types__qname_ptr_range__first
     using hypothesis H5.
***  Proved C2:  qname_location <= dns_types__qname_ptr_range__last
     using hypothesis H6.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_2.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H23 has been replaced by "true".  (It is already present, as H6)
          .
%%%  Simplified C11 on reading formula in, to give:
     %%%  C11:  true
***  Proved C11:  true
-S-  Applied substitution rule create_nxdom_rules(33).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__first by:
          0.
<S>  New C1:  start_byte + dns_types__header_bits div 8 >= 0
<S>  New C3:  start_byte + dns_types__header_bits div 8 >= 0
-S-  Applied substitution rule create_nxdom_rules(34).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__last by:
          8192.
<S>  New C2:  start_byte + dns_types__header_bits div 8 <= 8192
<S>  New C4:  start_byte + dns_types__header_bits div 8 <= 8192
-S-  Applied substitution rule create_nxdom_rules(40).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__first by:
          - 2147483648.
<S>  New C5:  start_byte + dns_types__header_bits div 8 >= - 2147483648
-S-  Applied substitution rule create_nxdom_rules(41).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__last by:
          2147483647.
<S>  New C6:  start_byte + dns_types__header_bits div 8 <= 2147483647
-S-  Applied substitution rule create_nxdom_rules(38).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H2:  start_byte >= 1
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
<S>  New C7:  dns_types__header_bits div 8 >= 1
-S-  Applied substitution rule create_nxdom_rules(39).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H3:  start_byte <= 8180
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
<S>  New C8:  dns_types__header_bits div 8 <= 8180
-S-  Applied substitution rule create_nxdom_rules(4).
     This was achieved by replacing all occurrences of system__min_int by:
          - 9223372036854775808.
<S>  New C9:  dns_types__header_bits div 8 >= - 9223372036854775808
-S-  Applied substitution rule create_nxdom_rules(5).
     This was achieved by replacing all occurrences of system__max_int by:
          9223372036854775807.
<S>  New C10:  dns_types__header_bits div 8 <= 9223372036854775807
-S-  Applied substitution rule create_nxdom_rules(1).
     This was achieved by replacing all occurrences of dns_types__packet_size 
          by:
          8192.
<S>  New H1:  start_byte <= 8192
-S-  Applied substitution rule create_nxdom_rules(2).
     This was achieved by replacing all occurrences of dns_types__header_bits 
          by:
          96.
<S>  New C1:  start_byte >= - 12
<S>  New C3:  start_byte >= - 12
<S>  New C2:  start_byte <= 8180
<S>  New C4:  start_byte <= 8180
<S>  New C5:  start_byte >= - 2147483660
<S>  New C6:  start_byte <= 2147483635
<S>  New C7:  true
<S>  New C8:  true
<S>  New C9:  true
<S>  New C10:  true
-S-  Applied substitution rule create_nxdom_rules(12).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 
          character__last)
-S-  Applied substitution rule create_nxdom_rules(13).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 255)
-S-  Applied substitution rule create_nxdom_rules(27).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__first by:
          0.
<S>  New H5:  qname_location >= 0
-S-  Applied substitution rule create_nxdom_rules(28).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__last by:
          16383.
<S>  New H6:  qname_location <= 16383
-S-  Applied substitution rule create_nxdom_rules(44).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(45).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= 255)
-S-  Applied substitution rule create_nxdom_rules(51).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H7:  fld_messageid(fld_header(output_packet)) >= 0
<S>  New H13:  fld_qdcount(fld_header(output_packet)) >= 0
<S>  New H15:  fld_ancount(fld_header(output_packet)) >= 0
<S>  New H17:  fld_nscount(fld_header(output_packet)) >= 0
<S>  New H19:  fld_arcount(fld_header(output_packet)) >= 0
-S-  Applied substitution rule create_nxdom_rules(52).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H8:  fld_messageid(fld_header(output_packet)) <= 65535
<S>  New H14:  fld_qdcount(fld_header(output_packet)) <= 65535
<S>  New H16:  fld_ancount(fld_header(output_packet)) <= 65535
<S>  New H18:  fld_nscount(fld_header(output_packet)) <= 65535
<S>  New H20:  fld_arcount(fld_header(output_packet)) <= 65535
-S-  Applied substitution rule create_nxdom_rules(57).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__first by:
          dns_types__query.
<S>  New H9:  dns_types__query <= fld_opcode(fld_header(output_packet))
-S-  Applied substitution rule create_nxdom_rules(58).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__last by:
          dns_types__status.
<S>  New H10:  fld_opcode(fld_header(output_packet)) <= dns_types__status
-S-  Applied substitution rule create_nxdom_rules(83).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H11:  dns_types__no_error <= fld_rcode(fld_header(output_packet))
-S-  Applied substitution rule create_nxdom_rules(84).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H12:  fld_rcode(fld_header(output_packet)) <= dns_types__refused
-S-  Applied substitution rule create_nxdom_rules(119).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(domainname, [i___1]
          ) and element(domainname, [i___1]) <= 255)
-S-  Applied substitution rule create_nxdom_rules(120).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(domainname, [i___1]) and element(domainname, [i___1]) <= 255)
***  Proved C1:  start_byte >= - 12
     using hypothesis H2.
***  Proved C3:  start_byte >= - 12
     using hypothesis H2.
***  Proved C2:  start_byte <= 8180
     using hypothesis H3.
***  Proved C4:  start_byte <= 8180
     using hypothesis H3.
***  Proved C5:  start_byte >= - 2147483660
     using hypothesis H2.
***  Proved C6:  start_byte <= 2147483635
     using hypothesis H3.
***  Proved C7:  true
***  Proved C8:  true
***  Proved C9:  true
***  Proved C10:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_3.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H23 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H25).
%%%  Simplified H34 on reading formula in, to give:
     %%%  H34:  true
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  dns_types__response_code__first <= dns_types__name_error
-S-  Applied substitution rule create_nxdom_rules(83).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H11:  dns_types__no_error <= fld_rcode(fld_header(output_packet))
<S>  New C1:  true
-S-  Applied substitution rule create_nxdom_rules(84).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H12:  fld_rcode(fld_header(output_packet)) <= dns_types__refused
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_4.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H23 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H25).
%%%  Simplified H34 on reading formula in, to give:
     %%%  H34:  true
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__response_code__first <= dns_types__name_error
-S-  Applied substitution rule create_nxdom_rules(51).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H7:  fld_messageid(fld_header(output_packet)) >= 0
<S>  New H13:  fld_qdcount(fld_header(output_packet)) >= 0
<S>  New H15:  fld_ancount(fld_header(output_packet)) >= 0
<S>  New H17:  fld_nscount(fld_header(output_packet)) >= 0
<S>  New H19:  fld_arcount(fld_header(output_packet)) >= 0
<S>  New C1:  true
-S-  Applied substitution rule create_nxdom_rules(52).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H8:  fld_messageid(fld_header(output_packet)) <= 65535
<S>  New H14:  fld_qdcount(fld_header(output_packet)) <= 65535
<S>  New H16:  fld_ancount(fld_header(output_packet)) <= 65535
<S>  New H18:  fld_nscount(fld_header(output_packet)) <= 65535
<S>  New H20:  fld_arcount(fld_header(output_packet)) <= 65535
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_5.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H23 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H25).
%%%  Simplified H34 on reading formula in, to give:
     %%%  H34:  true
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__response_code__first <= dns_types__name_error
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H46 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H47 has been replaced by "true".  (It is already present, as H6)
          .
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  true
***  Proved C5:  true
-S-  Applied substitution rule create_nxdom_rules(27).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__first by:
          0.
<S>  New H5:  qname_location >= 0
<S>  New C1:  start_byte + dns_types__header_bits div 8 >= 0
-S-  Applied substitution rule create_nxdom_rules(28).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__last by:
          16383.
<S>  New H6:  qname_location <= 16383
<S>  New C2:  start_byte + dns_types__header_bits div 8 <= 16383
-S-  Applied substitution rule create_nxdom_rules(17).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H43:  true
<S>  New C3:  element(domainname, [rr_type__wirestringtypeindex__first]) >= 0
-S-  Applied substitution rule create_nxdom_rules(18).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H44:  true
<S>  New C4:  element(domainname, [rr_type__wirestringtypeindex__first]) <= 
          2147483647
-S-  Applied substitution rule create_nxdom_rules(119).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> character__first <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 
          character__last)
<S>  New C6:  1 <= rr_type__wirestringtypeindex__last
<S>  New C3:  element(domainname, [1]) >= 0
<S>  New C4:  element(domainname, [1]) <= 2147483647
-S-  Applied substitution rule create_nxdom_rules(120).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
<S>  New C6:  true
***  Proved C6:  true
-S-  Applied substitution rule create_nxdom_rules(1).
     This was achieved by replacing all occurrences of dns_types__packet_size 
          by:
          8192.
<S>  New H1:  start_byte <= 8192
-S-  Applied substitution rule create_nxdom_rules(2).
     This was achieved by replacing all occurrences of dns_types__header_bits 
          by:
          96.
<S>  New H24:  start_byte + 12 >= dns_types__packet_length_range__first
<S>  New H25:  start_byte + 12 <= dns_types__packet_length_range__last
<S>  New H28:  start_byte + 12 >= dns_types__packet_bytes_range__base__first
<S>  New H29:  start_byte + 12 <= dns_types__packet_bytes_range__base__last
<S>  New H30:  12 >= dns_types__packet_bytes_range__first
<S>  New H31:  12 <= dns_types__packet_bytes_range__last
<S>  New H32:  12 >= system__min_int
<S>  New H33:  12 <= system__max_int
<S>  New C1:  start_byte >= - 12
<S>  New C2:  start_byte <= 16371
-S-  Applied substitution rule create_nxdom_rules(4).
     This was achieved by replacing all occurrences of system__min_int by:
          - 9223372036854775808.
<S>  New H32:  true
-S-  Applied substitution rule create_nxdom_rules(5).
     This was achieved by replacing all occurrences of system__max_int by:
          9223372036854775807.
<S>  New H33:  true
-S-  Applied substitution rule create_nxdom_rules(12).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(domainname, [i___1]) and element(domainname, [i___1]) <= 
          character__last)
-S-  Applied substitution rule create_nxdom_rules(13).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(domainname, [i___1]) and element(domainname, [i___1]) <= 255)
-S-  Applied substitution rule create_nxdom_rules(33).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__first by:
          0.
<S>  New H24:  start_byte >= - 12
-S-  Applied substitution rule create_nxdom_rules(34).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__last by:
          8192.
<S>  New H25:  start_byte <= 8180
-S-  Applied substitution rule create_nxdom_rules(38).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H2:  start_byte >= 1
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
<S>  New H30:  true
-S-  Applied substitution rule create_nxdom_rules(39).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H3:  start_byte <= 8180
<S>  New H31:  true
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(40).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__first by:
          - 2147483648.
<S>  New H28:  start_byte >= - 2147483660
-S-  Applied substitution rule create_nxdom_rules(41).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__last by:
          2147483647.
<S>  New H29:  start_byte <= 2147483635
-S-  Applied substitution rule create_nxdom_rules(44).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(45).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= 255)
-S-  Applied substitution rule create_nxdom_rules(51).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H7:  fld_messageid(fld_header(output_packet)) >= 0
<S>  New H13:  fld_qdcount(fld_header(output_packet)) >= 0
<S>  New H15:  fld_ancount(fld_header(output_packet)) >= 0
<S>  New H17:  fld_nscount(fld_header(output_packet)) >= 0
<S>  New H19:  fld_arcount(fld_header(output_packet)) >= 0
<S>  New H37:  true
-S-  Applied substitution rule create_nxdom_rules(52).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H8:  fld_messageid(fld_header(output_packet)) <= 65535
<S>  New H14:  fld_qdcount(fld_header(output_packet)) <= 65535
<S>  New H16:  fld_ancount(fld_header(output_packet)) <= 65535
<S>  New H18:  fld_nscount(fld_header(output_packet)) <= 65535
<S>  New H20:  fld_arcount(fld_header(output_packet)) <= 65535
<S>  New H38:  true
-S-  Applied substitution rule create_nxdom_rules(57).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__first by:
          dns_types__query.
<S>  New H9:  dns_types__query <= fld_opcode(fld_header(output_packet))
-S-  Applied substitution rule create_nxdom_rules(58).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__last by:
          dns_types__status.
<S>  New H10:  fld_opcode(fld_header(output_packet)) <= dns_types__status
-S-  Applied substitution rule create_nxdom_rules(83).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H11:  dns_types__no_error <= fld_rcode(fld_header(output_packet))
<S>  New H35:  true
-S-  Applied substitution rule create_nxdom_rules(84).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H12:  fld_rcode(fld_header(output_packet)) <= dns_types__refused
<S>  New H36:  true
***  Proved C3:  element(domainname, [1]) >= 0
     using hypothesis H4.
***  Proved C4:  element(domainname, [1]) <= 2147483647
     using hypothesis H4.
***  Proved C1:  start_byte >= - 12
     using hypothesis H24.
***  Proved C2:  start_byte <= 16371
     using hypothesis H1.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_6.  @@@@@@@@@@
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(current_name, [i___1]) and element(
          current_name, [i___1]) <= character__last)
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
%%%  Simplified H33 on reading formula in, to give:
     %%%  H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(trimmed_name__1, [i___1]) and element(
          trimmed_name__1, [i___1]) <= character__last)
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H42).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H48 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H26).
%%%  Simplified H56 on reading formula in, to give:
     %%%  H56:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__2))
%%%  Simplified H58 on reading formula in, to give:
     %%%  H58:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__2))
%%%  Simplified H68 on reading formula in, to give:
     %%%  H68:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet__2), [i___1]
          ) and element(fld_bytes(output_packet__2), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H79 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H80 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H81 has been replaced by "true".  (It is already present, as 
          H35).
%%%  Simplified H90 on reading formula in, to give:
     %%%  H90:  true
---  Hypothesis H92 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H93 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H94 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H95 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H96 has been replaced by "true".  (It is already present, as 
          H84).
---  Hypothesis H97 has been replaced by "true".  (It is already present, as 
          H85).
---  Hypothesis H98 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H99 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H100 has been replaced by "true".  (It is already present, as 
          H35).
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  true
***  Proved C5:  true
***  Proved C6:  rr_type__wirestringtypeindex__first <= 
          rr_type__wirestringtypeindex__last
     using hypothesis H91.
-S-  Applied substitution rule create_nxdom_rules(27).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__first by:
          0.
<S>  New H9:  qname_location >= 0
<S>  New H28:  current_qname_location >= 0
<S>  New H34:  new_qname_location__1 >= 0
<S>  New C1:  output_bytes__2 >= 0
-S-  Applied substitution rule create_nxdom_rules(28).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__last by:
          16383.
<S>  New H10:  qname_location <= 16383
<S>  New H29:  current_qname_location <= 16383
<S>  New H35:  new_qname_location__1 <= 16383
<S>  New C2:  output_bytes__2 <= 16383
-S-  Applied substitution rule create_nxdom_rules(17).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H82:  amount_trimmed >= 0
<S>  New H84:  amount_trimmed + (element(domainname, [
          rr_type__wirestringtypeindex__first]) + 1) >= 0
<S>  New H86:  element(domainname, [rr_type__wirestringtypeindex__first]) >= - 1
<S>  New C3:  element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) 
          >= 0
-S-  Applied substitution rule create_nxdom_rules(18).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H83:  amount_trimmed <= 2147483647
<S>  New H85:  amount_trimmed + (element(domainname, [
          rr_type__wirestringtypeindex__first]) + 1) <= 2147483647
<S>  New H87:  element(domainname, [rr_type__wirestringtypeindex__first]) <= 
          2147483646
<S>  New C4:  element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) 
          <= 2147483647
-S-  Applied substitution rule create_nxdom_rules(1).
     This was achieved by replacing all occurrences of dns_types__packet_size 
          by:
          8192.
<S>  New H26:  start_byte <= 8192
<S>  New H52:  output_bytes__2 <= 8192
-S-  Applied substitution rule create_nxdom_rules(2).
     This was achieved by replacing all occurrences of dns_types__header_bits 
          by:
          96.
<S>  New H51:  output_bytes__2 >= 13
-S-  Applied substitution rule create_nxdom_rules(3).
     This was achieved by replacing all occurrences of rr_type__maxnumrecords 
          by:
          64.
<S>  New H50:  answer_count <= dns_types__unsigned_short__last - 64
<S>  New H53:  answer_count__2 <= answer_count + 64
-S-  Applied substitution rule create_nxdom_rules(4).
     This was achieved by replacing all occurrences of system__min_int by:
          - 9223372036854775808.
<S>  New H88:  element(domainname, [rr_type__wirestringtypeindex__first]) >= - 
          9223372036854775809
-S-  Applied substitution rule create_nxdom_rules(5).
     This was achieved by replacing all occurrences of system__max_int by:
          9223372036854775807.
<S>  New H89:  element(domainname, [rr_type__wirestringtypeindex__first]) <= 
          9223372036854775806
-S-  Applied substitution rule create_nxdom_rules(12).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 
          character__last)
<S>  New H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          current_name, [i___1]) and element(current_name, [i___1]) <= 
          character__last)
<S>  New H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          trimmed_name__1, [i___1]) and element(trimmed_name__1, [i___1]) <= 
          character__last)
-S-  Applied substitution rule create_nxdom_rules(13).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 255)
<S>  New H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          current_name, [i___1]) and element(current_name, [i___1]) <= 255)
<S>  New H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          trimmed_name__1, [i___1]) and element(trimmed_name__1, [i___1]) <= 
          255)
-S-  Applied substitution rule create_nxdom_rules(33).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__first by:
          0.
<S>  New H71:  output_bytes__2 >= 0
-S-  Applied substitution rule create_nxdom_rules(34).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__last by:
          8192.
<S>  New H4:  output_bytes <= 8192
<S>  New H32:  current_qname_location <= 8192
<S>  New H72:  output_bytes__2 <= 8192
-S-  Applied substitution rule create_nxdom_rules(38).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H6:  start_byte >= 1
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
<S>  New H68:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(output_packet__2), [i___1]) and element(fld_bytes(
          output_packet__2), [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(39).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H7:  start_byte <= 8180
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
<S>  New H68:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(output_packet__2), [i___1]
          ) and element(fld_bytes(output_packet__2), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(44).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
<S>  New H68:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet__2), [i___1]) and element(fld_bytes(
          output_packet__2), [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(45).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= 255)
<S>  New H68:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet__2), [i___1]) and element(fld_bytes(
          output_packet__2), [i___1]) <= 255)
-S-  Applied substitution rule create_nxdom_rules(51).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H11:  fld_messageid(fld_header(output_packet)) >= 0
<S>  New H17:  fld_qdcount(fld_header(output_packet)) >= 0
<S>  New H19:  fld_ancount(fld_header(output_packet)) >= 0
<S>  New H21:  fld_nscount(fld_header(output_packet)) >= 0
<S>  New H23:  fld_arcount(fld_header(output_packet)) >= 0
<S>  New H41:  answer_count >= 0
<S>  New H54:  fld_messageid(fld_header(output_packet__2)) >= 0
<S>  New H60:  fld_qdcount(fld_header(output_packet__2)) >= 0
<S>  New H62:  fld_ancount(fld_header(output_packet__2)) >= 0
<S>  New H64:  fld_nscount(fld_header(output_packet__2)) >= 0
<S>  New H66:  fld_arcount(fld_header(output_packet__2)) >= 0
<S>  New H69:  answer_count__2 >= 0
-S-  Applied substitution rule create_nxdom_rules(52).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H12:  fld_messageid(fld_header(output_packet)) <= 65535
<S>  New H18:  fld_qdcount(fld_header(output_packet)) <= 65535
<S>  New H20:  fld_ancount(fld_header(output_packet)) <= 65535
<S>  New H22:  fld_nscount(fld_header(output_packet)) <= 65535
<S>  New H24:  fld_arcount(fld_header(output_packet)) <= 65535
<S>  New H42:  answer_count <= 65535
<S>  New H55:  fld_messageid(fld_header(output_packet__2)) <= 65535
<S>  New H61:  fld_qdcount(fld_header(output_packet__2)) <= 65535
<S>  New H63:  fld_ancount(fld_header(output_packet__2)) <= 65535
<S>  New H65:  fld_nscount(fld_header(output_packet__2)) <= 65535
<S>  New H67:  fld_arcount(fld_header(output_packet__2)) <= 65535
<S>  New H70:  answer_count__2 <= 65535
<S>  New H50:  answer_count <= 65471
-S-  Applied substitution rule create_nxdom_rules(57).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__first by:
          dns_types__query.
<S>  New H13:  dns_types__query <= fld_opcode(fld_header(output_packet))
<S>  New H56:  dns_types__query <= fld_opcode(fld_header(output_packet__2))
-S-  Applied substitution rule create_nxdom_rules(58).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__last by:
          dns_types__status.
<S>  New H14:  fld_opcode(fld_header(output_packet)) <= dns_types__status
<S>  New H57:  fld_opcode(fld_header(output_packet__2)) <= dns_types__status
-S-  Applied substitution rule create_nxdom_rules(83).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H15:  dns_types__no_error <= fld_rcode(fld_header(output_packet))
<S>  New H58:  dns_types__no_error <= fld_rcode(fld_header(output_packet__2))
-S-  Applied substitution rule create_nxdom_rules(84).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H16:  fld_rcode(fld_header(output_packet)) <= dns_types__refused
<S>  New H59:  fld_rcode(fld_header(output_packet__2)) <= dns_types__refused
-S-  Applied substitution rule create_nxdom_rules(119).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H84:  amount_trimmed + (element(domainname, [1]) + 1) >= 0
<S>  New H85:  amount_trimmed + (element(domainname, [1]) + 1) <= 2147483647
<S>  New H86:  element(domainname, [1]) >= - 1
<S>  New H87:  element(domainname, [1]) <= 2147483646
<S>  New H91:  1 <= rr_type__wirestringtypeindex__last
<S>  New H88:  element(domainname, [1]) >= - 9223372036854775809
<S>  New H89:  element(domainname, [1]) <= 9223372036854775806
<S>  New H8:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(domainname, [i___1]
          ) and element(domainname, [i___1]) <= 255)
<S>  New H27:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(current_name, [
          i___1]) and element(current_name, [i___1]) <= 255)
<S>  New H33:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(trimmed_name__1, [
          i___1]) and element(trimmed_name__1, [i___1]) <= 255)
<S>  New C3:  element(trimmed_name__1, [1]) >= 0
<S>  New C4:  element(trimmed_name__1, [1]) <= 2147483647
-S-  Applied substitution rule create_nxdom_rules(120).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H3:  amount_trimmed < 129
<S>  New H91:  true
<S>  New H8:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(domainname, [i___1]) and element(domainname, [i___1]) <= 255)
<S>  New H27:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(current_name, [i___1]) and element(current_name, [i___1]) <= 
          255)
<S>  New H33:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(trimmed_name__1, [i___1]) and element(trimmed_name__1, [i___1]
          ) <= 255)
***  Proved C1:  output_bytes__2 >= 0
     using hypothesis H71.
***  Proved C2:  output_bytes__2 <= 16383
     using hypothesis H52.
***  Proved C3:  element(trimmed_name__1, [1]) >= 0
     using hypothesis H33.
***  Proved C4:  element(trimmed_name__1, [1]) <= 2147483647
     using hypothesis H33.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_7.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H23 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H25).
%%%  Simplified H34 on reading formula in, to give:
     %%%  H34:  true
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__response_code__first <= dns_types__name_error
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H46 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H47 has been replaced by "true".  (It is already present, as H6)
          .
%%%  Simplified H52 on reading formula in, to give:
     %%%  H52:  true
%%%  Simplified H54 on reading formula in, to give:
     %%%  H54:  true
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  true
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  true
%%%  Simplified C8 on reading formula in, to give:
     %%%  C8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified C11 on reading formula in, to give:
     %%%  C11:  fld_messageid(fld_header(output_packet)) >= 
          dns_types__unsigned_short__first
%%%  Simplified C12 on reading formula in, to give:
     %%%  C12:  fld_messageid(fld_header(output_packet)) <= 
          dns_types__unsigned_short__last
%%%  Simplified C13 on reading formula in, to give:
     %%%  C13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified C14 on reading formula in, to give:
     %%%  C14:  fld_opcode(fld_header(output_packet)) <= 
          dns_types__opcode_type__last
%%%  Simplified C15 on reading formula in, to give:
     %%%  C15:  dns_types__response_code__first <= dns_types__name_error
%%%  Simplified C16 on reading formula in, to give:
     %%%  C16:  dns_types__name_error <= dns_types__response_code__last
%%%  Simplified C17 on reading formula in, to give:
     %%%  C17:  fld_qdcount(fld_header(output_packet)) >= 
          dns_types__unsigned_short__first
%%%  Simplified C18 on reading formula in, to give:
     %%%  C18:  fld_qdcount(fld_header(output_packet)) <= 
          dns_types__unsigned_short__last
%%%  Simplified C19 on reading formula in, to give:
     %%%  C19:  0 >= dns_types__unsigned_short__first
%%%  Simplified C20 on reading formula in, to give:
     %%%  C20:  0 <= dns_types__unsigned_short__last
%%%  Simplified C21 on reading formula in, to give:
     %%%  C21:  fld_nscount(fld_header(output_packet)) >= 
          dns_types__unsigned_short__first
%%%  Simplified C22 on reading formula in, to give:
     %%%  C22:  fld_nscount(fld_header(output_packet)) <= 
          dns_types__unsigned_short__last
%%%  Simplified C23 on reading formula in, to give:
     %%%  C23:  fld_arcount(fld_header(output_packet)) >= 
          dns_types__unsigned_short__first
%%%  Simplified C24 on reading formula in, to give:
     %%%  C24:  fld_arcount(fld_header(output_packet)) <= 
          dns_types__unsigned_short__last
%%%  Simplified C25 on reading formula in, to give:
     %%%  C25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
***  Proved C1:  true
***  Proved C2:  true
***  Proved C3:  0 < rr_type__wirestringtypeindex__last
     using hypothesis H55.
***  Proved C4:  start_byte + dns_types__header_bits div 8 <= 
          dns_types__packet_length_range__last
     using hypothesis H25.
***  Proved C5:  qname_location <= start_byte + dns_types__header_bits div 8
     using hypothesis H57.
***  Proved C6:  start_byte >= dns_types__packet_bytes_range__first
     using hypothesis H2.
***  Proved C7:  start_byte <= dns_types__packet_bytes_range__last
     using hypothesis H3.
***  Proved C8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first 
          <= i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
     using hypothesis H4.
***  Proved C9:  qname_location >= dns_types__qname_ptr_range__first
     using hypothesis H5.
***  Proved C10:  qname_location <= dns_types__qname_ptr_range__last
     using hypothesis H6.
***  Proved C11:  fld_messageid(fld_header(output_packet)) >= 
          dns_types__unsigned_short__first
     using hypothesis H7.
***  Proved C12:  fld_messageid(fld_header(output_packet)) <= 
          dns_types__unsigned_short__last
     using hypothesis H8.
***  Proved C13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
     using hypothesis H9.
***  Proved C14:  fld_opcode(fld_header(output_packet)) <= 
          dns_types__opcode_type__last
     using hypothesis H10.
***  Proved C15:  dns_types__response_code__first <= dns_types__name_error
     using hypothesis H35.
***  Proved C16:  dns_types__name_error <= dns_types__response_code__last
     using hypothesis H36.
***  Proved C17:  fld_qdcount(fld_header(output_packet)) >= 
          dns_types__unsigned_short__first
     using hypothesis H13.
***  Proved C18:  fld_qdcount(fld_header(output_packet)) <= 
          dns_types__unsigned_short__last
     using hypothesis H14.
***  Proved C19:  0 >= dns_types__unsigned_short__first
     using hypothesis H37.
***  Proved C20:  0 <= dns_types__unsigned_short__last
     using hypothesis H38.
***  Proved C21:  fld_nscount(fld_header(output_packet)) >= 
          dns_types__unsigned_short__first
     using hypothesis H17.
***  Proved C22:  fld_nscount(fld_header(output_packet)) <= 
          dns_types__unsigned_short__last
     using hypothesis H18.
***  Proved C23:  fld_arcount(fld_header(output_packet)) >= 
          dns_types__unsigned_short__first
     using hypothesis H19.
***  Proved C24:  fld_arcount(fld_header(output_packet)) <= 
          dns_types__unsigned_short__last
     using hypothesis H20.
***  Proved C25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
     using hypothesis H21.
***  Proved C26:  start_byte <= dns_types__packet_size
     using hypothesis H1.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_8.  @@@@@@@@@@
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(current_name, [i___1]) and element(
          current_name, [i___1]) <= character__last)
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
%%%  Simplified H33 on reading formula in, to give:
     %%%  H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(trimmed_name__1, [i___1]) and element(
          trimmed_name__1, [i___1]) <= character__last)
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H42).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H48 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H26).
%%%  Simplified H56 on reading formula in, to give:
     %%%  H56:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__2))
%%%  Simplified H58 on reading formula in, to give:
     %%%  H58:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__2))
%%%  Simplified H68 on reading formula in, to give:
     %%%  H68:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet__2), [i___1]
          ) and element(fld_bytes(output_packet__2), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H79 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H80 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H81 has been replaced by "true".  (It is already present, as 
          H35).
%%%  Simplified H90 on reading formula in, to give:
     %%%  H90:  true
---  Hypothesis H92 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H93 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H94 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H95 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H96 has been replaced by "true".  (It is already present, as 
          H84).
---  Hypothesis H97 has been replaced by "true".  (It is already present, as 
          H85).
---  Hypothesis H98 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H99 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H100 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H105 has been replaced by "true".  (It is already present, as 
          H90).
---  Hypothesis H106 has been replaced by "true".  (It is already present, as 
          H91).
%%%  Simplified C8 on reading formula in, to give:
     %%%  C8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified C13 on reading formula in, to give:
     %%%  C13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__2))
%%%  Simplified C15 on reading formula in, to give:
     %%%  C15:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__2))
%%%  Simplified C25 on reading formula in, to give:
     %%%  C25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet__2), [i___1]
          ) and element(fld_bytes(output_packet__2), [i___1]) <= 
          dns_types__byte__last)
***  Proved C1:  answer_count__2 = 0
     using hypothesis H107.
***  Proved C3:  amount_trimmed + (element(domainname, [
          rr_type__wirestringtypeindex__first]) + 1) < 
          rr_type__wirestringtypeindex__last
     using hypothesis H108.
***  Proved C4:  output_bytes__2 <= dns_types__packet_length_range__last
     using hypothesis H72.
***  Proved C5:  new_qname_location__1 <= output_bytes__2
     using hypothesis H110.
***  Proved C6:  start_byte >= dns_types__packet_bytes_range__first
     using hypothesis H6.
***  Proved C7:  start_byte <= dns_types__packet_bytes_range__last
     using hypothesis H7.
***  Proved C8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first 
          <= i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
     using hypothesis H8.
***  Proved C9:  qname_location >= dns_types__qname_ptr_range__first
     using hypothesis H9.
***  Proved C10:  qname_location <= dns_types__qname_ptr_range__last
     using hypothesis H10.
***  Proved C11:  fld_messageid(fld_header(output_packet__2)) >= 
          dns_types__unsigned_short__first
     using hypothesis H54.
***  Proved C12:  fld_messageid(fld_header(output_packet__2)) <= 
          dns_types__unsigned_short__last
     using hypothesis H55.
***  Proved C13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__2))
     using hypothesis H56.
***  Proved C14:  fld_opcode(fld_header(output_packet__2)) <= 
          dns_types__opcode_type__last
     using hypothesis H57.
***  Proved C15:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__2))
     using hypothesis H58.
***  Proved C16:  fld_rcode(fld_header(output_packet__2)) <= 
          dns_types__response_code__last
     using hypothesis H59.
***  Proved C17:  fld_qdcount(fld_header(output_packet__2)) >= 
          dns_types__unsigned_short__first
     using hypothesis H60.
***  Proved C18:  fld_qdcount(fld_header(output_packet__2)) <= 
          dns_types__unsigned_short__last
     using hypothesis H61.
***  Proved C19:  fld_ancount(fld_header(output_packet__2)) >= 
          dns_types__unsigned_short__first
     using hypothesis H62.
***  Proved C20:  fld_ancount(fld_header(output_packet__2)) <= 
          dns_types__unsigned_short__last
     using hypothesis H63.
***  Proved C21:  fld_nscount(fld_header(output_packet__2)) >= 
          dns_types__unsigned_short__first
     using hypothesis H64.
***  Proved C22:  fld_nscount(fld_header(output_packet__2)) <= 
          dns_types__unsigned_short__last
     using hypothesis H65.
***  Proved C23:  fld_arcount(fld_header(output_packet__2)) >= 
          dns_types__unsigned_short__first
     using hypothesis H66.
***  Proved C24:  fld_arcount(fld_header(output_packet__2)) <= 
          dns_types__unsigned_short__last
     using hypothesis H67.
***  Proved C25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet__2), [i___1]
          ) and element(fld_bytes(output_packet__2), [i___1]) <= 
          dns_types__byte__last)
     using hypothesis H68.
***  Proved C26:  start_byte <= dns_types__packet_size
     using hypothesis H26.
-S-  Applied substitution rule create_nxdom_rules(1).
     This was achieved by replacing all occurrences of dns_types__packet_size 
          by:
          8192.
<S>  New H26:  start_byte <= 8192
<S>  New H52:  output_bytes__2 <= 8192
-S-  Applied substitution rule create_nxdom_rules(2).
     This was achieved by replacing all occurrences of dns_types__header_bits 
          by:
          96.
<S>  New H51:  output_bytes__2 >= 13
-S-  Applied substitution rule create_nxdom_rules(3).
     This was achieved by replacing all occurrences of rr_type__maxnumrecords 
          by:
          64.
<S>  New H50:  answer_count <= dns_types__unsigned_short__last - 64
<S>  New H53:  answer_count__2 <= answer_count + 64
-S-  Applied substitution rule create_nxdom_rules(4).
     This was achieved by replacing all occurrences of system__min_int by:
          - 9223372036854775808.
<S>  New H88:  element(domainname, [rr_type__wirestringtypeindex__first]) >= - 
          9223372036854775809
-S-  Applied substitution rule create_nxdom_rules(5).
     This was achieved by replacing all occurrences of system__max_int by:
          9223372036854775807.
<S>  New H89:  element(domainname, [rr_type__wirestringtypeindex__first]) <= 
          9223372036854775806
-S-  Applied substitution rule create_nxdom_rules(12).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 
          character__last)
<S>  New H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          current_name, [i___1]) and element(current_name, [i___1]) <= 
          character__last)
<S>  New H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          trimmed_name__1, [i___1]) and element(trimmed_name__1, [i___1]) <= 
          character__last)
-S-  Applied substitution rule create_nxdom_rules(13).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 255)
<S>  New H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          current_name, [i___1]) and element(current_name, [i___1]) <= 255)
<S>  New H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          trimmed_name__1, [i___1]) and element(trimmed_name__1, [i___1]) <= 
          255)
-S-  Applied substitution rule create_nxdom_rules(17).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H82:  amount_trimmed >= 0
<S>  New H84:  amount_trimmed + (element(domainname, [
          rr_type__wirestringtypeindex__first]) + 1) >= 0
<S>  New H86:  element(domainname, [rr_type__wirestringtypeindex__first]) >= - 1
<S>  New H103:  element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) 
          >= 0
-S-  Applied substitution rule create_nxdom_rules(18).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H83:  amount_trimmed <= 2147483647
<S>  New H85:  amount_trimmed + (element(domainname, [
          rr_type__wirestringtypeindex__first]) + 1) <= 2147483647
<S>  New H87:  element(domainname, [rr_type__wirestringtypeindex__first]) <= 
          2147483646
<S>  New H104:  element(trimmed_name__1, [rr_type__wirestringtypeindex__first]) 
          <= 2147483647
-S-  Applied substitution rule create_nxdom_rules(27).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__first by:
          0.
<S>  New H9:  qname_location >= 0
<S>  New H28:  current_qname_location >= 0
<S>  New H34:  new_qname_location__1 >= 0
<S>  New H101:  output_bytes__2 >= 0
-S-  Applied substitution rule create_nxdom_rules(28).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__last by:
          16383.
<S>  New H10:  qname_location <= 16383
<S>  New H29:  current_qname_location <= 16383
<S>  New H35:  new_qname_location__1 <= 16383
<S>  New H102:  output_bytes__2 <= 16383
-S-  Applied substitution rule create_nxdom_rules(33).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__first by:
          0.
<S>  New H71:  output_bytes__2 >= 0
-S-  Applied substitution rule create_nxdom_rules(34).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__last by:
          8192.
<S>  New H4:  output_bytes <= 8192
<S>  New H32:  current_qname_location <= 8192
<S>  New H72:  output_bytes__2 <= 8192
-S-  Applied substitution rule create_nxdom_rules(38).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H6:  start_byte >= 1
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
<S>  New H68:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(output_packet__2), [i___1]) and element(fld_bytes(
          output_packet__2), [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(39).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H7:  start_byte <= 8180
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
<S>  New H68:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(output_packet__2), [i___1]
          ) and element(fld_bytes(output_packet__2), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(44).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
<S>  New H68:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet__2), [i___1]) and element(fld_bytes(
          output_packet__2), [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(45).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= 255)
<S>  New H68:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet__2), [i___1]) and element(fld_bytes(
          output_packet__2), [i___1]) <= 255)
-S-  Applied substitution rule create_nxdom_rules(51).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H11:  fld_messageid(fld_header(output_packet)) >= 0
<S>  New H17:  fld_qdcount(fld_header(output_packet)) >= 0
<S>  New H19:  fld_ancount(fld_header(output_packet)) >= 0
<S>  New H21:  fld_nscount(fld_header(output_packet)) >= 0
<S>  New H23:  fld_arcount(fld_header(output_packet)) >= 0
<S>  New H41:  answer_count >= 0
<S>  New H54:  fld_messageid(fld_header(output_packet__2)) >= 0
<S>  New H60:  fld_qdcount(fld_header(output_packet__2)) >= 0
<S>  New H62:  fld_ancount(fld_header(output_packet__2)) >= 0
<S>  New H64:  fld_nscount(fld_header(output_packet__2)) >= 0
<S>  New H66:  fld_arcount(fld_header(output_packet__2)) >= 0
<S>  New H69:  answer_count__2 >= 0
-S-  Applied substitution rule create_nxdom_rules(52).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H12:  fld_messageid(fld_header(output_packet)) <= 65535
<S>  New H18:  fld_qdcount(fld_header(output_packet)) <= 65535
<S>  New H20:  fld_ancount(fld_header(output_packet)) <= 65535
<S>  New H22:  fld_nscount(fld_header(output_packet)) <= 65535
<S>  New H24:  fld_arcount(fld_header(output_packet)) <= 65535
<S>  New H42:  answer_count <= 65535
<S>  New H55:  fld_messageid(fld_header(output_packet__2)) <= 65535
<S>  New H61:  fld_qdcount(fld_header(output_packet__2)) <= 65535
<S>  New H63:  fld_ancount(fld_header(output_packet__2)) <= 65535
<S>  New H65:  fld_nscount(fld_header(output_packet__2)) <= 65535
<S>  New H67:  fld_arcount(fld_header(output_packet__2)) <= 65535
<S>  New H70:  answer_count__2 <= 65535
<S>  New H50:  answer_count <= 65471
-S-  Applied substitution rule create_nxdom_rules(57).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__first by:
          dns_types__query.
<S>  New H13:  dns_types__query <= fld_opcode(fld_header(output_packet))
<S>  New H56:  dns_types__query <= fld_opcode(fld_header(output_packet__2))
-S-  Applied substitution rule create_nxdom_rules(58).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__last by:
          dns_types__status.
<S>  New H14:  fld_opcode(fld_header(output_packet)) <= dns_types__status
<S>  New H57:  fld_opcode(fld_header(output_packet__2)) <= dns_types__status
-S-  Applied substitution rule create_nxdom_rules(83).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H15:  dns_types__no_error <= fld_rcode(fld_header(output_packet))
<S>  New H58:  dns_types__no_error <= fld_rcode(fld_header(output_packet__2))
-S-  Applied substitution rule create_nxdom_rules(84).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H16:  fld_rcode(fld_header(output_packet)) <= dns_types__refused
<S>  New H59:  fld_rcode(fld_header(output_packet__2)) <= dns_types__refused
-S-  Applied substitution rule create_nxdom_rules(119).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H91:  1 <= rr_type__wirestringtypeindex__last
<S>  New H108:  amount_trimmed + (element(domainname, [1]) + 1) < 
          rr_type__wirestringtypeindex__last
<S>  New H109:  element(trimmed_name__1, [1]) <> 0
<S>  New H88:  element(domainname, [1]) >= - 9223372036854775809
<S>  New H89:  element(domainname, [1]) <= 9223372036854775806
<S>  New H8:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(domainname, [i___1]
          ) and element(domainname, [i___1]) <= 255)
<S>  New H27:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(current_name, [
          i___1]) and element(current_name, [i___1]) <= 255)
<S>  New H33:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(trimmed_name__1, [
          i___1]) and element(trimmed_name__1, [i___1]) <= 255)
<S>  New H84:  amount_trimmed + (element(domainname, [1]) + 1) >= 0
<S>  New H86:  element(domainname, [1]) >= - 1
<S>  New H103:  element(trimmed_name__1, [1]) >= 0
<S>  New H85:  amount_trimmed + (element(domainname, [1]) + 1) <= 2147483647
<S>  New H87:  element(domainname, [1]) <= 2147483646
<S>  New H104:  element(trimmed_name__1, [1]) <= 2147483647
<S>  New C2:  amount_trimmed + (element(domainname, [1]) + 1) >= 0
-S-  Applied substitution rule create_nxdom_rules(120).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H3:  amount_trimmed < 129
<S>  New H91:  true
<S>  New H108:  amount_trimmed + (element(domainname, [1]) + 1) < 129
<S>  New H8:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(domainname, [i___1]) and element(domainname, [i___1]) <= 255)
<S>  New H27:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(current_name, [i___1]) and element(current_name, [i___1]) <= 
          255)
<S>  New H33:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(trimmed_name__1, [i___1]) and element(trimmed_name__1, [i___1]
          ) <= 255)
%%%  Hypotheses H103 & H109 together imply that
          0 < element(trimmed_name__1, [1]).
     H103 & H109 have therefore been deleted and a new H111 added to this 
          effect.
***  Proved C2:  amount_trimmed + (element(domainname, [1]) + 1) >= 0
     using hypothesis H84.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_9.  @@@@@@@@@@
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(current_name, [i___1]) and element(
          current_name, [i___1]) <= character__last)
***  Proved C1:  current_qname_location >= dns_types__qname_ptr_range__first
     using hypothesis H28.
***  Proved C2:  current_qname_location <= dns_types__qname_ptr_range__last
     using hypothesis H29.
***  Proved C3:  current_qname_location <= dns_types__packet_length_range__last
     using hypotheses H4 & H5.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_10.  @@@@@@@@@@
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(current_name, [i___1]) and element(
          current_name, [i___1]) <= character__last)
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
%%%  Simplified H33 on reading formula in, to give:
     %%%  H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(trimmed_name__1, [i___1]) and element(
          trimmed_name__1, [i___1]) <= character__last)
***  Proved C1:  new_qname_location__1 >= dns_types__qname_ptr_range__first
     using hypothesis H34.
***  Proved C2:  new_qname_location__1 <= dns_types__qname_ptr_range__last
     using hypothesis H35.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_11.  @@@@@@@@@@
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(current_name, [i___1]) and element(
          current_name, [i___1]) <= character__last)
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
%%%  Simplified H33 on reading formula in, to give:
     %%%  H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(trimmed_name__1, [i___1]) and element(
          trimmed_name__1, [i___1]) <= character__last)
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H35).
***  Proved C1:  answer_count >= dns_types__unsigned_short__first
     using hypothesis H41.
***  Proved C2:  answer_count <= dns_types__unsigned_short__last
     using hypothesis H42.
***  Proved C3:  new_qname_location__1 >= dns_types__qname_ptr_range__first
     using hypothesis H34.
***  Proved C4:  new_qname_location__1 <= dns_types__qname_ptr_range__last
     using hypothesis H35.
***  Proved C5:  start_byte >= dns_types__packet_bytes_range__first
     using hypothesis H6.
***  Proved C6:  start_byte <= dns_types__packet_bytes_range__last
     using hypothesis H7.
***  Proved C7:  start_byte <= dns_types__packet_size
     using hypothesis H26.
-S-  Applied substitution rule create_nxdom_rules(1).
     This was achieved by replacing all occurrences of dns_types__packet_size 
          by:
          8192.
<S>  New H26:  start_byte <= 8192
-S-  Applied substitution rule create_nxdom_rules(3).
     This was achieved by replacing all occurrences of rr_type__maxnumrecords 
          by:
          64.
<S>  New C8:  answer_count <= dns_types__unsigned_short__last - 64
-S-  Applied substitution rule create_nxdom_rules(12).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 
          character__last)
<S>  New H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          current_name, [i___1]) and element(current_name, [i___1]) <= 
          character__last)
<S>  New H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          trimmed_name__1, [i___1]) and element(trimmed_name__1, [i___1]) <= 
          character__last)
-S-  Applied substitution rule create_nxdom_rules(13).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 255)
<S>  New H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          current_name, [i___1]) and element(current_name, [i___1]) <= 255)
<S>  New H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          trimmed_name__1, [i___1]) and element(trimmed_name__1, [i___1]) <= 
          255)
-S-  Applied substitution rule create_nxdom_rules(27).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__first by:
          0.
<S>  New H9:  qname_location >= 0
<S>  New H28:  current_qname_location >= 0
<S>  New H34:  new_qname_location__1 >= 0
-S-  Applied substitution rule create_nxdom_rules(28).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__last by:
          16383.
<S>  New H10:  qname_location <= 16383
<S>  New H29:  current_qname_location <= 16383
<S>  New H35:  new_qname_location__1 <= 16383
-S-  Applied substitution rule create_nxdom_rules(34).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__last by:
          8192.
<S>  New H4:  output_bytes <= 8192
<S>  New H32:  current_qname_location <= 8192
-S-  Applied substitution rule create_nxdom_rules(38).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H6:  start_byte >= 1
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(39).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H7:  start_byte <= 8180
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(44).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(45).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= 255)
-S-  Applied substitution rule create_nxdom_rules(51).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H11:  fld_messageid(fld_header(output_packet)) >= 0
<S>  New H17:  fld_qdcount(fld_header(output_packet)) >= 0
<S>  New H19:  fld_ancount(fld_header(output_packet)) >= 0
<S>  New H21:  fld_nscount(fld_header(output_packet)) >= 0
<S>  New H23:  fld_arcount(fld_header(output_packet)) >= 0
<S>  New H41:  answer_count >= 0
-S-  Applied substitution rule create_nxdom_rules(52).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H12:  fld_messageid(fld_header(output_packet)) <= 65535
<S>  New H18:  fld_qdcount(fld_header(output_packet)) <= 65535
<S>  New H20:  fld_ancount(fld_header(output_packet)) <= 65535
<S>  New H22:  fld_nscount(fld_header(output_packet)) <= 65535
<S>  New H24:  fld_arcount(fld_header(output_packet)) <= 65535
<S>  New H42:  answer_count <= 65535
<S>  New C8:  answer_count <= 65471
-S-  Applied substitution rule create_nxdom_rules(57).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__first by:
          dns_types__query.
<S>  New H13:  dns_types__query <= fld_opcode(fld_header(output_packet))
-S-  Applied substitution rule create_nxdom_rules(58).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__last by:
          dns_types__status.
<S>  New H14:  fld_opcode(fld_header(output_packet)) <= dns_types__status
-S-  Applied substitution rule create_nxdom_rules(83).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H15:  dns_types__no_error <= fld_rcode(fld_header(output_packet))
-S-  Applied substitution rule create_nxdom_rules(84).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H16:  fld_rcode(fld_header(output_packet)) <= dns_types__refused
-S-  Applied substitution rule create_nxdom_rules(119).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H8:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(domainname, [i___1]
          ) and element(domainname, [i___1]) <= 255)
<S>  New H27:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(current_name, [
          i___1]) and element(current_name, [i___1]) <= 255)
<S>  New H33:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(trimmed_name__1, [
          i___1]) and element(trimmed_name__1, [i___1]) <= 255)
-S-  Applied substitution rule create_nxdom_rules(120).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H3:  amount_trimmed < 129
<S>  New H8:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(domainname, [i___1]) and element(domainname, [i___1]) <= 255)
<S>  New H27:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(current_name, [i___1]) and element(current_name, [i___1]) <= 
          255)
<S>  New H33:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(trimmed_name__1, [i___1]) and element(trimmed_name__1, [i___1]
          ) <= 255)
***  Proved C8:  answer_count <= 65471
     using hypothesis H1.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_12.  @@@@@@@@@@
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(current_name, [i___1]) and element(
          current_name, [i___1]) <= character__last)
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
%%%  Simplified H33 on reading formula in, to give:
     %%%  H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(trimmed_name__1, [i___1]) and element(
          trimmed_name__1, [i___1]) <= character__last)
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H42).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H48 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H26).
%%%  Simplified H56 on reading formula in, to give:
     %%%  H56:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__2))
%%%  Simplified H58 on reading formula in, to give:
     %%%  H58:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__2))
%%%  Simplified H68 on reading formula in, to give:
     %%%  H68:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet__2), [i___1]
          ) and element(fld_bytes(output_packet__2), [i___1]) <= 
          dns_types__byte__last)
***  Proved C1:  output_bytes__2 >= dns_types__packet_length_range__first
     using hypothesis H71.
***  Proved C2:  output_bytes__2 <= dns_types__packet_length_range__last
     using hypothesis H72.
***  Proved C3:  answer_count__2 >= dns_types__unsigned_short__first
     using hypothesis H69.
***  Proved C4:  answer_count__2 <= dns_types__unsigned_short__last
     using hypothesis H70.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_13.  @@@@@@@@@@
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(current_name, [i___1]) and element(
          current_name, [i___1]) <= character__last)
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
%%%  Simplified H33 on reading formula in, to give:
     %%%  H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(trimmed_name__1, [i___1]) and element(
          trimmed_name__1, [i___1]) <= character__last)
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H42).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H48 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H26).
%%%  Simplified H56 on reading formula in, to give:
     %%%  H56:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__2))
%%%  Simplified H58 on reading formula in, to give:
     %%%  H58:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__2))
%%%  Simplified H68 on reading formula in, to give:
     %%%  H68:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet__2), [i___1]
          ) and element(fld_bytes(output_packet__2), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H79 has been replaced by "true".  (It is already present, as 
          H35).
***  Proved C1:  new_qname_location__1 >= dns_types__qname_ptr_range__first
     using hypothesis H34.
***  Proved C2:  new_qname_location__1 <= dns_types__qname_ptr_range__last
     using hypothesis H35.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_14.  @@@@@@@@@@
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(current_name, [i___1]) and element(
          current_name, [i___1]) <= character__last)
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
%%%  Simplified H33 on reading formula in, to give:
     %%%  H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(trimmed_name__1, [i___1]) and element(
          trimmed_name__1, [i___1]) <= character__last)
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H42).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H48 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H26).
%%%  Simplified H56 on reading formula in, to give:
     %%%  H56:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__2))
%%%  Simplified H58 on reading formula in, to give:
     %%%  H58:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__2))
%%%  Simplified H68 on reading formula in, to give:
     %%%  H68:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet__2), [i___1]
          ) and element(fld_bytes(output_packet__2), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H79 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H80 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H81 has been replaced by "true".  (It is already present, as 
          H35).
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  true
***  Proved C7:  true
-S-  Applied substitution rule create_nxdom_rules(17).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H82:  amount_trimmed >= 0
<S>  New C1:  amount_trimmed + (element(domainname, [
          rr_type__wirestringtypeindex__first]) + 1) >= 0
<S>  New C3:  element(domainname, [rr_type__wirestringtypeindex__first]) >= - 1
-S-  Applied substitution rule create_nxdom_rules(18).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H83:  amount_trimmed <= 2147483647
<S>  New C2:  amount_trimmed + (element(domainname, [
          rr_type__wirestringtypeindex__first]) + 1) <= 2147483647
<S>  New C4:  element(domainname, [rr_type__wirestringtypeindex__first]) <= 
          2147483646
-S-  Applied substitution rule create_nxdom_rules(4).
     This was achieved by replacing all occurrences of system__min_int by:
          - 9223372036854775808.
<S>  New C5:  element(domainname, [rr_type__wirestringtypeindex__first]) >= - 
          9223372036854775809
-S-  Applied substitution rule create_nxdom_rules(5).
     This was achieved by replacing all occurrences of system__max_int by:
          9223372036854775807.
<S>  New C6:  element(domainname, [rr_type__wirestringtypeindex__first]) <= 
          9223372036854775806
-S-  Applied substitution rule create_nxdom_rules(119).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H8:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> character__first <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 
          character__last)
<S>  New H27:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> character__first <= element(
          current_name, [i___1]) and element(current_name, [i___1]) <= 
          character__last)
<S>  New H33:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> character__first <= element(
          trimmed_name__1, [i___1]) and element(trimmed_name__1, [i___1]) <= 
          character__last)
<S>  New C8:  1 <= rr_type__wirestringtypeindex__last
<S>  New C1:  amount_trimmed + (element(domainname, [1]) + 1) >= 0
<S>  New C3:  element(domainname, [1]) >= - 1
<S>  New C2:  amount_trimmed + (element(domainname, [1]) + 1) <= 2147483647
<S>  New C4:  element(domainname, [1]) <= 2147483646
<S>  New C5:  element(domainname, [1]) >= - 9223372036854775809
<S>  New C6:  element(domainname, [1]) <= 9223372036854775806
-S-  Applied substitution rule create_nxdom_rules(120).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H3:  amount_trimmed < 129
<S>  New H8:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
<S>  New H27:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 
          character__first <= element(current_name, [i___1]) and element(
          current_name, [i___1]) <= character__last)
<S>  New H33:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 
          character__first <= element(trimmed_name__1, [i___1]) and element(
          trimmed_name__1, [i___1]) <= character__last)
<S>  New C8:  true
***  Proved C8:  true
-S-  Applied substitution rule create_nxdom_rules(1).
     This was achieved by replacing all occurrences of dns_types__packet_size 
          by:
          8192.
<S>  New H26:  start_byte <= 8192
<S>  New H52:  output_bytes__2 <= 8192
-S-  Applied substitution rule create_nxdom_rules(2).
     This was achieved by replacing all occurrences of dns_types__header_bits 
          by:
          96.
<S>  New H51:  output_bytes__2 >= 13
-S-  Applied substitution rule create_nxdom_rules(3).
     This was achieved by replacing all occurrences of rr_type__maxnumrecords 
          by:
          64.
<S>  New H50:  answer_count <= dns_types__unsigned_short__last - 64
<S>  New H53:  answer_count__2 <= answer_count + 64
-S-  Applied substitution rule create_nxdom_rules(12).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H8:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(domainname, [i___1]) and element(domainname, [i___1]) <= 
          character__last)
<S>  New H27:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(current_name, [i___1]) and element(current_name, [i___1]) <= 
          character__last)
<S>  New H33:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(trimmed_name__1, [i___1]) and element(trimmed_name__1, [i___1]
          ) <= character__last)
-S-  Applied substitution rule create_nxdom_rules(13).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H8:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(domainname, [i___1]) and element(domainname, [i___1]) <= 255)
<S>  New H27:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(current_name, [i___1]) and element(current_name, [i___1]) <= 
          255)
<S>  New H33:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(trimmed_name__1, [i___1]) and element(trimmed_name__1, [i___1]
          ) <= 255)
-S-  Applied substitution rule create_nxdom_rules(27).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__first by:
          0.
<S>  New H9:  qname_location >= 0
<S>  New H28:  current_qname_location >= 0
<S>  New H34:  new_qname_location__1 >= 0
-S-  Applied substitution rule create_nxdom_rules(28).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__last by:
          16383.
<S>  New H10:  qname_location <= 16383
<S>  New H29:  current_qname_location <= 16383
<S>  New H35:  new_qname_location__1 <= 16383
-S-  Applied substitution rule create_nxdom_rules(33).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__first by:
          0.
<S>  New H71:  output_bytes__2 >= 0
-S-  Applied substitution rule create_nxdom_rules(34).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__last by:
          8192.
<S>  New H4:  output_bytes <= 8192
<S>  New H32:  current_qname_location <= 8192
<S>  New H72:  output_bytes__2 <= 8192
-S-  Applied substitution rule create_nxdom_rules(38).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H6:  start_byte >= 1
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
<S>  New H68:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(output_packet__2), [i___1]) and element(fld_bytes(
          output_packet__2), [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(39).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H7:  start_byte <= 8180
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
<S>  New H68:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(output_packet__2), [i___1]
          ) and element(fld_bytes(output_packet__2), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(44).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
<S>  New H68:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet__2), [i___1]) and element(fld_bytes(
          output_packet__2), [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(45).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H25:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= 255)
<S>  New H68:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet__2), [i___1]) and element(fld_bytes(
          output_packet__2), [i___1]) <= 255)
-S-  Applied substitution rule create_nxdom_rules(51).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H11:  fld_messageid(fld_header(output_packet)) >= 0
<S>  New H17:  fld_qdcount(fld_header(output_packet)) >= 0
<S>  New H19:  fld_ancount(fld_header(output_packet)) >= 0
<S>  New H21:  fld_nscount(fld_header(output_packet)) >= 0
<S>  New H23:  fld_arcount(fld_header(output_packet)) >= 0
<S>  New H41:  answer_count >= 0
<S>  New H54:  fld_messageid(fld_header(output_packet__2)) >= 0
<S>  New H60:  fld_qdcount(fld_header(output_packet__2)) >= 0
<S>  New H62:  fld_ancount(fld_header(output_packet__2)) >= 0
<S>  New H64:  fld_nscount(fld_header(output_packet__2)) >= 0
<S>  New H66:  fld_arcount(fld_header(output_packet__2)) >= 0
<S>  New H69:  answer_count__2 >= 0
-S-  Applied substitution rule create_nxdom_rules(52).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H12:  fld_messageid(fld_header(output_packet)) <= 65535
<S>  New H18:  fld_qdcount(fld_header(output_packet)) <= 65535
<S>  New H20:  fld_ancount(fld_header(output_packet)) <= 65535
<S>  New H22:  fld_nscount(fld_header(output_packet)) <= 65535
<S>  New H24:  fld_arcount(fld_header(output_packet)) <= 65535
<S>  New H42:  answer_count <= 65535
<S>  New H55:  fld_messageid(fld_header(output_packet__2)) <= 65535
<S>  New H61:  fld_qdcount(fld_header(output_packet__2)) <= 65535
<S>  New H63:  fld_ancount(fld_header(output_packet__2)) <= 65535
<S>  New H65:  fld_nscount(fld_header(output_packet__2)) <= 65535
<S>  New H67:  fld_arcount(fld_header(output_packet__2)) <= 65535
<S>  New H70:  answer_count__2 <= 65535
<S>  New H50:  answer_count <= 65471
-S-  Applied substitution rule create_nxdom_rules(57).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__first by:
          dns_types__query.
<S>  New H13:  dns_types__query <= fld_opcode(fld_header(output_packet))
<S>  New H56:  dns_types__query <= fld_opcode(fld_header(output_packet__2))
-S-  Applied substitution rule create_nxdom_rules(58).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__last by:
          dns_types__status.
<S>  New H14:  fld_opcode(fld_header(output_packet)) <= dns_types__status
<S>  New H57:  fld_opcode(fld_header(output_packet__2)) <= dns_types__status
-S-  Applied substitution rule create_nxdom_rules(83).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H15:  dns_types__no_error <= fld_rcode(fld_header(output_packet))
<S>  New H58:  dns_types__no_error <= fld_rcode(fld_header(output_packet__2))
-S-  Applied substitution rule create_nxdom_rules(84).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H16:  fld_rcode(fld_header(output_packet)) <= dns_types__refused
<S>  New H59:  fld_rcode(fld_header(output_packet__2)) <= dns_types__refused
***  Proved C3:  element(domainname, [1]) >= - 1
     using hypothesis H8.
***  Proved C4:  element(domainname, [1]) <= 2147483646
     using hypothesis H8.
***  Proved C5:  element(domainname, [1]) >= - 9223372036854775809
     using hypothesis H8.
***  Proved C6:  element(domainname, [1]) <= 9223372036854775806
     using hypothesis H8.
---  Eliminated hypothesis H30 (true-hypothesis).
---  Eliminated hypothesis H31 (true-hypothesis).
---  Eliminated hypothesis H36 (true-hypothesis).
---  Eliminated hypothesis H37 (true-hypothesis).
---  Eliminated hypothesis H38 (true-hypothesis).
---  Eliminated hypothesis H39 (true-hypothesis).
---  Eliminated hypothesis H40 (true-hypothesis).
---  Eliminated hypothesis H43 (true-hypothesis).
---  Eliminated hypothesis H44 (true-hypothesis).
---  Eliminated hypothesis H45 (true-hypothesis).
---  Eliminated hypothesis H46 (true-hypothesis).
---  Eliminated hypothesis H47 (true-hypothesis).
---  Eliminated hypothesis H48 (true-hypothesis).
---  Eliminated hypothesis H49 (true-hypothesis).
---  Eliminated hypothesis H73 (true-hypothesis).
---  Eliminated hypothesis H74 (true-hypothesis).
---  Eliminated hypothesis H75 (true-hypothesis).
---  Eliminated hypothesis H76 (true-hypothesis).
---  Eliminated hypothesis H77 (true-hypothesis).
---  Eliminated hypothesis H78 (true-hypothesis).
---  Eliminated hypothesis H79 (true-hypothesis).
---  Eliminated hypothesis H80 (true-hypothesis).
---  Eliminated hypothesis H81 (true-hypothesis).
---  Eliminated hypothesis H82 (duplicate of H2).
---  Eliminated hypothesis H72 (duplicate of H52).
---  Eliminated hypothesis H26 (redundant, given H7).
---  Eliminated hypothesis H29 (redundant, given H32).
---  Eliminated hypothesis H41 (redundant, given H1).
---  Eliminated hypothesis H42 (redundant, given H1).
---  Eliminated hypothesis H50 (redundant, given H1).
---  Eliminated hypothesis H70 (redundant, given H1 & H53).
---  Eliminated hypothesis H71 (redundant, given H51).
---  Eliminated hypothesis H83 (redundant, given H3).
-S-  Eliminated hypothesis H1.
     This was achieved by replacing all occurrences of answer_count by:
          0.
<S>  New H53:  answer_count__2 <= 64
***  Proved C1:  amount_trimmed + (element(domainname, [1]) + 1) >= 0
     using hypotheses H2 & H8.
***  Proved C2:  amount_trimmed + (element(domainname, [1]) + 1) <= 2147483647
     using hypotheses H3 & H8.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_15.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H23 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H25).
%%%  Simplified H34 on reading formula in, to give:
     %%%  H34:  true
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__response_code__first <= dns_types__name_error
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H46 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H47 has been replaced by "true".  (It is already present, as H6)
          .
%%%  Simplified H52 on reading formula in, to give:
     %%%  H52:  true
%%%  Simplified H54 on reading formula in, to give:
     %%%  H54:  not (0 < rr_type__wirestringtypeindex__last and element(
          domainname, [rr_type__wirestringtypeindex__first]) <> 0 and 
          qname_location <= start_byte + dns_types__header_bits div 8)
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H38).
%%%  Simplified H57 on reading formula in, to give:
     %%%  H57:  false
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H38).
***  Proved C1:  0 >= dns_types__unsigned_short__first
     using hypothesis H37.
***  Proved C2:  0 <= dns_types__unsigned_short__last
     using hypothesis H38.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_16.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H23 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H25).
%%%  Simplified H34 on reading formula in, to give:
     %%%  H34:  true
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__response_code__first <= dns_types__name_error
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H46 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H47 has been replaced by "true".  (It is already present, as H6)
          .
%%%  Simplified H52 on reading formula in, to give:
     %%%  H52:  true
%%%  Simplified H54 on reading formula in, to give:
     %%%  H54:  not (0 < rr_type__wirestringtypeindex__last and element(
          domainname, [rr_type__wirestringtypeindex__first]) <> 0 and 
          qname_location <= start_byte + dns_types__header_bits div 8)
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H38).
%%%  Simplified H57 on reading formula in, to give:
     %%%  H57:  true
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H38).
***  Proved C1:  0 >= dns_types__unsigned_short__first
     using hypothesis H37.
***  Proved C2:  0 <= dns_types__unsigned_short__last
     using hypothesis H38.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_17.  @@@@@@@@@@
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(current_name, [i___1]) and element(
          current_name, [i___1]) <= character__last)
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
%%%  Simplified H33 on reading formula in, to give:
     %%%  H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(trimmed_name__1, [i___1]) and element(
          trimmed_name__1, [i___1]) <= character__last)
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H42).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H48 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H26).
%%%  Simplified H56 on reading formula in, to give:
     %%%  H56:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__2))
%%%  Simplified H58 on reading formula in, to give:
     %%%  H58:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__2))
%%%  Simplified H68 on reading formula in, to give:
     %%%  H68:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet__2), [i___1]
          ) and element(fld_bytes(output_packet__2), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H79 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H80 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H81 has been replaced by "true".  (It is already present, as 
          H35).
%%%  Simplified H90 on reading formula in, to give:
     %%%  H90:  true
---  Hypothesis H92 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H93 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H94 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H95 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H96 has been replaced by "true".  (It is already present, as 
          H84).
---  Hypothesis H97 has been replaced by "true".  (It is already present, as 
          H85).
---  Hypothesis H98 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H99 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H100 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H105 has been replaced by "true".  (It is already present, as 
          H90).
---  Hypothesis H106 has been replaced by "true".  (It is already present, as 
          H91).
---  Hypothesis H108 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H109 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H111 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H112 has been replaced by "true".  (It is already present, as 
          H70).
***  Proved C1:  answer_count__2 >= dns_types__unsigned_short__first
     using hypothesis H69.
***  Proved C2:  answer_count__2 <= dns_types__unsigned_short__last
     using hypothesis H70.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_18.  @@@@@@@@@@
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(current_name, [i___1]) and element(
          current_name, [i___1]) <= character__last)
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
%%%  Simplified H33 on reading formula in, to give:
     %%%  H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(trimmed_name__1, [i___1]) and element(
          trimmed_name__1, [i___1]) <= character__last)
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H42).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H48 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H26).
%%%  Simplified H56 on reading formula in, to give:
     %%%  H56:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__2))
%%%  Simplified H58 on reading formula in, to give:
     %%%  H58:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__2))
%%%  Simplified H68 on reading formula in, to give:
     %%%  H68:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet__2), [i___1]
          ) and element(fld_bytes(output_packet__2), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H79 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H80 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H81 has been replaced by "true".  (It is already present, as 
          H35).
%%%  Simplified H90 on reading formula in, to give:
     %%%  H90:  true
---  Hypothesis H92 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H93 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H94 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H95 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H96 has been replaced by "true".  (It is already present, as 
          H84).
---  Hypothesis H97 has been replaced by "true".  (It is already present, as 
          H85).
---  Hypothesis H98 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H99 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H100 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H105 has been replaced by "true".  (It is already present, as 
          H90).
---  Hypothesis H106 has been replaced by "true".  (It is already present, as 
          H91).
---  Hypothesis H108 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H109 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H111 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H112 has been replaced by "true".  (It is already present, as 
          H70).
***  Proved C1:  answer_count__2 >= dns_types__unsigned_short__first
     using hypothesis H69.
***  Proved C2:  answer_count__2 <= dns_types__unsigned_short__last
     using hypothesis H70.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_19.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H23 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H25).
%%%  Simplified H34 on reading formula in, to give:
     %%%  H34:  true
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__response_code__first <= dns_types__name_error
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H46 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H47 has been replaced by "true".  (It is already present, as H6)
          .
%%%  Simplified H52 on reading formula in, to give:
     %%%  H52:  true
%%%  Simplified H54 on reading formula in, to give:
     %%%  H54:  not (0 < rr_type__wirestringtypeindex__last and element(
          domainname, [rr_type__wirestringtypeindex__first]) <> 0 and 
          qname_location <= start_byte + dns_types__header_bits div 8)
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H38).
%%%  Simplified H57 on reading formula in, to give:
     %%%  H57:  false
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H38).
-S-  Applied substitution rule create_nxdom_rules(1).
     This was achieved by replacing all occurrences of dns_types__packet_size 
          by:
          8192.
<S>  New H1:  start_byte <= 8192
<S>  New C2:  start_byte + dns_types__header_bits div 8 <= 8192
>>>  Restructured hypothesis H54 into:
     >>>  H54:  rr_type__wirestringtypeindex__last <= 0 or element(domainname, [
          rr_type__wirestringtypeindex__first]) = 0 or start_byte + 
          dns_types__header_bits div 8 < qname_location
-S-  Applied substitution rule create_nxdom_rules(2).
     This was achieved by replacing all occurrences of dns_types__header_bits 
          by:
          96.
<S>  New H24:  start_byte + 12 >= dns_types__packet_length_range__first
<S>  New H25:  start_byte + 12 <= dns_types__packet_length_range__last
<S>  New H28:  start_byte + 12 >= dns_types__packet_bytes_range__base__first
<S>  New H29:  start_byte + 12 <= dns_types__packet_bytes_range__base__last
<S>  New H30:  12 >= dns_types__packet_bytes_range__first
<S>  New H31:  12 <= dns_types__packet_bytes_range__last
<S>  New H32:  12 >= system__min_int
<S>  New H33:  12 <= system__max_int
<S>  New H48:  start_byte + 12 >= dns_types__qname_ptr_range__first
<S>  New H49:  start_byte + 12 <= dns_types__qname_ptr_range__last
<S>  New H54:  rr_type__wirestringtypeindex__last <= 0 or element(domainname, [
          rr_type__wirestringtypeindex__first]) = 0 or start_byte + 12 < 
          qname_location
<S>  New C1:  start_byte >= 1
<S>  New C2:  start_byte <= 8180
-S-  Applied substitution rule create_nxdom_rules(4).
     This was achieved by replacing all occurrences of system__min_int by:
          - 9223372036854775808.
<S>  New H32:  true
-S-  Applied substitution rule create_nxdom_rules(5).
     This was achieved by replacing all occurrences of system__max_int by:
          9223372036854775807.
<S>  New H33:  true
-S-  Applied substitution rule create_nxdom_rules(12).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 
          character__last)
-S-  Applied substitution rule create_nxdom_rules(13).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 255)
-S-  Applied substitution rule create_nxdom_rules(17).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H43:  true
<S>  New H50:  element(domainname, [rr_type__wirestringtypeindex__first]) >= 0
-S-  Applied substitution rule create_nxdom_rules(18).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H44:  true
<S>  New H51:  element(domainname, [rr_type__wirestringtypeindex__first]) <= 
          2147483647
-S-  Applied substitution rule create_nxdom_rules(27).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__first by:
          0.
<S>  New H5:  qname_location >= 0
<S>  New H48:  start_byte >= - 12
-S-  Applied substitution rule create_nxdom_rules(28).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__last by:
          16383.
<S>  New H6:  qname_location <= 16383
<S>  New H49:  start_byte <= 16371
-S-  Applied substitution rule create_nxdom_rules(33).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__first by:
          0.
<S>  New H24:  start_byte >= - 12
-S-  Applied substitution rule create_nxdom_rules(34).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__last by:
          8192.
<S>  New H25:  start_byte <= 8180
-S-  Applied substitution rule create_nxdom_rules(38).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H2:  start_byte >= 1
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
<S>  New H30:  true
-S-  Applied substitution rule create_nxdom_rules(39).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H3:  start_byte <= 8180
<S>  New H31:  true
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(40).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__first by:
          - 2147483648.
<S>  New H28:  start_byte >= - 2147483660
-S-  Applied substitution rule create_nxdom_rules(41).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__last by:
          2147483647.
<S>  New H29:  start_byte <= 2147483635
-S-  Applied substitution rule create_nxdom_rules(44).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(45).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= 255)
-S-  Applied substitution rule create_nxdom_rules(51).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H7:  fld_messageid(fld_header(output_packet)) >= 0
<S>  New H13:  fld_qdcount(fld_header(output_packet)) >= 0
<S>  New H15:  fld_ancount(fld_header(output_packet)) >= 0
<S>  New H17:  fld_nscount(fld_header(output_packet)) >= 0
<S>  New H19:  fld_arcount(fld_header(output_packet)) >= 0
<S>  New H37:  true
-S-  Applied substitution rule create_nxdom_rules(52).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H8:  fld_messageid(fld_header(output_packet)) <= 65535
<S>  New H14:  fld_qdcount(fld_header(output_packet)) <= 65535
<S>  New H16:  fld_ancount(fld_header(output_packet)) <= 65535
<S>  New H18:  fld_nscount(fld_header(output_packet)) <= 65535
<S>  New H20:  fld_arcount(fld_header(output_packet)) <= 65535
<S>  New H38:  true
-S-  Applied substitution rule create_nxdom_rules(57).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__first by:
          dns_types__query.
<S>  New H9:  dns_types__query <= fld_opcode(fld_header(output_packet))
-S-  Applied substitution rule create_nxdom_rules(58).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__last by:
          dns_types__status.
<S>  New H10:  fld_opcode(fld_header(output_packet)) <= dns_types__status
-S-  Applied substitution rule create_nxdom_rules(83).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H11:  dns_types__no_error <= fld_rcode(fld_header(output_packet))
<S>  New H35:  true
-S-  Applied substitution rule create_nxdom_rules(84).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H12:  fld_rcode(fld_header(output_packet)) <= dns_types__refused
<S>  New H36:  true
-S-  Applied substitution rule create_nxdom_rules(119).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H53:  1 <= rr_type__wirestringtypeindex__last
<S>  New H54:  rr_type__wirestringtypeindex__last <= 0 or element(domainname, [
          1]) = 0 or start_byte + 12 < qname_location
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(domainname, [i___1]
          ) and element(domainname, [i___1]) <= 255)
<S>  New H50:  element(domainname, [1]) >= 0
<S>  New H51:  element(domainname, [1]) <= 2147483647
-S-  Applied substitution rule create_nxdom_rules(120).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H53:  true
<S>  New H54:  element(domainname, [1]) = 0 or start_byte + 12 < qname_location
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(domainname, [i___1]) and element(domainname, [i___1]) <= 255)
***  Proved C1:  start_byte >= 1
     using hypothesis H2.
***  Proved C2:  start_byte <= 8180
     using hypothesis H25.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_20.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H23 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H25).
%%%  Simplified H34 on reading formula in, to give:
     %%%  H34:  true
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__response_code__first <= dns_types__name_error
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H46 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H47 has been replaced by "true".  (It is already present, as H6)
          .
%%%  Simplified H52 on reading formula in, to give:
     %%%  H52:  true
%%%  Simplified H54 on reading formula in, to give:
     %%%  H54:  not (0 < rr_type__wirestringtypeindex__last and element(
          domainname, [rr_type__wirestringtypeindex__first]) <> 0 and 
          qname_location <= start_byte + dns_types__header_bits div 8)
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H38).
%%%  Simplified H57 on reading formula in, to give:
     %%%  H57:  true
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H38).
-S-  Applied substitution rule create_nxdom_rules(1).
     This was achieved by replacing all occurrences of dns_types__packet_size 
          by:
          8192.
<S>  New H1:  start_byte <= 8192
<S>  New C2:  start_byte + dns_types__header_bits div 8 <= 8192
>>>  Restructured hypothesis H54 into:
     >>>  H54:  rr_type__wirestringtypeindex__last <= 0 or element(domainname, [
          rr_type__wirestringtypeindex__first]) = 0 or start_byte + 
          dns_types__header_bits div 8 < qname_location
-S-  Applied substitution rule create_nxdom_rules(2).
     This was achieved by replacing all occurrences of dns_types__header_bits 
          by:
          96.
<S>  New H24:  start_byte + 12 >= dns_types__packet_length_range__first
<S>  New H25:  start_byte + 12 <= dns_types__packet_length_range__last
<S>  New H28:  start_byte + 12 >= dns_types__packet_bytes_range__base__first
<S>  New H29:  start_byte + 12 <= dns_types__packet_bytes_range__base__last
<S>  New H30:  12 >= dns_types__packet_bytes_range__first
<S>  New H31:  12 <= dns_types__packet_bytes_range__last
<S>  New H32:  12 >= system__min_int
<S>  New H33:  12 <= system__max_int
<S>  New H48:  start_byte + 12 >= dns_types__qname_ptr_range__first
<S>  New H49:  start_byte + 12 <= dns_types__qname_ptr_range__last
<S>  New H54:  rr_type__wirestringtypeindex__last <= 0 or element(domainname, [
          rr_type__wirestringtypeindex__first]) = 0 or start_byte + 12 < 
          qname_location
<S>  New C1:  start_byte >= 1
<S>  New C2:  start_byte <= 8180
-S-  Applied substitution rule create_nxdom_rules(4).
     This was achieved by replacing all occurrences of system__min_int by:
          - 9223372036854775808.
<S>  New H32:  true
-S-  Applied substitution rule create_nxdom_rules(5).
     This was achieved by replacing all occurrences of system__max_int by:
          9223372036854775807.
<S>  New H33:  true
-S-  Applied substitution rule create_nxdom_rules(12).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 
          character__last)
-S-  Applied substitution rule create_nxdom_rules(13).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H4:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 255)
-S-  Applied substitution rule create_nxdom_rules(17).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New H43:  true
<S>  New H50:  element(domainname, [rr_type__wirestringtypeindex__first]) >= 0
-S-  Applied substitution rule create_nxdom_rules(18).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New H44:  true
<S>  New H51:  element(domainname, [rr_type__wirestringtypeindex__first]) <= 
          2147483647
-S-  Applied substitution rule create_nxdom_rules(27).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__first by:
          0.
<S>  New H5:  qname_location >= 0
<S>  New H48:  start_byte >= - 12
-S-  Applied substitution rule create_nxdom_rules(28).
     This was achieved by replacing all occurrences of 
          dns_types__qname_ptr_range__last by:
          16383.
<S>  New H6:  qname_location <= 16383
<S>  New H49:  start_byte <= 16371
-S-  Applied substitution rule create_nxdom_rules(33).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__first by:
          0.
<S>  New H24:  start_byte >= - 12
-S-  Applied substitution rule create_nxdom_rules(34).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__last by:
          8192.
<S>  New H25:  start_byte <= 8180
-S-  Applied substitution rule create_nxdom_rules(38).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H2:  start_byte >= 1
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
<S>  New H30:  true
-S-  Applied substitution rule create_nxdom_rules(39).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H3:  start_byte <= 8180
<S>  New H31:  true
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(40).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__first by:
          - 2147483648.
<S>  New H28:  start_byte >= - 2147483660
-S-  Applied substitution rule create_nxdom_rules(41).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__last by:
          2147483647.
<S>  New H29:  start_byte <= 2147483635
-S-  Applied substitution rule create_nxdom_rules(44).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule create_nxdom_rules(45).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H21:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet), [i___1]) and element(fld_bytes(
          output_packet), [i___1]) <= 255)
-S-  Applied substitution rule create_nxdom_rules(51).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H7:  fld_messageid(fld_header(output_packet)) >= 0
<S>  New H13:  fld_qdcount(fld_header(output_packet)) >= 0
<S>  New H15:  fld_ancount(fld_header(output_packet)) >= 0
<S>  New H17:  fld_nscount(fld_header(output_packet)) >= 0
<S>  New H19:  fld_arcount(fld_header(output_packet)) >= 0
<S>  New H37:  true
-S-  Applied substitution rule create_nxdom_rules(52).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H8:  fld_messageid(fld_header(output_packet)) <= 65535
<S>  New H14:  fld_qdcount(fld_header(output_packet)) <= 65535
<S>  New H16:  fld_ancount(fld_header(output_packet)) <= 65535
<S>  New H18:  fld_nscount(fld_header(output_packet)) <= 65535
<S>  New H20:  fld_arcount(fld_header(output_packet)) <= 65535
<S>  New H38:  true
-S-  Applied substitution rule create_nxdom_rules(57).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__first by:
          dns_types__query.
<S>  New H9:  dns_types__query <= fld_opcode(fld_header(output_packet))
-S-  Applied substitution rule create_nxdom_rules(58).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__last by:
          dns_types__status.
<S>  New H10:  fld_opcode(fld_header(output_packet)) <= dns_types__status
-S-  Applied substitution rule create_nxdom_rules(83).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H11:  dns_types__no_error <= fld_rcode(fld_header(output_packet))
<S>  New H35:  true
-S-  Applied substitution rule create_nxdom_rules(84).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H12:  fld_rcode(fld_header(output_packet)) <= dns_types__refused
<S>  New H36:  true
-S-  Applied substitution rule create_nxdom_rules(119).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H53:  1 <= rr_type__wirestringtypeindex__last
<S>  New H54:  rr_type__wirestringtypeindex__last <= 0 or element(domainname, [
          1]) = 0 or start_byte + 12 < qname_location
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(domainname, [i___1]
          ) and element(domainname, [i___1]) <= 255)
<S>  New H50:  element(domainname, [1]) >= 0
<S>  New H51:  element(domainname, [1]) <= 2147483647
-S-  Applied substitution rule create_nxdom_rules(120).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H53:  true
<S>  New H54:  element(domainname, [1]) = 0 or start_byte + 12 < qname_location
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(domainname, [i___1]) and element(domainname, [i___1]) <= 255)
***  Proved C1:  start_byte >= 1
     using hypothesis H2.
***  Proved C2:  start_byte <= 8180
     using hypothesis H25.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_21.  @@@@@@@@@@
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(current_name, [i___1]) and element(
          current_name, [i___1]) <= character__last)
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
%%%  Simplified H33 on reading formula in, to give:
     %%%  H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(trimmed_name__1, [i___1]) and element(
          trimmed_name__1, [i___1]) <= character__last)
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H42).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H48 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H26).
%%%  Simplified H56 on reading formula in, to give:
     %%%  H56:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__2))
%%%  Simplified H58 on reading formula in, to give:
     %%%  H58:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__2))
%%%  Simplified H68 on reading formula in, to give:
     %%%  H68:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet__2), [i___1]
          ) and element(fld_bytes(output_packet__2), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H79 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H80 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H81 has been replaced by "true".  (It is already present, as 
          H35).
%%%  Simplified H90 on reading formula in, to give:
     %%%  H90:  true
---  Hypothesis H92 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H93 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H94 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H95 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H96 has been replaced by "true".  (It is already present, as 
          H84).
---  Hypothesis H97 has been replaced by "true".  (It is already present, as 
          H85).
---  Hypothesis H98 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H99 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H100 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H105 has been replaced by "true".  (It is already present, as 
          H90).
---  Hypothesis H106 has been replaced by "true".  (It is already present, as 
          H91).
---  Hypothesis H108 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H109 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H111 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H112 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H113 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H114 has been replaced by "true".  (It is already present, as 
          H70).
***  Proved C1:  output_bytes__2 >= dns_types__header_bits div 8 + 1
     using hypothesis H51.
***  Proved C2:  output_bytes__2 <= dns_types__packet_size
     using hypothesis H52.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_create_nxdomain_response_22.  @@@@@@@@@@
%%%  Simplified H8 on reading formula in, to give:
     %%%  H8:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet), [i___1]) 
          and element(fld_bytes(output_packet), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(current_name, [i___1]) and element(
          current_name, [i___1]) <= character__last)
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
%%%  Simplified H33 on reading formula in, to give:
     %%%  H33:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(trimmed_name__1, [i___1]) and element(
          trimmed_name__1, [i___1]) <= character__last)
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H42).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H48 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H26).
%%%  Simplified H56 on reading formula in, to give:
     %%%  H56:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__2))
%%%  Simplified H58 on reading formula in, to give:
     %%%  H58:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__2))
%%%  Simplified H68 on reading formula in, to give:
     %%%  H68:  for_all(i___1 : integer, dns_types__packet_bytes_range__first 
          <= i___1 and i___1 <= dns_types__packet_bytes_range__last -> 
          dns_types__byte__first <= element(fld_bytes(output_packet__2), [i___1]
          ) and element(fld_bytes(output_packet__2), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H79 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H80 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H81 has been replaced by "true".  (It is already present, as 
          H35).
%%%  Simplified H90 on reading formula in, to give:
     %%%  H90:  true
---  Hypothesis H92 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H93 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H94 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H95 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H96 has been replaced by "true".  (It is already present, as 
          H84).
---  Hypothesis H97 has been replaced by "true".  (It is already present, as 
          H85).
---  Hypothesis H98 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H99 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H100 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H105 has been replaced by "true".  (It is already present, as 
          H90).
---  Hypothesis H106 has been replaced by "true".  (It is already present, as 
          H91).
---  Hypothesis H108 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H109 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H111 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H112 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H113 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H114 has been replaced by "true".  (It is already present, as 
          H70).
***  Proved C1:  output_bytes__2 >= dns_types__header_bits div 8 + 1
     using hypothesis H51.
***  Proved C2:  output_bytes__2 <= dns_types__packet_size
     using hypothesis H52.
***  PROVED VC.

