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

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



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

procedure DNS_Types.Byte_Swap






@@@@@@@@@@  VC: procedure_byte_swap_1.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  opcode_type__first <= fld_opcode(h)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  response_code__first <= fld_rcode(h)
***  Proved C1:  fld_messageid(h) >= unsigned_short__first
     using hypothesis H1.
***  Proved C2:  fld_messageid(h) <= unsigned_short__last
     using hypothesis H2.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_byte_swap_2.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  opcode_type__first <= fld_opcode(h)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  response_code__first <= fld_rcode(h)
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H1)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H2)
          .
***  Proved C1:  byte_swap_us(fld_messageid(h)) >= unsigned_short__first
     using hypothesis H17.
***  Proved C2:  byte_swap_us(fld_messageid(h)) <= unsigned_short__last
     using hypothesis H18.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_byte_swap_3.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  opcode_type__first <= fld_opcode(h)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  response_code__first <= fld_rcode(h)
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H1)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  fld_qdcount(h) >= unsigned_short__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  fld_qdcount(h) <= unsigned_short__last
***  Proved C1:  fld_qdcount(h) >= unsigned_short__first
     using hypothesis H7.
***  Proved C2:  fld_qdcount(h) <= unsigned_short__last
     using hypothesis H8.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_byte_swap_4.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  opcode_type__first <= fld_opcode(h)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  response_code__first <= fld_rcode(h)
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H1)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  fld_qdcount(h) >= unsigned_short__first
%%%  Simplified H22 on reading formula in, to give:
     %%%  H22:  fld_qdcount(h) <= unsigned_short__last
%%%  Simplified H23 on reading formula in, to give:
     %%%  H23:  byte_swap_us(fld_qdcount(h)) >= unsigned_short__first
%%%  Simplified H24 on reading formula in, to give:
     %%%  H24:  byte_swap_us(fld_qdcount(h)) <= unsigned_short__last
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  byte_swap_us(fld_qdcount(h)) >= unsigned_short__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  byte_swap_us(fld_qdcount(h)) <= unsigned_short__last
***  Proved C1:  byte_swap_us(fld_qdcount(h)) >= unsigned_short__first
     using hypothesis H23.
***  Proved C2:  byte_swap_us(fld_qdcount(h)) <= unsigned_short__last
     using hypothesis H24.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_byte_swap_5.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  opcode_type__first <= fld_opcode(h)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  response_code__first <= fld_rcode(h)
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H1)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  fld_qdcount(h) >= unsigned_short__first
%%%  Simplified H22 on reading formula in, to give:
     %%%  H22:  fld_qdcount(h) <= unsigned_short__last
%%%  Simplified H23 on reading formula in, to give:
     %%%  H23:  byte_swap_us(fld_qdcount(h)) >= unsigned_short__first
%%%  Simplified H24 on reading formula in, to give:
     %%%  H24:  byte_swap_us(fld_qdcount(h)) <= unsigned_short__last
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  fld_ancount(h) >= unsigned_short__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  fld_ancount(h) <= unsigned_short__last
***  Proved C1:  fld_ancount(h) >= unsigned_short__first
     using hypothesis H9.
***  Proved C2:  fld_ancount(h) <= unsigned_short__last
     using hypothesis H10.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_byte_swap_6.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  opcode_type__first <= fld_opcode(h)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  response_code__first <= fld_rcode(h)
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H1)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  fld_qdcount(h) >= unsigned_short__first
%%%  Simplified H22 on reading formula in, to give:
     %%%  H22:  fld_qdcount(h) <= unsigned_short__last
%%%  Simplified H23 on reading formula in, to give:
     %%%  H23:  byte_swap_us(fld_qdcount(h)) >= unsigned_short__first
%%%  Simplified H24 on reading formula in, to give:
     %%%  H24:  byte_swap_us(fld_qdcount(h)) <= unsigned_short__last
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  fld_ancount(h) >= unsigned_short__first
%%%  Simplified H28 on reading formula in, to give:
     %%%  H28:  fld_ancount(h) <= unsigned_short__last
%%%  Simplified H29 on reading formula in, to give:
     %%%  H29:  byte_swap_us(fld_ancount(h)) >= unsigned_short__first
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  byte_swap_us(fld_ancount(h)) <= unsigned_short__last
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  byte_swap_us(fld_ancount(h)) >= unsigned_short__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  byte_swap_us(fld_ancount(h)) <= unsigned_short__last
***  Proved C1:  byte_swap_us(fld_ancount(h)) >= unsigned_short__first
     using hypothesis H29.
***  Proved C2:  byte_swap_us(fld_ancount(h)) <= unsigned_short__last
     using hypothesis H30.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_byte_swap_7.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  opcode_type__first <= fld_opcode(h)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  response_code__first <= fld_rcode(h)
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H1)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  fld_qdcount(h) >= unsigned_short__first
%%%  Simplified H22 on reading formula in, to give:
     %%%  H22:  fld_qdcount(h) <= unsigned_short__last
