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

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



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

task_type Udp_Dns_Package.Udp_Dns_Task






@@@@@@@@@@  VC: task_type_udp_dns_task_1.  @@@@@@@@@@
-S-  Applied substitution rule udp_dns_task_rules(55).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule udp_dns_task_rules(56).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


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


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


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


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


@@@@@@@@@@  VC: task_type_udp_dns_task_6.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          input_packet__3))
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__response_code__first <= fld_rcode(fld_header(
          input_packet__3))
%%%  Simplified H17 on reading formula in, to give:
     %%%  H17:  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(input_packet__3), [i___1])
           and element(fld_bytes(input_packet__3), [i___1]) <= 
          dns_types__byte__last)
***  Proved C1:  input_bytes__3 >= dns_types__packet_length_range__first
     using hypothesis H18.
***  Proved C2:  input_bytes__3 <= dns_types__packet_length_range__last
     using hypothesis H19.
***  PROVED VC.


@@@@@@@@@@  VC: task_type_udp_dns_task_7.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          input_packet__3))
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__response_code__first <= fld_rcode(fld_header(
          input_packet__3))
%%%  Simplified H17 on reading formula in, to give:
     %%%  H17:  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(input_packet__3), [i___1])
           and element(fld_bytes(input_packet__3), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
-S-  Applied substitution rule udp_dns_task_rules(16).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule udp_dns_task_rules(17).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: task_type_udp_dns_task_8.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          input_packet__3))
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__response_code__first <= fld_rcode(fld_header(
          input_packet__3))
%%%  Simplified H17 on reading formula in, to give:
     %%%  H17:  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(input_packet__3), [i___1])
           and element(fld_bytes(input_packet__3), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H25 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H30 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H11).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H12).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H19).
%%%  Simplified H43 on reading formula in, to give:
     %%%  H43:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H45 on reading formula in, to give:
     %%%  H45:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H55 on reading formula in, to give:
     %%%  H55:  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:  input_bytes__3 >= dns_types__packet_length_range__first
     using hypothesis H18.
***  Proved C2:  input_bytes__3 <= dns_types__packet_length_range__last
     using hypothesis H19.
+++  Using "A->B, A |- B" on hypotheses H2 & H23 yields a new hypothesis:
     +++  H56:  input_bytes__3 >= 1 + dns_types__header_bits div 8 and 
          input_bytes__3 <= dns_network__max_query_size
-S-  Applied substitution rule udp_dns_task_rules(3).
     This was achieved by replacing all occurrences of dns_types__header_bits 
          by:
          96.
<S>  New H2:  not failure__3 -> input_bytes__3 >= 13 and input_bytes__3 <= 
          dns_network__max_query_size
<S>  New H56:  input_bytes__3 >= 13 and input_bytes__3 <= 
          dns_network__max_query_size
<S>  New C3:  input_bytes__3 >= 13
-S-  Applied substitution rule udp_dns_task_rules(5).
     This was achieved by replacing all occurrences of 
          dns_network__max_query_size by:
          311.
<S>  New H2:  not failure__3 -> input_bytes__3 >= 13 and input_bytes__3 <= 311
<S>  New H56:  input_bytes__3 >= 13 and input_bytes__3 <= 311
-S-  Applied substitution rule udp_dns_task_rules(44).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__first by:
          0.
<S>  New H18:  input_bytes__3 >= 0
-S-  Applied substitution rule udp_dns_task_rules(45).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__last by:
          8192.
<S>  New H19:  input_bytes__3 <= 8192
-S-  Applied substitution rule udp_dns_task_rules(49).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H17:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(input_packet__3), [i___1]) and element(fld_bytes(
          input_packet__3), [i___1]) <= dns_types__byte__last)
<S>  New H55:  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 udp_dns_task_rules(50).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H17:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(input_packet__3), [i___1])
           and element(fld_bytes(input_packet__3), [i___1]) <= 
          dns_types__byte__last)
<S>  New H55:  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 udp_dns_task_rules(55).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H17:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(input_packet__3), [i___1]) and element(fld_bytes(
          input_packet__3), [i___1]) <= dns_types__byte__last)
