*****************************************************************************
                       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.Process_Request_Tcp






@@@@@@@@@@  VC: procedure_process_request_tcp_1.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__response_code__first <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  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(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
***  Proved C1:  input_bytes__1 >= dns_types__packet_length_range__first
     using hypothesis H20.
***  Proved C2:  input_bytes__1 <= dns_types__packet_length_range__last
     using hypothesis H21.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_process_request_tcp_2.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__response_code__first <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  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(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
***  Proved C1:  input_bytes__1 >= dns_types__packet_length_range__first
     using hypothesis H20.
***  Proved C2:  input_bytes__1 <= dns_types__packet_length_range__last
     using hypothesis H21.
+++  Using "A->B, A |- B" on hypotheses H2 & H24 yields a new hypothesis:
     +++  H25:  input_bytes__1 >= 1 + dns_types__header_bits div 8 and 
          input_bytes__1 <= dns_network__max_query_size
-S-  Applied substitution rule process_requ_rules(3).
     This was achieved by replacing all occurrences of dns_types__header_bits 
          by:
          96.
<S>  New H2:  not failure__1 -> input_bytes__1 >= 13 and input_bytes__1 <= 
          dns_network__max_query_size
<S>  New H25:  input_bytes__1 >= 13 and input_bytes__1 <= 
          dns_network__max_query_size
<S>  New C3:  input_bytes__1 >= 13
-S-  Applied substitution rule process_requ_rules(5).
     This was achieved by replacing all occurrences of 
          dns_network__max_query_size by:
          311.
<S>  New H2:  not failure__1 -> input_bytes__1 >= 13 and input_bytes__1 <= 311
<S>  New H25:  input_bytes__1 >= 13 and input_bytes__1 <= 311
-S-  Applied substitution rule process_requ_rules(40).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__first by:
          0.
<S>  New H20:  input_bytes__1 >= 0
-S-  Applied substitution rule process_requ_rules(41).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__last by:
          8192.
<S>  New H21:  input_bytes__1 <= 8192
-S-  Applied substitution rule process_requ_rules(45).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(fld_rest(input_packet__1)), [i___1]) and element(
          fld_bytes(fld_rest(input_packet__1)), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(46).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(51).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(input_packet__1)), [i___1]) and element(
          fld_bytes(fld_rest(input_packet__1)), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(52).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(input_packet__1)), [i___1]) and element(
          fld_bytes(fld_rest(input_packet__1)), [i___1]) <= 255)
-S-  Applied substitution rule process_requ_rules(58).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H3:  fld_length(input_packet__1) >= 0
<S>  New H5:  fld_messageid(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H11:  fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H13:  fld_ancount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H15:  fld_nscount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H17:  fld_arcount(fld_header(fld_rest(input_packet__1))) >= 0
-S-  Applied substitution rule process_requ_rules(59).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H4:  fld_length(input_packet__1) <= 65535
<S>  New H6:  fld_messageid(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H12:  fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H14:  fld_ancount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H16:  fld_nscount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H18:  fld_arcount(fld_header(fld_rest(input_packet__1))) <= 65535
-S-  Applied substitution rule process_requ_rules(64).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__first by:
          dns_types__query.
<S>  New H7:  dns_types__query <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
-S-  Applied substitution rule process_requ_rules(65).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__last by:
          dns_types__status.
<S>  New H8:  fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
          dns_types__status
-S-  Applied substitution rule process_requ_rules(90).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H9:  dns_types__no_error <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
-S-  Applied substitution rule process_requ_rules(91).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H10:  fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
          dns_types__refused
---  Eliminated hypothesis H1 (true-hypothesis).
---  Eliminated hypothesis H22 (true-hypothesis).
---  Eliminated hypothesis H23 (true-hypothesis).
>>>  Using "A->B, A |- B" on H2, given H24, we simplify the former to:
     >>>  H2:  input_bytes__1 >= 13 and input_bytes__1 <= 311
---  Eliminated hypothesis H24, which only specifies a value for failure__1.
     This is not referred to anywhere else in the VC.
>>>  Hypothesis H2 has now been split into two, giving:
     >>>  H26:  input_bytes__1 >= 13
     >>>  H27:  input_bytes__1 <= 311
---  Attempted addition of new hypothesis:
          input_bytes__1 >= 13
     eliminated: this already exists (as H26).
---  Attempted addition of new hypothesis:
          input_bytes__1 <= 311
     eliminated: this already exists (as H27).
>>>  Hypothesis H25 has now been split into two, giving:
     >>>  H26:  input_bytes__1 >= 13
     >>>  H27:  input_bytes__1 <= 311
***  Proved C4:  input_bytes__1 < 312
     using hypothesis H27.
***  Proved C3:  input_bytes__1 >= 13
     using hypothesis H26.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_process_request_tcp_3.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__response_code__first <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  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(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H21).
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          output_packet__2)))
%%%  Simplified H37 on reading formula in, to give:
     %%%  H37:  dns_types__response_code__first <= fld_rcode(fld_header(
          fld_rest(output_packet__2)))
%%%  Simplified H47 on reading formula in, to give:
     %%%  H47:  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(fld_rest(output_packet__2)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__2)), [i___1]
          ) <= dns_types__byte__last)
***  Proved C1:  max_transmit__2 >= dns_types__packet_length_range__first
     using hypothesis H50.