%%%  Simplified H23 on reading formula in, to give:
     %%%  H23:  byte_swap_us(fld_qdcount(h)) >= unsigned_short__first
%%%  Simplified H24 on reading formula in, to give:
     %%%  H24:  byte_swap_us(fld_qdcount(h)) <= unsigned_short__last
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  fld_ancount(h) >= unsigned_short__first
%%%  Simplified H28 on reading formula in, to give:
     %%%  H28:  fld_ancount(h) <= unsigned_short__last
%%%  Simplified H29 on reading formula in, to give:
     %%%  H29:  byte_swap_us(fld_ancount(h)) >= unsigned_short__first
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  byte_swap_us(fld_ancount(h)) <= unsigned_short__last
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  fld_nscount(h) >= unsigned_short__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  fld_nscount(h) <= unsigned_short__last
***  Proved C1:  fld_nscount(h) >= unsigned_short__first
     using hypothesis H11.
***  Proved C2:  fld_nscount(h) <= unsigned_short__last
     using hypothesis H12.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_byte_swap_8.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  opcode_type__first <= fld_opcode(h)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  response_code__first <= fld_rcode(h)
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H1)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  fld_qdcount(h) >= unsigned_short__first
%%%  Simplified H22 on reading formula in, to give:
     %%%  H22:  fld_qdcount(h) <= unsigned_short__last
%%%  Simplified H23 on reading formula in, to give:
     %%%  H23:  byte_swap_us(fld_qdcount(h)) >= unsigned_short__first
%%%  Simplified H24 on reading formula in, to give:
     %%%  H24:  byte_swap_us(fld_qdcount(h)) <= unsigned_short__last
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  fld_ancount(h) >= unsigned_short__first
%%%  Simplified H28 on reading formula in, to give:
     %%%  H28:  fld_ancount(h) <= unsigned_short__last
%%%  Simplified H29 on reading formula in, to give:
     %%%  H29:  byte_swap_us(fld_ancount(h)) >= unsigned_short__first
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  byte_swap_us(fld_ancount(h)) <= unsigned_short__last
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
%%%  Simplified H33 on reading formula in, to give:
     %%%  H33:  fld_nscount(h) >= unsigned_short__first
%%%  Simplified H34 on reading formula in, to give:
     %%%  H34:  fld_nscount(h) <= unsigned_short__last
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  byte_swap_us(fld_nscount(h)) >= unsigned_short__first
%%%  Simplified H36 on reading formula in, to give:
     %%%  H36:  byte_swap_us(fld_nscount(h)) <= unsigned_short__last
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  byte_swap_us(fld_nscount(h)) >= unsigned_short__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  byte_swap_us(fld_nscount(h)) <= unsigned_short__last
***  Proved C1:  byte_swap_us(fld_nscount(h)) >= unsigned_short__first
     using hypothesis H35.
***  Proved C2:  byte_swap_us(fld_nscount(h)) <= unsigned_short__last
     using hypothesis H36.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_byte_swap_9.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  opcode_type__first <= fld_opcode(h)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  response_code__first <= fld_rcode(h)
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H1)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  fld_qdcount(h) >= unsigned_short__first
%%%  Simplified H22 on reading formula in, to give:
     %%%  H22:  fld_qdcount(h) <= unsigned_short__last
%%%  Simplified H23 on reading formula in, to give:
     %%%  H23:  byte_swap_us(fld_qdcount(h)) >= unsigned_short__first
%%%  Simplified H24 on reading formula in, to give:
     %%%  H24:  byte_swap_us(fld_qdcount(h)) <= unsigned_short__last
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  fld_ancount(h) >= unsigned_short__first
%%%  Simplified H28 on reading formula in, to give:
     %%%  H28:  fld_ancount(h) <= unsigned_short__last
%%%  Simplified H29 on reading formula in, to give:
     %%%  H29:  byte_swap_us(fld_ancount(h)) >= unsigned_short__first
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  byte_swap_us(fld_ancount(h)) <= unsigned_short__last
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
%%%  Simplified H33 on reading formula in, to give:
     %%%  H33:  fld_nscount(h) >= unsigned_short__first
%%%  Simplified H34 on reading formula in, to give:
     %%%  H34:  fld_nscount(h) <= unsigned_short__last
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  byte_swap_us(fld_nscount(h)) >= unsigned_short__first
%%%  Simplified H36 on reading formula in, to give:
     %%%  H36:  byte_swap_us(fld_nscount(h)) <= unsigned_short__last
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H36).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  fld_arcount(h) >= unsigned_short__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  fld_arcount(h) <= unsigned_short__last
***  Proved C1:  fld_arcount(h) >= unsigned_short__first
     using hypothesis H13.