<S>  New H55:  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 udp_dns_task_rules(56).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H17:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(input_packet__3), [i___1]) and element(fld_bytes(
          input_packet__3), [i___1]) <= 255)
<S>  New H55:  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 udp_dns_task_rules(62).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H3:  fld_messageid(fld_header(input_packet__3)) >= 0
<S>  New H9:  fld_qdcount(fld_header(input_packet__3)) >= 0
<S>  New H11:  fld_ancount(fld_header(input_packet__3)) >= 0
<S>  New H13:  fld_nscount(fld_header(input_packet__3)) >= 0
<S>  New H15:  fld_arcount(fld_header(input_packet__3)) >= 0
<S>  New H41:  fld_messageid(fld_header(output_packet)) >= 0
<S>  New H47:  fld_qdcount(fld_header(output_packet)) >= 0
<S>  New H49:  fld_ancount(fld_header(output_packet)) >= 0
<S>  New H51:  fld_nscount(fld_header(output_packet)) >= 0
<S>  New H53:  fld_arcount(fld_header(output_packet)) >= 0
-S-  Applied substitution rule udp_dns_task_rules(63).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H4:  fld_messageid(fld_header(input_packet__3)) <= 65535
<S>  New H10:  fld_qdcount(fld_header(input_packet__3)) <= 65535
<S>  New H12:  fld_ancount(fld_header(input_packet__3)) <= 65535
<S>  New H14:  fld_nscount(fld_header(input_packet__3)) <= 65535
<S>  New H16:  fld_arcount(fld_header(input_packet__3)) <= 65535
<S>  New H42:  fld_messageid(fld_header(output_packet)) <= 65535
<S>  New H48:  fld_qdcount(fld_header(output_packet)) <= 65535
<S>  New H50:  fld_ancount(fld_header(output_packet)) <= 65535
<S>  New H52:  fld_nscount(fld_header(output_packet)) <= 65535
<S>  New H54:  fld_arcount(fld_header(output_packet)) <= 65535
-S-  Applied substitution rule udp_dns_task_rules(68).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__first by:
          dns_types__query.
<S>  New H5:  dns_types__query <= fld_opcode(fld_header(input_packet__3))
<S>  New H43:  dns_types__query <= fld_opcode(fld_header(output_packet))
-S-  Applied substitution rule udp_dns_task_rules(69).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__last by:
          dns_types__status.
<S>  New H6:  fld_opcode(fld_header(input_packet__3)) <= dns_types__status
<S>  New H44:  fld_opcode(fld_header(output_packet)) <= dns_types__status
-S-  Applied substitution rule udp_dns_task_rules(94).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H7:  dns_types__no_error <= fld_rcode(fld_header(input_packet__3))
<S>  New H45:  dns_types__no_error <= fld_rcode(fld_header(output_packet))
-S-  Applied substitution rule udp_dns_task_rules(95).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H8:  fld_rcode(fld_header(input_packet__3)) <= dns_types__refused
<S>  New H46:  fld_rcode(fld_header(output_packet)) <= dns_types__refused
---  Eliminated hypothesis H1 (true-hypothesis).
---  Eliminated hypothesis H20 (true-hypothesis).
---  Eliminated hypothesis H21 (true-hypothesis).
---  Eliminated hypothesis H22 (true-hypothesis).
---  Eliminated hypothesis H24 (true-hypothesis).
---  Eliminated hypothesis H25 (true-hypothesis).
---  Eliminated hypothesis H26 (true-hypothesis).
---  Eliminated hypothesis H27 (true-hypothesis).
---  Eliminated hypothesis H28 (true-hypothesis).
---  Eliminated hypothesis H29 (true-hypothesis).
---  Eliminated hypothesis H30 (true-hypothesis).
---  Eliminated hypothesis H31 (true-hypothesis).
---  Eliminated hypothesis H32 (true-hypothesis).
---  Eliminated hypothesis H33 (true-hypothesis).
---  Eliminated hypothesis H34 (true-hypothesis).
---  Eliminated hypothesis H35 (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).
>>>  Using "A->B, A |- B" on H2, given H23, we simplify the former to:
     >>>  H2:  input_bytes__3 >= 13 and input_bytes__3 <= 311