***  Proved C2:  max_transmit__2 <= dns_types__packet_length_range__last
     using hypothesis H51.
***  Proved C3:  output_bytes__2 >= dns_types__packet_length_range__first
     using hypothesis H48.
***  Proved C4:  output_bytes__2 <= dns_types__packet_length_range__last
     using hypothesis H49.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_process_request_tcp_4.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__response_code__first <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  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(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H21).
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          output_packet__2)))
%%%  Simplified H37 on reading formula in, to give:
     %%%  H37:  dns_types__response_code__first <= fld_rcode(fld_header(
          fld_rest(output_packet__2)))
%%%  Simplified H47 on reading formula in, to give:
     %%%  H47:  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(fld_rest(output_packet__2)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__2)), [i___1]
          ) <= dns_types__byte__last)
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H49).
-S-  Applied substitution rule process_requ_rules(58).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H3:  fld_length(input_packet__1) >= 0
<S>  New H5:  fld_messageid(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H11:  fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H13:  fld_ancount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H15:  fld_nscount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H17:  fld_arcount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H33:  fld_messageid(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H39:  fld_qdcount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H41:  fld_ancount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H43:  fld_nscount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H45:  fld_arcount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New C1:  output_bytes__2 >= 0
<S>  New C3:  output_bytes__2 >= 0
-S-  Applied substitution rule process_requ_rules(59).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H4:  fld_length(input_packet__1) <= 65535
<S>  New H6:  fld_messageid(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H12:  fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H14:  fld_ancount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H16:  fld_nscount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H18:  fld_arcount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H34:  fld_messageid(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H40:  fld_qdcount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H42:  fld_ancount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H44:  fld_nscount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H46:  fld_arcount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New C2:  output_bytes__2 <= 65535
<S>  New C4:  output_bytes__2 <= 65535
+++  Using "A->B, A |- B" on hypotheses H2 & H24 yields a new hypothesis:
     +++  H59:  input_bytes__1 >= 1 + dns_types__header_bits div 8 and 
          input_bytes__1 <= dns_network__max_query_size
-S-  Applied substitution rule process_requ_rules(1).
     This was achieved by replacing all occurrences of 
          system__default_bit_order by:
          system__low_order_first.
<S>  New H58:  true
-S-  Applied substitution rule process_requ_rules(2).
     This was achieved by replacing all occurrences of dns_types__packet_size 
          by:
          8192.
<S>  New H30:  output_bytes__2 <= 8192
<S>  New H31:  max_transmit__2 <= 8192
-S-  Applied substitution rule process_requ_rules(3).
     This was achieved by replacing all occurrences of dns_types__header_bits 
          by:
          96.
<S>  New H2:  not failure__1 -> input_bytes__1 >= 13 and input_bytes__1 <= 
          dns_network__max_query_size
<S>  New H27:  input_bytes__1 >= 13
<S>  New H29:  output_bytes__2 >= 13
<S>  New H59:  input_bytes__1 >= 13 and input_bytes__1 <= 
          dns_network__max_query_size
-S-  Applied substitution rule process_requ_rules(4).
     This was achieved by replacing all occurrences of dns_types__udp_max_size 
          by:
          512.
<S>  New H32:  max_transmit__2 >= 512
-S-  Applied substitution rule process_requ_rules(5).
     This was achieved by replacing all occurrences of 
          dns_network__max_query_size by:
          311.
<S>  New H2:  not failure__1 -> input_bytes__1 >= 13 and input_bytes__1 <= 311
<S>  New H59:  input_bytes__1 >= 13 and input_bytes__1 <= 311
-S-  Applied substitution rule process_requ_rules(40).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__first by:
          0.
<S>  New H20:  input_bytes__1 >= 0
<S>  New H48:  output_bytes__2 >= 0
<S>  New H50:  max_transmit__2 >= 0
-S-  Applied substitution rule process_requ_rules(41).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__last by:
          8192.
<S>  New H21:  input_bytes__1 <= 8192
<S>  New H49:  output_bytes__2 <= 8192
<S>  New H51:  max_transmit__2 <= 8192
-S-  Applied substitution rule process_requ_rules(45).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(fld_rest(input_packet__1)), [i___1]) and element(
          fld_bytes(fld_rest(input_packet__1)), [i___1]) <= 
          dns_types__byte__last)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(fld_rest(output_packet__2)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__2)), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(46).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(fld_rest(output_packet__2)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__2)), [i___1]
          ) <= dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(51).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(input_packet__1)), [i___1]) and element(
          fld_bytes(fld_rest(input_packet__1)), [i___1]) <= 
          dns_types__byte__last)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(output_packet__2)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__2)), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(52).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(input_packet__1)), [i___1]) and element(
          fld_bytes(fld_rest(input_packet__1)), [i___1]) <= 255)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(output_packet__2)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__2)), [i___1]) <= 255)
-S-  Applied substitution rule process_requ_rules(64).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__first by:
          dns_types__query.
<S>  New H7:  dns_types__query <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
<S>  New H35:  dns_types__query <= fld_opcode(fld_header(fld_rest(
          output_packet__2)))
-S-  Applied substitution rule process_requ_rules(65).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__last by:
          dns_types__status.
<S>  New H8:  fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
          dns_types__status
<S>  New H36:  fld_opcode(fld_header(fld_rest(output_packet__2))) <= 
          dns_types__status