***  Proved C2:  fld_arcount(h) <= unsigned_short__last
     using hypothesis H14.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_byte_swap_10.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  opcode_type__first <= fld_opcode(h)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  response_code__first <= fld_rcode(h)
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H1)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  fld_qdcount(h) >= unsigned_short__first
%%%  Simplified H22 on reading formula in, to give:
     %%%  H22:  fld_qdcount(h) <= unsigned_short__last
%%%  Simplified H23 on reading formula in, to give:
     %%%  H23:  byte_swap_us(fld_qdcount(h)) >= unsigned_short__first
%%%  Simplified H24 on reading formula in, to give:
     %%%  H24:  byte_swap_us(fld_qdcount(h)) <= unsigned_short__last
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  fld_ancount(h) >= unsigned_short__first
%%%  Simplified H28 on reading formula in, to give:
     %%%  H28:  fld_ancount(h) <= unsigned_short__last
%%%  Simplified H29 on reading formula in, to give:
     %%%  H29:  byte_swap_us(fld_ancount(h)) >= unsigned_short__first
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  byte_swap_us(fld_ancount(h)) <= unsigned_short__last
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
%%%  Simplified H33 on reading formula in, to give:
     %%%  H33:  fld_nscount(h) >= unsigned_short__first
%%%  Simplified H34 on reading formula in, to give:
     %%%  H34:  fld_nscount(h) <= unsigned_short__last
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  byte_swap_us(fld_nscount(h)) >= unsigned_short__first
%%%  Simplified H36 on reading formula in, to give:
     %%%  H36:  byte_swap_us(fld_nscount(h)) <= unsigned_short__last
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H36).
%%%  Simplified H39 on reading formula in, to give:
     %%%  H39:  fld_arcount(h) >= unsigned_short__first
%%%  Simplified H40 on reading formula in, to give:
     %%%  H40:  fld_arcount(h) <= unsigned_short__last
%%%  Simplified H41 on reading formula in, to give:
     %%%  H41:  byte_swap_us(fld_arcount(h)) >= unsigned_short__first
%%%  Simplified H42 on reading formula in, to give:
     %%%  H42:  byte_swap_us(fld_arcount(h)) <= unsigned_short__last
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  byte_swap_us(fld_arcount(h)) >= unsigned_short__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  byte_swap_us(fld_arcount(h)) <= unsigned_short__last
***  Proved C1:  byte_swap_us(fld_arcount(h)) >= unsigned_short__first
     using hypothesis H41.
***  Proved C2:  byte_swap_us(fld_arcount(h)) <= unsigned_short__last
     using hypothesis H42.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_byte_swap_11.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  opcode_type__first <= fld_opcode(h)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  response_code__first <= fld_rcode(h)
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H1)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  fld_qdcount(h) >= unsigned_short__first
%%%  Simplified H22 on reading formula in, to give:
     %%%  H22:  fld_qdcount(h) <= unsigned_short__last
%%%  Simplified H23 on reading formula in, to give:
     %%%  H23:  byte_swap_us(fld_qdcount(h)) >= unsigned_short__first
%%%  Simplified H24 on reading formula in, to give:
     %%%  H24:  byte_swap_us(fld_qdcount(h)) <= unsigned_short__last
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  fld_ancount(h) >= unsigned_short__first
%%%  Simplified H28 on reading formula in, to give:
     %%%  H28:  fld_ancount(h) <= unsigned_short__last
%%%  Simplified H29 on reading formula in, to give:
     %%%  H29:  byte_swap_us(fld_ancount(h)) >= unsigned_short__first
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  byte_swap_us(fld_ancount(h)) <= unsigned_short__last
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
%%%  Simplified H33 on reading formula in, to give:
     %%%  H33:  fld_nscount(h) >= unsigned_short__first
%%%  Simplified H34 on reading formula in, to give:
     %%%  H34:  fld_nscount(h) <= unsigned_short__last
%%%  Simplified H35 on reading formula in, to give:
     %%%  H35:  byte_swap_us(fld_nscount(h)) >= unsigned_short__first
%%%  Simplified H36 on reading formula in, to give:
     %%%  H36:  byte_swap_us(fld_nscount(h)) <= unsigned_short__last
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H35).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H36).
%%%  Simplified H39 on reading formula in, to give:
     %%%  H39:  fld_arcount(h) >= unsigned_short__first
%%%  Simplified H40 on reading formula in, to give:
     %%%  H40:  fld_arcount(h) <= unsigned_short__last
%%%  Simplified H41 on reading formula in, to give:
     %%%  H41:  byte_swap_us(fld_arcount(h)) >= unsigned_short__first
%%%  Simplified H42 on reading formula in, to give:
     %%%  H42:  byte_swap_us(fld_arcount(h)) <= unsigned_short__last
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H41).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H42).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  true
***  Proved C1:  true
***  PROVED VC.