---  Eliminated hypothesis H23, which only specifies a value for failure__3.
     This is not referred to anywhere else in the VC.
>>>  Hypothesis H2 has now been split into two, giving:
     >>>  H57:  input_bytes__3 >= 13
     >>>  H58:  input_bytes__3 <= 311
---  Attempted addition of new hypothesis:
          input_bytes__3 >= 13
     eliminated: this already exists (as H57).
---  Attempted addition of new hypothesis:
          input_bytes__3 <= 311
     eliminated: this already exists (as H58).
>>>  Hypothesis H56 has now been split into two, giving:
     >>>  H57:  input_bytes__3 >= 13
     >>>  H58:  input_bytes__3 <= 311
***  Proved C4:  input_bytes__3 < 312
     using hypothesis H58.
***  Proved C3:  input_bytes__3 >= 13
     using hypothesis H57.
***  PROVED VC.


@@@@@@@@@@  VC: task_type_udp_dns_task_9.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          input_packet__3))
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__response_code__first <= fld_rcode(fld_header(
          input_packet__3))
%%%  Simplified H17 on reading formula in, to give:
     %%%  H17:  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(input_packet__3), [i___1])
           and element(fld_bytes(input_packet__3), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H25 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H30 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H11).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H12).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H19).
%%%  Simplified H43 on reading formula in, to give:
     %%%  H43:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H45 on reading formula in, to give:
     %%%  H45:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H55 on reading formula in, to give:
     %%%  H55:  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 H56 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H19).
%%%  Simplified H66 on reading formula in, to give:
     %%%  H66:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__5))
%%%  Simplified H68 on reading formula in, to give:
     %%%  H68:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__5))
%%%  Simplified H78 on reading formula in, to give:
     %%%  H78:  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__5), [i___1]
          ) and element(fld_bytes(output_packet__5), [i___1]) <= 
          dns_types__byte__last)
***  Proved C1:  max_transmit__5 >= dns_types__packet_length_range__first
     using hypothesis H81.
***  Proved C2:  max_transmit__5 <= dns_types__packet_length_range__last
     using hypothesis H82.
***  Proved C3:  output_bytes__5 >= dns_types__packet_length_range__first
     using hypothesis H79.
***  Proved C4:  output_bytes__5 <= dns_types__packet_length_range__last
     using hypothesis H80.
***  PROVED VC.


@@@@@@@@@@  VC: task_type_udp_dns_task_10.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          input_packet__3))
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__response_code__first <= fld_rcode(fld_header(
          input_packet__3))
%%%  Simplified H17 on reading formula in, to give:
     %%%  H17:  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(input_packet__3), [i___1])
           and element(fld_bytes(input_packet__3), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H25 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H30 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H11).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H12).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H19).
%%%  Simplified H43 on reading formula in, to give:
     %%%  H43:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H45 on reading formula in, to give:
     %%%  H45:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H55 on reading formula in, to give:
     %%%  H55:  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 H56 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H19).
%%%  Simplified H66 on reading formula in, to give:
     %%%  H66:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__5))
%%%  Simplified H68 on reading formula in, to give:
     %%%  H68:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__5))