-S-  Applied substitution rule process_requ_rules(90).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H9:  dns_types__no_error <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
<S>  New H37:  dns_types__no_error <= fld_rcode(fld_header(fld_rest(
          output_packet__2)))
-S-  Applied substitution rule process_requ_rules(91).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H10:  fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
          dns_types__refused
<S>  New H38:  fld_rcode(fld_header(fld_rest(output_packet__2))) <= 
          dns_types__refused
***  Proved C1:  output_bytes__2 >= 0
     using hypothesis H48.
***  Proved C3:  output_bytes__2 >= 0
     using hypothesis H48.
***  Proved C2:  output_bytes__2 <= 65535
     using hypothesis H30.
***  Proved C4:  output_bytes__2 <= 65535
     using hypothesis H30.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_process_request_tcp_5.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__response_code__first <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  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(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H21).
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          output_packet__2)))
%%%  Simplified H37 on reading formula in, to give:
     %%%  H37:  dns_types__response_code__first <= fld_rcode(fld_header(
          fld_rest(output_packet__2)))
%%%  Simplified H47 on reading formula in, to give:
     %%%  H47:  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(fld_rest(output_packet__2)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__2)), [i___1]
          ) <= dns_types__byte__last)
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H59).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H60).
***  Proved C1:  dns_types__byte_swap_us(output_bytes__2) >= 
          dns_types__unsigned_short__first
     using hypothesis H63.
***  Proved C2:  dns_types__byte_swap_us(output_bytes__2) <= 
          dns_types__unsigned_short__last
     using hypothesis H64.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_process_request_tcp_6.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__response_code__first <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  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(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H21).
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          output_packet__2)))
%%%  Simplified H37 on reading formula in, to give:
     %%%  H37:  dns_types__response_code__first <= fld_rcode(fld_header(
          fld_rest(output_packet__2)))
%%%  Simplified H47 on reading formula in, to give:
     %%%  H47:  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(fld_rest(output_packet__2)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__2)), [i___1]
          ) <= dns_types__byte__last)
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H49).
-S-  Applied substitution rule process_requ_rules(58).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H3:  fld_length(input_packet__1) >= 0
<S>  New H5:  fld_messageid(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H11:  fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H13:  fld_ancount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H15:  fld_nscount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H17:  fld_arcount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H33:  fld_messageid(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H39:  fld_qdcount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H41:  fld_ancount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H43:  fld_nscount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H45:  fld_arcount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New C1:  output_bytes__2 >= 0
<S>  New C3:  output_bytes__2 >= 0
-S-  Applied substitution rule process_requ_rules(59).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H4:  fld_length(input_packet__1) <= 65535
<S>  New H6:  fld_messageid(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H12:  fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H14:  fld_ancount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H16:  fld_nscount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H18:  fld_arcount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H34:  fld_messageid(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H40:  fld_qdcount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H42:  fld_ancount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H44:  fld_nscount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H46:  fld_arcount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New C2:  output_bytes__2 <= 65535
<S>  New C4:  output_bytes__2 <= 65535
>>>  Restructured hypothesis H58 into:
     >>>  H58:  system__default_bit_order <> system__low_order_first
+++  Using "A->B, A |- B" on hypotheses H2 & H24 yields a new hypothesis:
     +++  H59:  input_bytes__1 >= 1 + dns_types__header_bits div 8 and 
          input_bytes__1 <= dns_network__max_query_size
-S-  Applied substitution rule process_requ_rules(1).
     This was achieved by replacing all occurrences of 
          system__default_bit_order by:
          system__low_order_first.
<S>  New H58:  false
-S-  Applied substitution rule process_requ_rules(2).
     This was achieved by replacing all occurrences of dns_types__packet_size 
          by:
          8192.
<S>  New H30:  output_bytes__2 <= 8192
<S>  New H31:  max_transmit__2 <= 8192
-S-  Applied substitution rule process_requ_rules(3).
     This was achieved by replacing all occurrences of dns_types__header_bits 
          by:
          96.
<S>  New H2:  not failure__1 -> input_bytes__1 >= 13 and input_bytes__1 <= 
          dns_network__max_query_size
<S>  New H27:  input_bytes__1 >= 13
<S>  New H29:  output_bytes__2 >= 13
<S>  New H59:  input_bytes__1 >= 13 and input_bytes__1 <= 
          dns_network__max_query_size
-S-  Applied substitution rule process_requ_rules(4).
     This was achieved by replacing all occurrences of dns_types__udp_max_size 
          by:
          512.
<S>  New H32:  max_transmit__2 >= 512
-S-  Applied substitution rule process_requ_rules(5).
     This was achieved by replacing all occurrences of 
          dns_network__max_query_size by:
          311.
<S>  New H2:  not failure__1 -> input_bytes__1 >= 13 and input_bytes__1 <= 311
<S>  New H59:  input_bytes__1 >= 13 and input_bytes__1 <= 311
-S-  Applied substitution rule process_requ_rules(40).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__first by:
          0.
<S>  New H20:  input_bytes__1 >= 0
<S>  New H48:  output_bytes__2 >= 0
<S>  New H50:  max_transmit__2 >= 0
-S-  Applied substitution rule process_requ_rules(41).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__last by:
          8192.
<S>  New H21:  input_bytes__1 <= 8192
<S>  New H49:  output_bytes__2 <= 8192
<S>  New H51:  max_transmit__2 <= 8192
-S-  Applied substitution rule process_requ_rules(45).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(fld_rest(input_packet__1)), [i___1]) and element(
          fld_bytes(fld_rest(input_packet__1)), [i___1]) <= 
          dns_types__byte__last)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(fld_rest(output_packet__2)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__2)), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(46).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(fld_rest(output_packet__2)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__2)), [i___1]
          ) <= dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(51).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(input_packet__1)), [i___1]) and element(
          fld_bytes(fld_rest(input_packet__1)), [i___1]) <= 
          dns_types__byte__last)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(output_packet__2)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__2)), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(52).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(input_packet__1)), [i___1]) and element(
          fld_bytes(fld_rest(input_packet__1)), [i___1]) <= 255)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(output_packet__2)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__2)), [i___1]) <= 255)
-S-  Applied substitution rule process_requ_rules(64).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__first by:
          dns_types__query.
<S>  New H7:  dns_types__query <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
<S>  New H35:  dns_types__query <= fld_opcode(fld_header(fld_rest(
          output_packet__2)))
-S-  Applied substitution rule process_requ_rules(65).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__last by:
          dns_types__status.
<S>  New H8:  fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
          dns_types__status
<S>  New H36:  fld_opcode(fld_header(fld_rest(output_packet__2))) <= 
          dns_types__status
-S-  Applied substitution rule process_requ_rules(90).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H9:  dns_types__no_error <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
<S>  New H37:  dns_types__no_error <= fld_rcode(fld_header(fld_rest(
          output_packet__2)))
-S-  Applied substitution rule process_requ_rules(91).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H10:  fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
          dns_types__refused
<S>  New H38:  fld_rcode(fld_header(fld_rest(output_packet__2))) <= 
          dns_types__refused
***  Proved C1:  output_bytes__2 >= 0
     using hypothesis H48.
***  Proved C3:  output_bytes__2 >= 0
     using hypothesis H48.
***  Proved C2:  output_bytes__2 <= 65535
     using hypothesis H30.
***  Proved C4:  output_bytes__2 <= 65535
     using hypothesis H30.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_process_request_tcp_7.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__response_code__first <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  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(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H21).
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          output_packet__2)))
%%%  Simplified H37 on reading formula in, to give:
     %%%  H37:  dns_types__response_code__first <= fld_rcode(fld_header(
          fld_rest(output_packet__2)))
%%%  Simplified H47 on reading formula in, to give:
     %%%  H47:  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(fld_rest(output_packet__2)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__2)), [i___1]
          ) <= dns_types__byte__last)
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H59).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H60).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H64).
***  Proved C1:  output_bytes__2 >= dns_types__packet_length_range__first
     using hypothesis H48.
***  Proved C2:  output_bytes__2 <= dns_types__packet_length_range__last
     using hypothesis H49.
***  Proved C3:  output_bytes__2 > dns_types__header_bits div 8
     using hypothesis H29.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_process_request_tcp_8.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__response_code__first <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  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(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H21).
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          output_packet__2)))
%%%  Simplified H37 on reading formula in, to give:
     %%%  H37:  dns_types__response_code__first <= fld_rcode(fld_header(
          fld_rest(output_packet__2)))
%%%  Simplified H47 on reading formula in, to give:
     %%%  H47:  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(fld_rest(output_packet__2)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__2)), [i___1]
          ) <= dns_types__byte__last)
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H59).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H60).
***  Proved C1:  output_bytes__2 >= dns_types__packet_length_range__first
     using hypothesis H48.
***  Proved C2:  output_bytes__2 <= dns_types__packet_length_range__last
     using hypothesis H49.
***  Proved C3:  output_bytes__2 > dns_types__header_bits div 8
     using hypothesis H29.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_process_request_tcp_9.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__response_code__first <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  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(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H21).
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          output_packet__2)))
%%%  Simplified H37 on reading formula in, to give:
     %%%  H37:  dns_types__response_code__first <= fld_rcode(fld_header(
          fld_rest(output_packet__2)))
%%%  Simplified H47 on reading formula in, to give:
     %%%  H47:  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(fld_rest(output_packet__2)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__2)), [i___1]
          ) <= dns_types__byte__last)
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H59).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H60).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H49).
%%%  Simplified H75 on reading formula in, to give:
     %%%  H75:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          output_packet__3)))
%%%  Simplified H77 on reading formula in, to give:
     %%%  H77:  dns_types__response_code__first <= fld_rcode(fld_header(
          fld_rest(output_packet__3)))
%%%  Simplified H87 on reading formula in, to give:
     %%%  H87:  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(fld_rest(output_packet__3)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__3)), [i___1]
          ) <= dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(128).
     This was achieved by replacing all occurrences of 
          protected_spark_io_05__number_base__first by:
          2.
<S>  New C1:  true
-S-  Applied substitution rule process_requ_rules(129).
     This was achieved by replacing all occurrences of 
          protected_spark_io_05__number_base__last by:
          16.
<S>  New C2:  true
-S-  Applied substitution rule process_requ_rules(12).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New C3:  true
-S-  Applied substitution rule process_requ_rules(13).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New C4:  true
-S-  Applied substitution rule process_requ_rules(7).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C5:  fld_messageid(fld_header(fld_rest(output_packet__3))) >= - 
          2147483648