%%%  Simplified H78 on reading formula in, to give:
     %%%  H78:  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__5), [i___1]
          ) and element(fld_bytes(output_packet__5), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H83 has been replaced by "true".  (It is already present, as 
          H81).
---  Hypothesis H84 has been replaced by "true".  (It is already present, as 
          H82).
---  Hypothesis H85 has been replaced by "true".  (It is already present, as 
          H79).
---  Hypothesis H86 has been replaced by "true".  (It is already present, as 
          H80).
---  Hypothesis H87 has been replaced by "true".  (It is already present, as 
          H79).
---  Hypothesis H88 has been replaced by "true".  (It is already present, as 
          H80).
---  Hypothesis H89 has been replaced by "true".  (It is already present, as 
          H81).
---  Hypothesis H90 has been replaced by "true".  (It is already present, as 
          H82).
***  Proved C1:  dns_types__packet_length_range__min(max_transmit__5, 
          output_bytes__5) >= dns_types__packet_length_range__first
     using hypotheses H79 & H81.
***  Proved C2:  dns_types__packet_length_range__min(max_transmit__5, 
          output_bytes__5) <= dns_types__packet_length_range__last
     using hypotheses H80 & H82.
***  PROVED VC.


@@@@@@@@@@  VC: task_type_udp_dns_task_11.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          input_packet__3))
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__response_code__first <= fld_rcode(fld_header(
          input_packet__3))
%%%  Simplified H17 on reading formula in, to give:
     %%%  H17:  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(input_packet__3), [i___1])
           and element(fld_bytes(input_packet__3), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H25 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H30 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H11).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H12).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H19).
%%%  Simplified H43 on reading formula in, to give:
     %%%  H43:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H45 on reading formula in, to give:
     %%%  H45:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H55 on reading formula in, to give:
     %%%  H55:  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 H56 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H19).
%%%  Simplified H66 on reading formula in, to give:
     %%%  H66:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__5))
%%%  Simplified H68 on reading formula in, to give:
     %%%  H68:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__5))
%%%  Simplified H78 on reading formula in, to give:
     %%%  H78:  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__5), [i___1]
          ) and element(fld_bytes(output_packet__5), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H83 has been replaced by "true".  (It is already present, as 
          H81).
---  Hypothesis H84 has been replaced by "true".  (It is already present, as 
          H82).
---  Hypothesis H85 has been replaced by "true".  (It is already present, as 
          H79).
---  Hypothesis H86 has been replaced by "true".  (It is already present, as 
          H80).
---  Hypothesis H87 has been replaced by "true".  (It is already present, as 
          H79).
---  Hypothesis H88 has been replaced by "true".  (It is already present, as 
          H80).
---  Hypothesis H89 has been replaced by "true".  (It is already present, as 
          H81).
---  Hypothesis H90 has been replaced by "true".  (It is already present, as 
          H82).
---  Hypothesis H93 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H94 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H95 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H96 has been replaced by "true".  (It is already present, as 
          H67).
---  Hypothesis H97 has been replaced by "true".  (It is already present, as 
          H68).
---  Hypothesis H98 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H99 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H100 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H101 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H102 has been replaced by "true".  (It is already present, as 
          H73).
---  Hypothesis H103 has been replaced by "true".  (It is already present, as 
          H74).
---  Hypothesis H104 has been replaced by "true".  (It is already present, as 
          H75).
---  Hypothesis H105 has been replaced by "true".  (It is already present, as 
          H76).
---  Hypothesis H106 has been replaced by "true".  (It is already present, as 
          H77).
---  Hypothesis H107 has been replaced by "true".  (It is already present, as 
          H78).
---  Hypothesis H108 has been replaced by "true".  (It is already present, as 
          H91).
---  Hypothesis H109 has been replaced by "true".  (It is already present, as 
          H92).
***  Proved C1:  dns_types__packet_length_range__min(max_transmit__5, 
          output_bytes__5) >= dns_types__packet_length_range__first
     using hypothesis H91.
***  Proved C2:  dns_types__packet_length_range__min(max_transmit__5, 
          output_bytes__5) <= dns_types__packet_length_range__last
     using hypothesis H92.
+++  Using "A->B, A |- B" on hypotheses H2 & H23 yields a new hypothesis:
     +++  H111:  input_bytes__3 >= 1 + dns_types__header_bits div 8 and 
          input_bytes__3 <= dns_network__max_query_size
-S-  Applied substitution rule udp_dns_task_rules(2).
     This was achieved by replacing all occurrences of dns_types__packet_size 
          by:
          8192.
<S>  New H61:  output_bytes__5 <= 8192
<S>  New H62:  max_transmit__5 <= 8192
-S-  Applied substitution rule udp_dns_task_rules(3).
     This was achieved by replacing all occurrences of dns_types__header_bits 
          by:
          96.
<S>  New H2:  not failure__3 -> input_bytes__3 >= 13 and input_bytes__3 <= 
          dns_network__max_query_size
<S>  New H58:  input_bytes__3 >= 13
<S>  New H60:  output_bytes__5 >= 13
<S>  New H111:  input_bytes__3 >= 13 and input_bytes__3 <= 
          dns_network__max_query_size
<S>  New C3:  dns_types__packet_length_range__min(max_transmit__5, 
          output_bytes__5) > 12
-S-  Applied substitution rule udp_dns_task_rules(4).
     This was achieved by replacing all occurrences of dns_types__udp_max_size 
          by:
          512.
<S>  New H63:  max_transmit__5 >= 512
-S-  Applied substitution rule udp_dns_task_rules(5).
     This was achieved by replacing all occurrences of 
          dns_network__max_query_size by:
          311.
<S>  New H2:  not failure__3 -> input_bytes__3 >= 13 and input_bytes__3 <= 311
<S>  New H111:  input_bytes__3 >= 13 and input_bytes__3 <= 311
-S-  Applied substitution rule udp_dns_task_rules(44).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__first by:
          0.
<S>  New H18:  input_bytes__3 >= 0
<S>  New H79:  output_bytes__5 >= 0
<S>  New H81:  max_transmit__5 >= 0
<S>  New H91:  dns_types__packet_length_range__min(max_transmit__5, 
          output_bytes__5) >= 0
-S-  Applied substitution rule udp_dns_task_rules(45).
     This was achieved by replacing all occurrences of 
          dns_types__packet_length_range__last by:
          8192.
<S>  New H19:  input_bytes__3 <= 8192
<S>  New H80:  output_bytes__5 <= 8192
<S>  New H82:  max_transmit__5 <= 8192
<S>  New H92:  dns_types__packet_length_range__min(max_transmit__5, 
          output_bytes__5) <= 8192
-S-  Applied substitution rule udp_dns_task_rules(49).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H17:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(fld_bytes(input_packet__3), [i___1]) and element(fld_bytes(
          input_packet__3), [i___1]) <= dns_types__byte__last)