<S>  New C7:  fld_messageid(fld_header(fld_rest(output_packet__3))) >= - 
          2147483648
-S-  Applied substitution rule process_requ_rules(8).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C6:  fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
          2147483647
<S>  New C8:  fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
          2147483647
***  Proved C1:  true
***  Proved C2:  true
***  Proved C3:  true
***  Proved C4:  true
+++  Using "A->B, A |- B" on hypotheses H2 & H24 yields a new hypothesis:
     +++  H90:  input_bytes__1 >= 1 + dns_types__header_bits div 8 and 
          input_bytes__1 <= dns_network__max_query_size
-S-  Applied substitution rule process_requ_rules(1).
     This was achieved by replacing all occurrences of 
          system__default_bit_order by:
          system__low_order_first.
<S>  New H58:  true
<S>  New H70:  true
-S-  Applied substitution rule process_requ_rules(2).
     This was achieved by replacing all occurrences of dns_types__packet_size 
          by:
          8192.
<S>  New H30:  output_bytes__2 <= 8192
<S>  New H31:  max_transmit__2 <= 8192
-S-  Applied substitution rule process_requ_rules(3).
     This was achieved by replacing all occurrences of dns_types__header_bits 
          by:
          96.
<S>  New H2:  not failure__1 -> input_bytes__1 >= 13 and input_bytes__1 <= 
          dns_network__max_query_size
<S>  New H27:  input_bytes__1 >= 13
<S>  New H29:  output_bytes__2 >= 13
<S>  New H69:  output_bytes__2 > 12
<S>  New H90:  input_bytes__1 >= 13 and input_bytes__1 <= 
          dns_network__max_query_size
-S-  Applied substitution rule process_requ_rules(4).
     This was achieved by replacing all occurrences of dns_types__udp_max_size 
          by:
          512.
<S>  New H32:  max_transmit__2 >= 512
-S-  Applied substitution rule process_requ_rules(5).
     This was achieved by replacing all occurrences of 
          dns_network__max_query_size by:
          311.
<S>  New H2:  not failure__1 -> input_bytes__1 >= 13 and input_bytes__1 <= 311
<S>  New H90:  input_bytes__1 >= 13 and input_bytes__1 <= 311
-S-  Applied substitution rule process_requ_rules(40).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__first by:
          0.
<S>  New H20:  input_bytes__1 >= 0
<S>  New H48:  output_bytes__2 >= 0
<S>  New H50:  max_transmit__2 >= 0
-S-  Applied substitution rule process_requ_rules(41).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__last by:
          8192.
<S>  New H21:  input_bytes__1 <= 8192
<S>  New H49:  output_bytes__2 <= 8192
<S>  New H51:  max_transmit__2 <= 8192
-S-  Applied substitution rule process_requ_rules(45).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(fld_rest(input_packet__1)), [i___1]) and element(
          fld_bytes(fld_rest(input_packet__1)), [i___1]) <= 
          dns_types__byte__last)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(fld_rest(output_packet__2)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__2)), [i___1]) <= 
          dns_types__byte__last)
<S>  New H87:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(fld_rest(output_packet__3)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__3)), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(46).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(fld_rest(output_packet__2)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__2)), [i___1]
          ) <= dns_types__byte__last)
<S>  New H87:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(fld_rest(output_packet__3)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__3)), [i___1]
          ) <= dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(51).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(input_packet__1)), [i___1]) and element(
          fld_bytes(fld_rest(input_packet__1)), [i___1]) <= 
          dns_types__byte__last)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(output_packet__2)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__2)), [i___1]) <= 
          dns_types__byte__last)
<S>  New H87:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(output_packet__3)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__3)), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(52).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(input_packet__1)), [i___1]) and element(
          fld_bytes(fld_rest(input_packet__1)), [i___1]) <= 255)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(output_packet__2)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__2)), [i___1]) <= 255)