<S>  New H55:  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 H78:  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__5), [i___1]) and element(fld_bytes(
          output_packet__5), [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule udp_dns_task_rules(50).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H17:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(input_packet__3), [i___1])
           and element(fld_bytes(input_packet__3), [i___1]) <= 
          dns_types__byte__last)
<S>  New H55:  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 H78:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(fld_bytes(output_packet__5), [i___1]
          ) and element(fld_bytes(output_packet__5), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule udp_dns_task_rules(55).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H17:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(input_packet__3), [i___1]) and element(fld_bytes(
          input_packet__3), [i___1]) <= dns_types__byte__last)
<S>  New H55:  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 H78:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet__5), [i___1]) and element(fld_bytes(
          output_packet__5), [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule udp_dns_task_rules(56).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H17:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(input_packet__3), [i___1]) and element(fld_bytes(
          input_packet__3), [i___1]) <= 255)
<S>  New H55:  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 H78:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(fld_bytes(output_packet__5), [i___1]) and element(fld_bytes(
          output_packet__5), [i___1]) <= 255)
-S-  Applied substitution rule udp_dns_task_rules(62).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__first by:
          0.
<S>  New H3:  fld_messageid(fld_header(input_packet__3)) >= 0
<S>  New H9:  fld_qdcount(fld_header(input_packet__3)) >= 0
<S>  New H11:  fld_ancount(fld_header(input_packet__3)) >= 0
<S>  New H13:  fld_nscount(fld_header(input_packet__3)) >= 0
<S>  New H15:  fld_arcount(fld_header(input_packet__3)) >= 0
<S>  New H41:  fld_messageid(fld_header(output_packet)) >= 0
<S>  New H47:  fld_qdcount(fld_header(output_packet)) >= 0
<S>  New H49:  fld_ancount(fld_header(output_packet)) >= 0
<S>  New H51:  fld_nscount(fld_header(output_packet)) >= 0
<S>  New H53:  fld_arcount(fld_header(output_packet)) >= 0
<S>  New H64:  fld_messageid(fld_header(output_packet__5)) >= 0
<S>  New H70:  fld_qdcount(fld_header(output_packet__5)) >= 0
<S>  New H72:  fld_ancount(fld_header(output_packet__5)) >= 0
<S>  New H74:  fld_nscount(fld_header(output_packet__5)) >= 0
<S>  New H76:  fld_arcount(fld_header(output_packet__5)) >= 0
-S-  Applied substitution rule udp_dns_task_rules(63).
     This was achieved by replacing all occurrences of 
          dns_types__unsigned_short__last by:
          65535.
<S>  New H4:  fld_messageid(fld_header(input_packet__3)) <= 65535
<S>  New H10:  fld_qdcount(fld_header(input_packet__3)) <= 65535
<S>  New H12:  fld_ancount(fld_header(input_packet__3)) <= 65535
<S>  New H14:  fld_nscount(fld_header(input_packet__3)) <= 65535
<S>  New H16:  fld_arcount(fld_header(input_packet__3)) <= 65535
<S>  New H42:  fld_messageid(fld_header(output_packet)) <= 65535
<S>  New H48:  fld_qdcount(fld_header(output_packet)) <= 65535
<S>  New H50:  fld_ancount(fld_header(output_packet)) <= 65535
<S>  New H52:  fld_nscount(fld_header(output_packet)) <= 65535
<S>  New H54:  fld_arcount(fld_header(output_packet)) <= 65535
<S>  New H65:  fld_messageid(fld_header(output_packet__5)) <= 65535
<S>  New H71:  fld_qdcount(fld_header(output_packet__5)) <= 65535
<S>  New H73:  fld_ancount(fld_header(output_packet__5)) <= 65535
<S>  New H75:  fld_nscount(fld_header(output_packet__5)) <= 65535
<S>  New H77:  fld_arcount(fld_header(output_packet__5)) <= 65535
-S-  Applied substitution rule udp_dns_task_rules(68).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__first by:
          dns_types__query.
<S>  New H5:  dns_types__query <= fld_opcode(fld_header(input_packet__3))
<S>  New H43:  dns_types__query <= fld_opcode(fld_header(output_packet))
<S>  New H66:  dns_types__query <= fld_opcode(fld_header(output_packet__5))
-S-  Applied substitution rule udp_dns_task_rules(69).
     This was achieved by replacing all occurrences of 
          dns_types__opcode_type__last by:
          dns_types__status.
<S>  New H6:  fld_opcode(fld_header(input_packet__3)) <= dns_types__status
<S>  New H44:  fld_opcode(fld_header(output_packet)) <= dns_types__status
<S>  New H67:  fld_opcode(fld_header(output_packet__5)) <= dns_types__status
-S-  Applied substitution rule udp_dns_task_rules(94).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__first by:
          dns_types__no_error.
<S>  New H7:  dns_types__no_error <= fld_rcode(fld_header(input_packet__3))
<S>  New H45:  dns_types__no_error <= fld_rcode(fld_header(output_packet))
<S>  New H68:  dns_types__no_error <= fld_rcode(fld_header(output_packet__5))
-S-  Applied substitution rule udp_dns_task_rules(95).
     This was achieved by replacing all occurrences of 
          dns_types__response_code__last by:
          dns_types__refused.