<S>  New H87:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(output_packet__3)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__3)), [i___1]) <= 255)
-S-  Applied substitution rule process_requ_rules(58).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H3:  fld_length(input_packet__1) >= 0
<S>  New H5:  fld_messageid(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H11:  fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H13:  fld_ancount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H15:  fld_nscount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H17:  fld_arcount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H33:  fld_messageid(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H39:  fld_qdcount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H41:  fld_ancount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H43:  fld_nscount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H45:  fld_arcount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H59:  output_bytes__2 >= 0
<S>  New H63:  dns_types__byte_swap_us(output_bytes__2) >= 0
<S>  New H71:  fld_length(output_packet__3) >= 0
<S>  New H73:  fld_messageid(fld_header(fld_rest(output_packet__3))) >= 0
<S>  New H79:  fld_qdcount(fld_header(fld_rest(output_packet__3))) >= 0
<S>  New H81:  fld_ancount(fld_header(fld_rest(output_packet__3))) >= 0
<S>  New H83:  fld_nscount(fld_header(fld_rest(output_packet__3))) >= 0
<S>  New H85:  fld_arcount(fld_header(fld_rest(output_packet__3))) >= 0
-S-  Applied substitution rule process_requ_rules(59).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H4:  fld_length(input_packet__1) <= 65535
<S>  New H6:  fld_messageid(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H12:  fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H14:  fld_ancount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H16:  fld_nscount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H18:  fld_arcount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H34:  fld_messageid(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H40:  fld_qdcount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H42:  fld_ancount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H44:  fld_nscount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H46:  fld_arcount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H60:  output_bytes__2 <= 65535
<S>  New H64:  dns_types__byte_swap_us(output_bytes__2) <= 65535
<S>  New H72:  fld_length(output_packet__3) <= 65535
<S>  New H74:  fld_messageid(fld_header(fld_rest(output_packet__3))) <= 65535
<S>  New H80:  fld_qdcount(fld_header(fld_rest(output_packet__3))) <= 65535
<S>  New H82:  fld_ancount(fld_header(fld_rest(output_packet__3))) <= 65535
<S>  New H84:  fld_nscount(fld_header(fld_rest(output_packet__3))) <= 65535
<S>  New H86:  fld_arcount(fld_header(fld_rest(output_packet__3))) <= 65535
-S-  Applied substitution rule process_requ_rules(64).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__first by:
          dns_types__query.
<S>  New H7:  dns_types__query <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
<S>  New H35:  dns_types__query <= fld_opcode(fld_header(fld_rest(
          output_packet__2)))
<S>  New H75:  dns_types__query <= fld_opcode(fld_header(fld_rest(
          output_packet__3)))
-S-  Applied substitution rule process_requ_rules(65).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__last by:
          dns_types__status.
<S>  New H8:  fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
          dns_types__status
<S>  New H36:  fld_opcode(fld_header(fld_rest(output_packet__2))) <= 
          dns_types__status
<S>  New H76:  fld_opcode(fld_header(fld_rest(output_packet__3))) <= 
          dns_types__status
-S-  Applied substitution rule process_requ_rules(90).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H9:  dns_types__no_error <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
<S>  New H37:  dns_types__no_error <= fld_rcode(fld_header(fld_rest(
          output_packet__2)))
<S>  New H77:  dns_types__no_error <= fld_rcode(fld_header(fld_rest(
          output_packet__3)))
-S-  Applied substitution rule process_requ_rules(91).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H10:  fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
          dns_types__refused
<S>  New H38:  fld_rcode(fld_header(fld_rest(output_packet__2))) <= 
          dns_types__refused
<S>  New H78:  fld_rcode(fld_header(fld_rest(output_packet__3))) <= 
          dns_types__refused
***  Proved C5:  fld_messageid(fld_header(fld_rest(output_packet__3))) >= - 
          2147483648
     using hypothesis H73.
***  Proved C7:  fld_messageid(fld_header(fld_rest(output_packet__3))) >= - 
          2147483648
     using hypothesis H73.
***  Proved C6:  fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
          2147483647
     using hypothesis H74.
***  Proved C8:  fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
          2147483647
     using hypothesis H74.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_process_request_tcp_10.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__response_code__first <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  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(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H21).
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          output_packet__2)))
%%%  Simplified H37 on reading formula in, to give:
     %%%  H37:  dns_types__response_code__first <= fld_rcode(fld_header(
          fld_rest(output_packet__2)))
%%%  Simplified H47 on reading formula in, to give:
     %%%  H47:  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(fld_rest(output_packet__2)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__2)), [i___1]
          ) <= dns_types__byte__last)
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H59).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H60).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H49).
%%%  Simplified H71 on reading formula in, to give:
     %%%  H71:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          output_packet__3)))
%%%  Simplified H73 on reading formula in, to give:
     %%%  H73:  dns_types__response_code__first <= fld_rcode(fld_header(
          fld_rest(output_packet__3)))
%%%  Simplified H83 on reading formula in, to give:
     %%%  H83:  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(fld_rest(output_packet__3)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__3)), [i___1]
          ) <= dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(128).
     This was achieved by replacing all occurrences of 
          protected_spark_io_05__number_base__first by:
          2.
<S>  New C1:  true
-S-  Applied substitution rule process_requ_rules(129).
     This was achieved by replacing all occurrences of 
          protected_spark_io_05__number_base__last by:
          16.
<S>  New C2:  true
-S-  Applied substitution rule process_requ_rules(12).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New C3:  true
-S-  Applied substitution rule process_requ_rules(13).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New C4:  true
-S-  Applied substitution rule process_requ_rules(7).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C5:  fld_messageid(fld_header(fld_rest(output_packet__3))) >= - 
          2147483648
<S>  New C7:  fld_messageid(fld_header(fld_rest(output_packet__3))) >= - 
          2147483648
-S-  Applied substitution rule process_requ_rules(8).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C6:  fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
          2147483647
<S>  New C8:  fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
          2147483647
***  Proved C1:  true
***  Proved C2:  true
***  Proved C3:  true
***  Proved C4:  true
>>>  Restructured hypothesis H58 into:
     >>>  H58:  system__default_bit_order <> system__low_order_first
+++  Using "A->B, A |- B" on hypotheses H2 & H24 yields a new hypothesis:
     +++  H86:  input_bytes__1 >= 1 + dns_types__header_bits div 8 and 
          input_bytes__1 <= dns_network__max_query_size
-S-  Applied substitution rule process_requ_rules(1).
     This was achieved by replacing all occurrences of 
          system__default_bit_order by:
          system__low_order_first.