<S>  New H8:  fld_rcode(fld_header(input_packet__3)) <= dns_types__refused
<S>  New H46:  fld_rcode(fld_header(output_packet)) <= dns_types__refused
<S>  New H69:  fld_rcode(fld_header(output_packet__5)) <= dns_types__refused
---  Eliminated hypothesis H1 (true-hypothesis).
---  Eliminated hypothesis H20 (true-hypothesis).
---  Eliminated hypothesis H21 (true-hypothesis).
---  Eliminated hypothesis H22 (true-hypothesis).
---  Eliminated hypothesis H24 (true-hypothesis).
---  Eliminated hypothesis H25 (true-hypothesis).
---  Eliminated hypothesis H26 (true-hypothesis).
---  Eliminated hypothesis H27 (true-hypothesis).
---  Eliminated hypothesis H28 (true-hypothesis).
---  Eliminated hypothesis H29 (true-hypothesis).
---  Eliminated hypothesis H30 (true-hypothesis).
---  Eliminated hypothesis H31 (true-hypothesis).
---  Eliminated hypothesis H32 (true-hypothesis).
---  Eliminated hypothesis H33 (true-hypothesis).
---  Eliminated hypothesis H34 (true-hypothesis).
---  Eliminated hypothesis H35 (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 H56 (true-hypothesis).
---  Eliminated hypothesis H57 (true-hypothesis).
---  Eliminated hypothesis H83 (true-hypothesis).
---  Eliminated hypothesis H84 (true-hypothesis).
---  Eliminated hypothesis H85 (true-hypothesis).
---  Eliminated hypothesis H86 (true-hypothesis).
---  Eliminated hypothesis H87 (true-hypothesis).
---  Eliminated hypothesis H88 (true-hypothesis).
---  Eliminated hypothesis H89 (true-hypothesis).
---  Eliminated hypothesis H90 (true-hypothesis).
---  Eliminated hypothesis H93 (true-hypothesis).
---  Eliminated hypothesis H94 (true-hypothesis).
---  Eliminated hypothesis H95 (true-hypothesis).
---  Eliminated hypothesis H96 (true-hypothesis).
---  Eliminated hypothesis H97 (true-hypothesis).
---  Eliminated hypothesis H98 (true-hypothesis).
---  Eliminated hypothesis H99 (true-hypothesis).
---  Eliminated hypothesis H100 (true-hypothesis).
---  Eliminated hypothesis H101 (true-hypothesis).
---  Eliminated hypothesis H102 (true-hypothesis).
---  Eliminated hypothesis H103 (true-hypothesis).
---  Eliminated hypothesis H104 (true-hypothesis).
---  Eliminated hypothesis H105 (true-hypothesis).
---  Eliminated hypothesis H106 (true-hypothesis).
---  Eliminated hypothesis H107 (true-hypothesis).
---  Eliminated hypothesis H108 (true-hypothesis).
---  Eliminated hypothesis H109 (true-hypothesis).
---  Eliminated hypothesis H110 (true-hypothesis).
---  Eliminated hypothesis H80 (duplicate of H61).
---  Eliminated hypothesis H82 (duplicate of H62).
>>>  Using "A->B, A |- B" on H2, given H23, we simplify the former to:
     >>>  H2:  input_bytes__3 >= 13 and input_bytes__3 <= 311
---  Eliminated hypothesis H18 (redundant, given H58).
---  Eliminated hypothesis H19 (redundant, given H59).
---  Eliminated hypothesis H79 (redundant, given H60).
---  Eliminated hypothesis H81 (redundant, given H63).
---  Eliminated hypothesis H23, which only specifies a value for failure__3.
     This is not referred to anywhere else in the VC.
---  Attempted addition of new hypothesis:
          input_bytes__3 >= 13
     eliminated: this already exists (as H58).
>>>  Hypothesis H2 has now been split into two, giving:
     >>>  H58:  input_bytes__3 >= 13
     >>>  H112:  input_bytes__3 <= 311
---  Attempted addition of new hypothesis:
          input_bytes__3 >= 13
     eliminated: this already exists (as H58).
---  Attempted addition of new hypothesis:
          input_bytes__3 <= 311
     eliminated: this already exists (as H112).
>>>  Hypothesis H111 has now been split into two, giving:
     >>>  H58:  input_bytes__3 >= 13
     >>>  H112:  input_bytes__3 <= 311
     +++  New H113:  integer__size >= 0
     +++  New H114:  natural__size >= 0
     +++  New H115:  system__bit_order__size >= 0
     +++  New H116:  dns_types__packet_length_range__size >= 0
     +++  New H117:  dns_types__packet_bytes_range__size >= 0
     +++  New H118:  dns_types__dns_packet__size >= 0


@@@@@@@@@@  VC: task_type_udp_dns_task_12.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          input_packet__3))
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  dns_types__response_code__first <= fld_rcode(fld_header(
          input_packet__3))