<S>  New H58:  false
<S>  New H66:  true
-S-  Applied substitution rule process_requ_rules(2).
     This was achieved by replacing all occurrences of dns_types__packet_size 
          by:
          8192.
<S>  New H30:  output_bytes__2 <= 8192
<S>  New H31:  max_transmit__2 <= 8192
-S-  Applied substitution rule process_requ_rules(3).
     This was achieved by replacing all occurrences of dns_types__header_bits 
          by:
          96.
<S>  New H2:  not failure__1 -> input_bytes__1 >= 13 and input_bytes__1 <= 
          dns_network__max_query_size
<S>  New H27:  input_bytes__1 >= 13
<S>  New H29:  output_bytes__2 >= 13
<S>  New H65:  output_bytes__2 > 12
<S>  New H86:  input_bytes__1 >= 13 and input_bytes__1 <= 
          dns_network__max_query_size
-S-  Applied substitution rule process_requ_rules(4).
     This was achieved by replacing all occurrences of dns_types__udp_max_size 
          by:
          512.
<S>  New H32:  max_transmit__2 >= 512
-S-  Applied substitution rule process_requ_rules(5).
     This was achieved by replacing all occurrences of 
          dns_network__max_query_size by:
          311.
<S>  New H2:  not failure__1 -> input_bytes__1 >= 13 and input_bytes__1 <= 311
<S>  New H86:  input_bytes__1 >= 13 and input_bytes__1 <= 311
-S-  Applied substitution rule process_requ_rules(40).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__first by:
          0.
<S>  New H20:  input_bytes__1 >= 0
<S>  New H48:  output_bytes__2 >= 0
<S>  New H50:  max_transmit__2 >= 0
-S-  Applied substitution rule process_requ_rules(41).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__last by:
          8192.
<S>  New H21:  input_bytes__1 <= 8192
<S>  New H49:  output_bytes__2 <= 8192
<S>  New H51:  max_transmit__2 <= 8192
-S-  Applied substitution rule process_requ_rules(45).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(fld_rest(input_packet__1)), [i___1]) and element(
          fld_bytes(fld_rest(input_packet__1)), [i___1]) <= 
          dns_types__byte__last)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(fld_rest(output_packet__2)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__2)), [i___1]) <= 
          dns_types__byte__last)
<S>  New H83:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(fld_rest(output_packet__3)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__3)), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(46).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(fld_rest(output_packet__2)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__2)), [i___1]
          ) <= dns_types__byte__last)
<S>  New H83:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(fld_rest(output_packet__3)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__3)), [i___1]
          ) <= dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(51).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(input_packet__1)), [i___1]) and element(
          fld_bytes(fld_rest(input_packet__1)), [i___1]) <= 
          dns_types__byte__last)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(output_packet__2)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__2)), [i___1]) <= 
          dns_types__byte__last)
<S>  New H83:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(output_packet__3)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__3)), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule process_requ_rules(52).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(input_packet__1)), [i___1]) and element(
          fld_bytes(fld_rest(input_packet__1)), [i___1]) <= 255)
<S>  New H47:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(output_packet__2)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__2)), [i___1]) <= 255)
<S>  New H83:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(fld_rest(output_packet__3)), [i___1]) and element(
          fld_bytes(fld_rest(output_packet__3)), [i___1]) <= 255)