%%%  Simplified H17 on reading formula in, to give:
     %%%  H17:  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(input_packet__3), [i___1])
           and element(fld_bytes(input_packet__3), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H25 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H30 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H11).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H12).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H19).
%%%  Simplified H43 on reading formula in, to give:
     %%%  H43:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet))
%%%  Simplified H45 on reading formula in, to give:
     %%%  H45:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet))
%%%  Simplified H55 on reading formula in, to give:
     %%%  H55:  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 H56 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H19).
%%%  Simplified H66 on reading formula in, to give:
     %%%  H66:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__5))
%%%  Simplified H68 on reading formula in, to give:
     %%%  H68:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__5))
%%%  Simplified H78 on reading formula in, to give:
     %%%  H78:  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__5), [i___1]
          ) and element(fld_bytes(output_packet__5), [i___1]) <= 
          dns_types__byte__last)
---  Hypothesis H83 has been replaced by "true".  (It is already present, as 
          H81).
---  Hypothesis H84 has been replaced by "true".  (It is already present, as 
          H82).
---  Hypothesis H85 has been replaced by "true".  (It is already present, as 
          H79).
---  Hypothesis H86 has been replaced by "true".  (It is already present, as 
          H80).
---  Hypothesis H87 has been replaced by "true".  (It is already present, as 
          H79).
---  Hypothesis H88 has been replaced by "true".  (It is already present, as 
          H80).
---  Hypothesis H89 has been replaced by "true".  (It is already present, as 
          H81).
---  Hypothesis H90 has been replaced by "true".  (It is already present, as 
          H82).
---  Hypothesis H93 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H94 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H95 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H96 has been replaced by "true".  (It is already present, as 
          H67).
---  Hypothesis H97 has been replaced by "true".  (It is already present, as 
          H68).
---  Hypothesis H98 has been replaced by "true".  (It is already present, as 
          H69).
---  Hypothesis H99 has been replaced by "true".  (It is already present, as 
          H70).
---  Hypothesis H100 has been replaced by "true".  (It is already present, as 
          H71).
---  Hypothesis H101 has been replaced by "true".  (It is already present, as 
          H72).
---  Hypothesis H102 has been replaced by "true".  (It is already present, as 
          H73).
---  Hypothesis H103 has been replaced by "true".  (It is already present, as 
          H74).
---  Hypothesis H104 has been replaced by "true".  (It is already present, as 
          H75).
---  Hypothesis H105 has been replaced by "true".  (It is already present, as 
          H76).
---  Hypothesis H106 has been replaced by "true".  (It is already present, as 
          H77).
---  Hypothesis H107 has been replaced by "true".  (It is already present, as 
          H78).
---  Hypothesis H108 has been replaced by "true".  (It is already present, as 
          H91).
---  Hypothesis H109 has been replaced by "true".  (It is already present, as 
          H92).
---  Hypothesis H111 has been replaced by "true".  (It is already present, as 
          H91).
---  Hypothesis H112 has been replaced by "true".  (It is already present, as 
          H92).
%%%  Simplified H117 on reading formula in, to give:
     %%%  H117:  dns_types__opcode_type__first <= fld_opcode(fld_header(
          output_packet__6))
%%%  Simplified H119 on reading formula in, to give:
     %%%  H119:  dns_types__response_code__first <= fld_rcode(fld_header(
          output_packet__6))
%%%  Simplified H129 on reading formula in, to give:
     %%%  H129:  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__6), [i___1]
          ) and element(fld_bytes(output_packet__6), [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule udp_dns_task_rules(16).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule udp_dns_task_rules(17).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


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


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


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