-S-  Applied substitution rule process_requ_rules(58).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H3:  fld_length(input_packet__1) >= 0
<S>  New H5:  fld_messageid(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H11:  fld_qdcount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H13:  fld_ancount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H15:  fld_nscount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H17:  fld_arcount(fld_header(fld_rest(input_packet__1))) >= 0
<S>  New H33:  fld_messageid(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H39:  fld_qdcount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H41:  fld_ancount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H43:  fld_nscount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H45:  fld_arcount(fld_header(fld_rest(output_packet__2))) >= 0
<S>  New H59:  output_bytes__2 >= 0
<S>  New H67:  fld_length(output_packet__3) >= 0
<S>  New H69:  fld_messageid(fld_header(fld_rest(output_packet__3))) >= 0
<S>  New H75:  fld_qdcount(fld_header(fld_rest(output_packet__3))) >= 0
<S>  New H77:  fld_ancount(fld_header(fld_rest(output_packet__3))) >= 0
<S>  New H79:  fld_nscount(fld_header(fld_rest(output_packet__3))) >= 0
<S>  New H81:  fld_arcount(fld_header(fld_rest(output_packet__3))) >= 0
-S-  Applied substitution rule process_requ_rules(59).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H4:  fld_length(input_packet__1) <= 65535
<S>  New H6:  fld_messageid(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H12:  fld_qdcount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H14:  fld_ancount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H16:  fld_nscount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H18:  fld_arcount(fld_header(fld_rest(input_packet__1))) <= 65535
<S>  New H34:  fld_messageid(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H40:  fld_qdcount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H42:  fld_ancount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H44:  fld_nscount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H46:  fld_arcount(fld_header(fld_rest(output_packet__2))) <= 65535
<S>  New H60:  output_bytes__2 <= 65535
<S>  New H68:  fld_length(output_packet__3) <= 65535
<S>  New H70:  fld_messageid(fld_header(fld_rest(output_packet__3))) <= 65535
<S>  New H76:  fld_qdcount(fld_header(fld_rest(output_packet__3))) <= 65535
<S>  New H78:  fld_ancount(fld_header(fld_rest(output_packet__3))) <= 65535
<S>  New H80:  fld_nscount(fld_header(fld_rest(output_packet__3))) <= 65535
<S>  New H82:  fld_arcount(fld_header(fld_rest(output_packet__3))) <= 65535
-S-  Applied substitution rule process_requ_rules(64).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__first by:
          dns_types__query.
<S>  New H7:  dns_types__query <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
<S>  New H35:  dns_types__query <= fld_opcode(fld_header(fld_rest(
          output_packet__2)))
<S>  New H71:  dns_types__query <= fld_opcode(fld_header(fld_rest(
          output_packet__3)))
-S-  Applied substitution rule process_requ_rules(65).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__last by:
          dns_types__status.
<S>  New H8:  fld_opcode(fld_header(fld_rest(input_packet__1))) <= 
          dns_types__status
<S>  New H36:  fld_opcode(fld_header(fld_rest(output_packet__2))) <= 
          dns_types__status
<S>  New H72:  fld_opcode(fld_header(fld_rest(output_packet__3))) <= 
          dns_types__status
-S-  Applied substitution rule process_requ_rules(90).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H9:  dns_types__no_error <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
<S>  New H37:  dns_types__no_error <= fld_rcode(fld_header(fld_rest(
          output_packet__2)))
<S>  New H73:  dns_types__no_error <= fld_rcode(fld_header(fld_rest(
          output_packet__3)))
-S-  Applied substitution rule process_requ_rules(91).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H10:  fld_rcode(fld_header(fld_rest(input_packet__1))) <= 
          dns_types__refused
<S>  New H38:  fld_rcode(fld_header(fld_rest(output_packet__2))) <= 
          dns_types__refused
<S>  New H74:  fld_rcode(fld_header(fld_rest(output_packet__3))) <= 
          dns_types__refused
***  Proved C5:  fld_messageid(fld_header(fld_rest(output_packet__3))) >= - 
          2147483648
     using hypothesis H69.
***  Proved C7:  fld_messageid(fld_header(fld_rest(output_packet__3))) >= - 
          2147483648
     using hypothesis H69.
***  Proved C6:  fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
          2147483647
     using hypothesis H70.
***  Proved C8:  fld_messageid(fld_header(fld_rest(output_packet__3))) <= 
          2147483647
     using hypothesis H70.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_process_request_tcp_11.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__response_code__first <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  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(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H21).
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          output_packet__2)))
%%%  Simplified H37 on reading formula in, to give:
     %%%  H37:  dns_types__response_code__first <= fld_rcode(fld_header(
          fld_rest(output_packet__2)))
%%%  Simplified H47 on reading formula in, to give:
     %%%  H47:  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(fld_rest(output_packet__2)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__2)), [i___1]
          ) <= dns_types__byte__last)
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H59).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H60).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H49).
%%%  Simplified H75 on reading formula in, to give:
     %%%  H75:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          output_packet__3)))
%%%  Simplified H77 on reading formula in, to give:
     %%%  H77:  dns_types__response_code__first <= fld_rcode(fld_header(
          fld_rest(output_packet__3)))
%%%  Simplified H87 on reading formula in, to give:
     %%%  H87:  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(fld_rest(output_packet__3)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__3)), [i___1]
          ) <= dns_types__byte__last)
---  Hypothesis H96 has been replaced by "true".  (It is already present, as 
          H94).
---  Hypothesis H97 has been replaced by "true".  (It is already present, as 
          H95).
***  Proved C1:  0 >= natural__first
     using hypothesis H92.
***  Proved C2:  0 <= natural__last
     using hypothesis H93.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_process_request_tcp_12.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  dns_types__response_code__first <= fld_rcode(fld_header(fld_rest(
          input_packet__1)))
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  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(fld_rest(input_packet__1))
          , [i___1]) and element(fld_bytes(fld_rest(input_packet__1)), [i___1]) 
          <= dns_types__byte__last)
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H21).
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          output_packet__2)))
%%%  Simplified H37 on reading formula in, to give:
     %%%  H37:  dns_types__response_code__first <= fld_rcode(fld_header(
          fld_rest(output_packet__2)))
%%%  Simplified H47 on reading formula in, to give:
     %%%  H47:  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(fld_rest(output_packet__2)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__2)), [i___1]
          ) <= dns_types__byte__last)
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H59).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H60).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H49).
%%%  Simplified H71 on reading formula in, to give:
     %%%  H71:  dns_types__opcode_type__first <= fld_opcode(fld_header(fld_rest(
          output_packet__3)))
%%%  Simplified H73 on reading formula in, to give:
     %%%  H73:  dns_types__response_code__first <= fld_rcode(fld_header(
          fld_rest(output_packet__3)))
%%%  Simplified H83 on reading formula in, to give:
     %%%  H83:  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(fld_rest(output_packet__3)
          ), [i___1]) and element(fld_bytes(fld_rest(output_packet__3)), [i___1]
          ) <= dns_types__byte__last)
---  Hypothesis H92 has been replaced by "true".  (It is already present, as 
          H90).
---  Hypothesis H93 has been replaced by "true".  (It is already present, as 
          H91).
***  Proved C1:  0 >= natural__first
     using hypothesis H88.
***  Proved C2:  0 <= natural__last
     using hypothesis H89.
***  PROVED VC.


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


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


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


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


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

