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






@@@@@@@@@@  VC: procedure_set_ttl_data_ptr_response_1.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  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(bytes, [i___1]) and element(bytes, [
          i___1]) <= dns_types__byte__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(fld_domainname(ptr_record), [i___1]) and 
          element(fld_domainname(ptr_record), [i___1]) <= character__last)
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H2)
          .
***  Proved C1:  fld_ttlinseconds(fld_inherit(ptr_record)) >= 
          unsigned_types__unsigned32__first
     using hypothesis H7.
***  Proved C2:  fld_ttlinseconds(fld_inherit(ptr_record)) <= 
          unsigned_types__unsigned32__last
     using hypothesis H8.
***  Proved C3:  start_byte >= dns_types__packet_bytes_range__first
     using hypothesis H5.
***  Proved C4:  start_byte <= dns_types__packet_bytes_range__last
     using hypothesis H6.
-S-  Applied substitution rule set_ttl_data_rules(7).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
          ptr_record), [i___1]) <= character__last)
-S-  Applied substitution rule set_ttl_data_rules(8).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
          ptr_record), [i___1]) <= 255)
-S-  Applied substitution rule set_ttl_data_rules(17).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 
          dns_types__byte__last)
<S>  New H5:  start_byte >= 1
-S-  Applied substitution rule set_ttl_data_rules(18).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H3:  start_byte <= 8174 - current_name_length
<S>  New H6:  start_byte <= 8180
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
          i___1]) <= dns_types__byte__last)
<S>  New C5:  start_byte <= 8177
-S-  Applied substitution rule set_ttl_data_rules(23).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule set_ttl_data_rules(24).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
-S-  Applied substitution rule set_ttl_data_rules(35).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H7:  fld_ttlinseconds(fld_inherit(ptr_record)) >= 0
-S-  Applied substitution rule set_ttl_data_rules(36).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H8:  fld_ttlinseconds(fld_inherit(ptr_record)) <= 4294967295
-S-  Applied substitution rule set_ttl_data_rules(41).
     This was achieved by replacing all occurrences of 
          rr_type__classtype__first by:
          rr_type__internet.
<S>  New H9:  rr_type__internet <= fld_class(fld_inherit(ptr_record))
-S-  Applied substitution rule set_ttl_data_rules(42).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H10:  fld_class(fld_inherit(ptr_record)) <= rr_type__hs
-S-  Applied substitution rule set_ttl_data_rules(68).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H12:  current_name_length >= 1
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(fld_domainname(
          ptr_record), [i___1]) and element(fld_domainname(ptr_record), [i___1])
           <= 255)
-S-  Applied substitution rule set_ttl_data_rules(69).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H2:  current_name_length <= 129
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(fld_domainname(ptr_record), [i___1]) and element(
          fld_domainname(ptr_record), [i___1]) <= 255)
---  Eliminated hypothesis H13 (true-hypothesis).
---  Eliminated hypothesis H1 (redundant, given H12).
---  Eliminated hypothesis H6 (redundant, given H3 & H12).
     +++  New H14:  integer__size >= 0
     +++  New H15:  character__size >= 0
     +++  New H16:  positive__size >= 0
     +++  New H17:  dns_types__packet_bytes_range__size >= 0
     +++  New H18:  unsigned_types__unsigned16__size >= 0
     +++  New H19:  unsigned_types__unsigned32__size >= 0
     +++  New H20:  rr_type__classtype__size >= 0
     +++  New H21:  rr_type__wirestringtypeindex__size >= 0
     +++  New H22:  rr_type__wirestringtype__size >= 0
     +++  New H23:  rr_type__resourcerecordtype__size >= 0
     +++  New H24:  rr_type__ptr_record_type__ptrrecordtype__size >= 0


@@@@@@@@@@  VC: procedure_set_ttl_data_ptr_response_2.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  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(bytes, [i___1]) and element(bytes, [
          i___1]) <= dns_types__byte__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(fld_domainname(ptr_record), [i___1]) and 
          element(fld_domainname(ptr_record), [i___1]) <= character__last)
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H6)
          .
%%%  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(bytes__1, [i___1]) and element(
          bytes__1, [i___1]) <= dns_types__byte__last)
***  Proved C3:  start_byte + 4 >= dns_types__packet_bytes_range__first
     using hypothesis H5.
-S-  Applied substitution rule set_ttl_data_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New C1:  current_name_length >= 0
<S>  New C6:  current_name_length >= 0
-S-  Applied substitution rule set_ttl_data_rules(30).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New C2:  current_name_length <= 65535
<S>  New C7:  current_name_length <= 65535
-S-  Applied substitution rule set_ttl_data_rules(18).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H3:  start_byte <= 8174 - current_name_length
<S>  New H4:  for_all(i___1 : integer, dns_types__packet_bytes_range__first <= 
          i___1 and i___1 <= 8180 -> dns_types__byte__first <= element(bytes, [
          i___1]) and element(bytes, [i___1]) <= dns_types__byte__last)
<S>  New H6:  start_byte <= 8180
<S>  New H18:  start_byte <= 8177
<S>  New H19:  for_all(i___1 : integer, dns_types__packet_bytes_range__first <= 
          i___1 and i___1 <= 8180 -> dns_types__byte__first <= element(
          bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 
          dns_types__byte__last)
<S>  New C4:  start_byte <= 8176
<S>  New C5:  start_byte <= 8175
-S-  Applied substitution rule set_ttl_data_rules(19).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__first by:
          - 2147483648.
<S>  New C8:  start_byte >= - 2147483652
-S-  Applied substitution rule set_ttl_data_rules(20).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__last by:
          2147483647.
<S>  New C9:  start_byte <= 2147483643
***  Proved C1:  current_name_length >= 0
     using hypothesis H1.
***  Proved C6:  current_name_length >= 0
     using hypothesis H1.
***  Proved C9:  start_byte <= 2147483643
     using hypothesis H6.
-S-  Applied substitution rule set_ttl_data_rules(7).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
          ptr_record), [i___1]) <= character__last)
-S-  Applied substitution rule set_ttl_data_rules(8).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
          ptr_record), [i___1]) <= 255)
-S-  Applied substitution rule set_ttl_data_rules(17).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
          i___1]) <= dns_types__byte__last)
<S>  New H5:  start_byte >= 1
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(bytes__1, [i___1]) and element(
          bytes__1, [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule set_ttl_data_rules(23).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 
          dns_types__byte__last)
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule set_ttl_data_rules(24).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 255)
-S-  Applied substitution rule set_ttl_data_rules(35).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H7:  fld_ttlinseconds(fld_inherit(ptr_record)) >= 0
-S-  Applied substitution rule set_ttl_data_rules(36).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H8:  fld_ttlinseconds(fld_inherit(ptr_record)) <= 4294967295
-S-  Applied substitution rule set_ttl_data_rules(41).
     This was achieved by replacing all occurrences of 
          rr_type__classtype__first by:
          rr_type__internet.
<S>  New H9:  rr_type__internet <= fld_class(fld_inherit(ptr_record))
-S-  Applied substitution rule set_ttl_data_rules(42).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H10:  fld_class(fld_inherit(ptr_record)) <= rr_type__hs
-S-  Applied substitution rule set_ttl_data_rules(68).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H12:  current_name_length >= 1
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(fld_domainname(
          ptr_record), [i___1]) and element(fld_domainname(ptr_record), [i___1])
           <= 255)
-S-  Applied substitution rule set_ttl_data_rules(69).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H2:  current_name_length <= 129
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(fld_domainname(ptr_record), [i___1]) and element(
          fld_domainname(ptr_record), [i___1]) <= 255)
***  Proved C2:  current_name_length <= 65535
     using hypothesis H2.
***  Proved C7:  current_name_length <= 65535
     using hypothesis H2.
***  Proved C8:  start_byte >= - 2147483652
     using hypothesis H5.
---  Eliminated hypothesis H13 (true-hypothesis).
---  Eliminated hypothesis H14 (true-hypothesis).
---  Eliminated hypothesis H15 (true-hypothesis).
---  Eliminated hypothesis H16 (true-hypothesis).
---  Eliminated hypothesis H17 (true-hypothesis).
---  Eliminated hypothesis H1 (redundant, given H12).
---  Eliminated hypothesis H6 (redundant, given H18).
---  Eliminated hypothesis H18 (redundant, given H3 & H12).
     +++  New H20:  integer__size >= 0
     +++  New H21:  character__size >= 0
     +++  New H22:  positive__size >= 0
     +++  New H23:  dns_types__packet_bytes_range__size >= 0
     +++  New H24:  unsigned_types__unsigned16__size >= 0
     +++  New H25:  unsigned_types__unsigned32__size >= 0
     +++  New H26:  rr_type__classtype__size >= 0
     +++  New H27:  rr_type__wirestringtypeindex__size >= 0
     +++  New H28:  rr_type__wirestringtype__size >= 0
     +++  New H29:  rr_type__resourcerecordtype__size >= 0
     +++  New H30:  rr_type__ptr_record_type__ptrrecordtype__size >= 0


@@@@@@@@@@  VC: procedure_set_ttl_data_ptr_response_3.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  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(bytes, [i___1]) and element(bytes, [
          i___1]) <= dns_types__byte__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(fld_domainname(ptr_record), [i___1]) and 
          element(fld_domainname(ptr_record), [i___1]) <= character__last)
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H6)
          .
%%%  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(bytes__1, [i___1]) and element(
          bytes__1, [i___1]) <= dns_types__byte__last)
---  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 H29 on reading formula in, to give:
     %%%  H29:  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(bytes__2, [i___1]) and element(
          bytes__2, [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule set_ttl_data_rules(2).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C1:  current_name_length >= - 2147483648
<S>  New C3:  true
-S-  Applied substitution rule set_ttl_data_rules(3).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C2:  current_name_length <= 2147483647
<S>  New C4:  true
***  Proved C1:  current_name_length >= - 2147483648
     using hypothesis H1.
***  Proved C3:  true
***  Proved C4:  true
-S-  Applied substitution rule set_ttl_data_rules(7).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
          ptr_record), [i___1]) <= character__last)
-S-  Applied substitution rule set_ttl_data_rules(8).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
          ptr_record), [i___1]) <= 255)
-S-  Applied substitution rule set_ttl_data_rules(17).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 
          dns_types__byte__last)
<S>  New H5:  start_byte >= 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(bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 
          dns_types__byte__last)
<S>  New H22:  start_byte >= - 3
<S>  New H29:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(bytes__2, [i___1]) and element(bytes__2, [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule set_ttl_data_rules(18).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H3:  start_byte <= 8174 - current_name_length
<S>  New H6:  start_byte <= 8180
<S>  New H18:  start_byte <= 8177
<S>  New H23:  start_byte <= 8176
<S>  New H24:  start_byte <= 8175
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
          i___1]) <= dns_types__byte__last)
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(bytes__1, [i___1]) and element(
          bytes__1, [i___1]) <= dns_types__byte__last)
<S>  New H29:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(bytes__2, [i___1]) and element(
          bytes__2, [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule set_ttl_data_rules(19).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__first by:
          - 2147483648.
<S>  New H27:  start_byte >= - 2147483652
-S-  Applied substitution rule set_ttl_data_rules(20).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__last by:
          2147483647.
<S>  New H28:  start_byte <= 2147483643
-S-  Applied substitution rule set_ttl_data_rules(23).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 
          dns_types__byte__last)
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 
          dns_types__byte__last)
<S>  New H29:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes__2, [i___1]) and element(bytes__2, [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule set_ttl_data_rules(24).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 255)
<S>  New H29:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes__2, [i___1]) and element(bytes__2, [i___1]) <= 255)
-S-  Applied substitution rule set_ttl_data_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New H20:  current_name_length >= 0
-S-  Applied substitution rule set_ttl_data_rules(30).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New H21:  current_name_length <= 65535
-S-  Applied substitution rule set_ttl_data_rules(35).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H7:  fld_ttlinseconds(fld_inherit(ptr_record)) >= 0
-S-  Applied substitution rule set_ttl_data_rules(36).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H8:  fld_ttlinseconds(fld_inherit(ptr_record)) <= 4294967295
-S-  Applied substitution rule set_ttl_data_rules(41).
     This was achieved by replacing all occurrences of 
          rr_type__classtype__first by:
          rr_type__internet.
<S>  New H9:  rr_type__internet <= fld_class(fld_inherit(ptr_record))
-S-  Applied substitution rule set_ttl_data_rules(42).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H10:  fld_class(fld_inherit(ptr_record)) <= rr_type__hs
-S-  Applied substitution rule set_ttl_data_rules(68).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H12:  current_name_length >= 1
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(fld_domainname(
          ptr_record), [i___1]) and element(fld_domainname(ptr_record), [i___1])
           <= 255)
-S-  Applied substitution rule set_ttl_data_rules(69).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H2:  current_name_length <= 129
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(fld_domainname(ptr_record), [i___1]) and element(
          fld_domainname(ptr_record), [i___1]) <= 255)
***  Proved C2:  current_name_length <= 2147483647
     using hypothesis H21.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_set_ttl_data_ptr_response_4.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  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(bytes, [i___1]) and element(bytes, [
          i___1]) <= dns_types__byte__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(fld_domainname(ptr_record), [i___1]) and 
          element(fld_domainname(ptr_record), [i___1]) <= character__last)
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H6)
          .
%%%  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(bytes__1, [i___1]) and element(
          bytes__1, [i___1]) <= dns_types__byte__last)
---  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 H29 on reading formula in, to give:
     %%%  H29:  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(bytes__2, [i___1]) and element(
          bytes__2, [i___1]) <= dns_types__byte__last)
***  Proved C1:  1 <= current_name_length -> current_name_length >= 
          rr_type__wirestringtypeindex__first and current_name_length <= 
          rr_type__wirestringtypeindex__last
     using hypotheses H2 & H12.
-S-  Applied substitution rule set_ttl_data_rules(2).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H30:  current_name_length >= - 2147483648
<S>  New H32:  true
-S-  Applied substitution rule set_ttl_data_rules(3).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H31:  current_name_length <= 2147483647
<S>  New H33:  true
-S-  Applied substitution rule set_ttl_data_rules(7).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
          ptr_record), [i___1]) <= character__last)
-S-  Applied substitution rule set_ttl_data_rules(8).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
          ptr_record), [i___1]) <= 255)
-S-  Applied substitution rule set_ttl_data_rules(17).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 
          dns_types__byte__last)
<S>  New H5:  start_byte >= 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(bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 
          dns_types__byte__last)
<S>  New H22:  start_byte >= - 3
<S>  New H29:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(bytes__2, [i___1]) and element(bytes__2, [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule set_ttl_data_rules(18).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H3:  start_byte <= 8174 - current_name_length
<S>  New H6:  start_byte <= 8180
<S>  New H18:  start_byte <= 8177
<S>  New H23:  start_byte <= 8176
<S>  New H24:  start_byte <= 8175
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
          i___1]) <= dns_types__byte__last)
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(bytes__1, [i___1]) and element(
          bytes__1, [i___1]) <= dns_types__byte__last)
<S>  New H29:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(bytes__2, [i___1]) and element(
          bytes__2, [i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule set_ttl_data_rules(19).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__first by:
          - 2147483648.
<S>  New H27:  start_byte >= - 2147483652
-S-  Applied substitution rule set_ttl_data_rules(20).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__last by:
          2147483647.
<S>  New H28:  start_byte <= 2147483643
-S-  Applied substitution rule set_ttl_data_rules(23).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 
          dns_types__byte__last)
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 
          dns_types__byte__last)
<S>  New H29:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes__2, [i___1]) and element(bytes__2, [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule set_ttl_data_rules(24).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
<S>  New H19:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes__1, [i___1]) and element(bytes__1, [i___1]) <= 255)
<S>  New H29:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes__2, [i___1]) and element(bytes__2, [i___1]) <= 255)
-S-  Applied substitution rule set_ttl_data_rules(29).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New H20:  current_name_length >= 0
-S-  Applied substitution rule set_ttl_data_rules(30).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New H21:  current_name_length <= 65535
-S-  Applied substitution rule set_ttl_data_rules(35).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H7:  fld_ttlinseconds(fld_inherit(ptr_record)) >= 0
-S-  Applied substitution rule set_ttl_data_rules(36).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H8:  fld_ttlinseconds(fld_inherit(ptr_record)) <= 4294967295
-S-  Applied substitution rule set_ttl_data_rules(41).
     This was achieved by replacing all occurrences of 
          rr_type__classtype__first by:
          rr_type__internet.
<S>  New H9:  rr_type__internet <= fld_class(fld_inherit(ptr_record))
-S-  Applied substitution rule set_ttl_data_rules(42).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H10:  fld_class(fld_inherit(ptr_record)) <= rr_type__hs
-S-  Applied substitution rule set_ttl_data_rules(68).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H12:  current_name_length >= 1
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(fld_domainname(
          ptr_record), [i___1]) and element(fld_domainname(ptr_record), [i___1])
           <= 255)
<S>  New C2:  1 <= current_name_length -> 1 <= 
          rr_type__wirestringtypeindex__last
-S-  Applied substitution rule set_ttl_data_rules(69).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H2:  current_name_length <= 129
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(fld_domainname(ptr_record), [i___1]) and element(
          fld_domainname(ptr_record), [i___1]) <= 255)
<S>  New C2:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_set_ttl_data_ptr_response_5.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  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(bytes, [i___1]) and element(bytes, [
          i___1]) <= dns_types__byte__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(fld_domainname(ptr_record), [i___1]) and 
          element(fld_domainname(ptr_record), [i___1]) <= character__last)
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H7)
          .
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H5)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H6)
          .
%%%  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(bytes__1, [i___1]) and element(
          bytes__1, [i___1]) <= dns_types__byte__last)
---  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 H29 on reading formula in, to give:
     %%%  H29:  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(bytes__2, [i___1]) and element(
          bytes__2, [i___1]) <= dns_types__byte__last)
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  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(bytes__2, [i___1]) and element(
          bytes__2, [i___1]) <= dns_types__byte__last)
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
%%%  Simplified C11 on reading formula in, to give:
     %%%  C11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(fld_domainname(ptr_record), [i___1]) and 
          element(fld_domainname(ptr_record), [i___1]) <= character__last)
%%%  Simplified C19 on reading formula in, to give:
     %%%  C19:  true
***  Proved C1:  start_byte <= dns_types__packet_bytes_range__last - 6 - 
          current_name_length
     using hypothesis H3.
***  Proved C3:  1 <= rr_type__wirestringtypeindex__last
     using hypotheses H2 & H36.
***  Proved C4:  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(bytes__2, [i___1]) and element(
          bytes__2, [i___1]) <= dns_types__byte__last)
     using hypothesis H29.
***  Proved C5:  start_byte >= dns_types__packet_bytes_range__first
     using hypothesis H5.
***  Proved C6:  start_byte <= dns_types__packet_bytes_range__last
     using hypothesis H6.
***  Proved C7:  fld_ttlinseconds(fld_inherit(ptr_record)) >= 
          unsigned_types__unsigned32__first
     using hypothesis H7.
***  Proved C8:  fld_ttlinseconds(fld_inherit(ptr_record)) <= 
          unsigned_types__unsigned32__last
     using hypothesis H8.
***  Proved C9:  rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
     using hypothesis H9.
***  Proved C10:  fld_class(fld_inherit(ptr_record)) <= rr_type__classtype__last
     using hypothesis H10.
***  Proved C11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first 
          <= i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(fld_domainname(ptr_record), [i___1]) and 
          element(fld_domainname(ptr_record), [i___1]) <= character__last)
     using hypothesis H11.
***  Proved C12:  current_name_length >= rr_type__wirestringtypeindex__first
     using hypothesis H12.
***  Proved C13:  current_name_length <= rr_type__wirestringtypeindex__last
     using hypothesis H2.
***  Proved C14:  current_name_length >= 0
     using hypothesis H1.
***  Proved C15:  current_name_length <= rr_type__wirestringtypeindex__last
     using hypothesis H2.
***  Proved C16:  start_byte <= dns_types__packet_bytes_range__last - 6 - 
          current_name_length
     using hypothesis H3.
***  Proved C18:  1 <= rr_type__wirestringtypeindex__last
     using hypotheses H2 & H36.
***  Proved C19:  true
***  Proved C20:  1 <= current_name_length
     using hypothesis H36.
-S-  Applied substitution rule set_ttl_data_rules(68).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> character__first <= element(
          fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
          ptr_record), [i___1]) <= character__last)
<S>  New H12:  current_name_length >= 1
<S>  New H34:  1 <= current_name_length -> current_name_length >= 1 and 
          current_name_length <= rr_type__wirestringtypeindex__last
<S>  New H35:  1 <= current_name_length -> 1 <= 
          rr_type__wirestringtypeindex__last
<S>  New C2:  true
<S>  New C17:  true
***  Proved C2:  true
***  Proved C17:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_set_ttl_data_ptr_response_6.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  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(bytes, [i___1]) and element(bytes, [
          i___1]) <= dns_types__byte__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(fld_domainname(ptr_record), [i___1]) and 
          element(fld_domainname(ptr_record), [i___1]) <= character__last)
---  Hypothesis H15 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H1)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  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(update(bytes, [start_byte + 5 + 
          loop__1__i], element(fld_domainname(ptr_record), [loop__1__i])), [
          i___1]) and element(update(bytes, [start_byte + 5 + loop__1__i], 
          element(fld_domainname(ptr_record), [loop__1__i])), [i___1]) <= 
          dns_types__byte__last)
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
%%%  Simplified C11 on reading formula in, to give:
     %%%  C11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(fld_domainname(ptr_record), [i___1]) and 
          element(fld_domainname(ptr_record), [i___1]) <= character__last)
%%%  Simplified C19 on reading formula in, to give:
     %%%  C19:  loop__1__i >= 0
***  Proved C1:  start_byte <= dns_types__packet_bytes_range__last - 6 - 
          current_name_length
     using hypothesis H1.
***  Proved C2:  loop__1__i + 1 >= rr_type__wirestringtypeindex__first
     using hypothesis H2.
***  Proved C4:  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(update(bytes, [start_byte + 5 + 
          loop__1__i], element(fld_domainname(ptr_record), [loop__1__i])), [
          i___1]) and element(update(bytes, [start_byte + 5 + loop__1__i], 
          element(fld_domainname(ptr_record), [loop__1__i])), [i___1]) <= 
          dns_types__byte__last)
     using hypotheses H4, H21, H22, H27 & H28.
***  Proved C5:  start_byte >= dns_types__packet_bytes_range__first
     using hypothesis H5.
***  Proved C6:  start_byte <= dns_types__packet_bytes_range__last
     using hypothesis H6.
***  Proved C7:  fld_ttlinseconds(fld_inherit(ptr_record)) >= 
          unsigned_types__unsigned32__first
     using hypothesis H7.
***  Proved C8:  fld_ttlinseconds(fld_inherit(ptr_record)) <= 
          unsigned_types__unsigned32__last
     using hypothesis H8.
***  Proved C9:  rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
     using hypothesis H9.
***  Proved C10:  fld_class(fld_inherit(ptr_record)) <= rr_type__classtype__last
     using hypothesis H10.
***  Proved C11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first 
          <= i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(fld_domainname(ptr_record), [i___1]) and 
          element(fld_domainname(ptr_record), [i___1]) <= character__last)
     using hypothesis H11.
***  Proved C12:  current_name_length >= rr_type__wirestringtypeindex__first
     using hypothesis H12.
***  Proved C13:  current_name_length <= rr_type__wirestringtypeindex__last
     using hypothesis H13.
***  Proved C14:  current_name_length >= 0
     using hypothesis H14.
***  Proved C15:  current_name_length <= rr_type__wirestringtypeindex__last
     using hypothesis H13.
***  Proved C16:  start_byte <= dns_types__packet_bytes_range__last - 6 - 
          current_name_length
     using hypothesis H1.
***  Proved C17:  loop__1__i + 1 >= rr_type__wirestringtypeindex__first
     using hypothesis H2.
***  Proved C19:  loop__1__i >= 0
     using hypothesis H19.
-S-  Applied substitution rule set_ttl_data_rules(69).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H3:  loop__1__i <= 129
<S>  New H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= 129 -> character__first <= element(fld_domainname(
          ptr_record), [i___1]) and element(fld_domainname(ptr_record), [i___1])
           <= character__last)
<S>  New H13:  current_name_length <= 129
<S>  New C3:  loop__1__i <= 128
<S>  New C18:  loop__1__i <= 128
***  Proved C3:  loop__1__i <= 128
     using hypotheses H13, H20 & H35.
***  Proved C18:  loop__1__i <= 128
     using hypotheses H13, H20 & H35.
>>>  Restructured hypothesis H35 into:
     >>>  H35:  loop__1__i <> current_name_length
-S-  Applied substitution rule set_ttl_data_rules(7).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= 129 -> 0 <= element(fld_domainname(ptr_record), [
          i___1]) and element(fld_domainname(ptr_record), [i___1]) <= 
          character__last)
-S-  Applied substitution rule set_ttl_data_rules(8).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= 129 -> 0 <= element(fld_domainname(ptr_record), [
          i___1]) and element(fld_domainname(ptr_record), [i___1]) <= 255)
-S-  Applied substitution rule set_ttl_data_rules(17).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          dns_types__packet_bytes_range__last -> dns_types__byte__first <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 
          dns_types__byte__last)
<S>  New H5:  start_byte >= 1
<S>  New H27:  start_byte + 5 + loop__1__i >= 1
<S>  New H31:  loop__1__i >= 1
-S-  Applied substitution rule set_ttl_data_rules(18).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H1:  start_byte <= 8174 - current_name_length
<S>  New H6:  start_byte <= 8180
<S>  New H28:  start_byte + 5 + loop__1__i <= 8180
<S>  New H32:  loop__1__i <= 8180
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 
          dns_types__byte__first <= element(bytes, [i___1]) and element(bytes, [
          i___1]) <= dns_types__byte__last)
-S-  Applied substitution rule set_ttl_data_rules(19).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__first by:
          - 2147483648.
<S>  New H29:  start_byte + 5 + loop__1__i >= - 2147483648
<S>  New H33:  start_byte >= - 2147483653
-S-  Applied substitution rule set_ttl_data_rules(20).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__last by:
          2147483647.
<S>  New H30:  start_byte + 5 + loop__1__i <= 2147483647
<S>  New H34:  start_byte <= 2147483642
-S-  Applied substitution rule set_ttl_data_rules(23).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H21:  element(fld_domainname(ptr_record), [loop__1__i]) >= 0
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 
          dns_types__byte__last)
-S-  Applied substitution rule set_ttl_data_rules(24).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H22:  element(fld_domainname(ptr_record), [loop__1__i]) <= 255
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
-S-  Applied substitution rule set_ttl_data_rules(35).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H7:  fld_ttlinseconds(fld_inherit(ptr_record)) >= 0
-S-  Applied substitution rule set_ttl_data_rules(36).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H8:  fld_ttlinseconds(fld_inherit(ptr_record)) <= 4294967295
-S-  Applied substitution rule set_ttl_data_rules(41).
     This was achieved by replacing all occurrences of 
          rr_type__classtype__first by:
          rr_type__internet.
<S>  New H9:  rr_type__internet <= fld_class(fld_inherit(ptr_record))
-S-  Applied substitution rule set_ttl_data_rules(42).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H10:  fld_class(fld_inherit(ptr_record)) <= rr_type__hs
-S-  Applied substitution rule set_ttl_data_rules(68).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H2:  loop__1__i >= 1
<S>  New H12:  current_name_length >= 1
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(fld_domainname(ptr_record), [i___1]) and element(
          fld_domainname(ptr_record), [i___1]) <= 255)
%%%  Hypotheses H20 & H35 together imply that
          loop__1__i < current_name_length.
     H20 & H35 have therefore been deleted and a new H36 added to this effect.
***  Proved C20:  loop__1__i + 1 <= current_name_length
     via its standard form, which is:
     Std.Fm C20:  current_name_length - loop__1__i > 0
     using hypothesis H36.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_set_ttl_data_ptr_response_7.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  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(bytes, [i___1]) and element(bytes, [
          i___1]) <= dns_types__byte__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  rr_type__classtype__first <= fld_class(fld_inherit(ptr_record))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(fld_domainname(ptr_record), [i___1]) and 
          element(fld_domainname(ptr_record), [i___1]) <= character__last)
---  Hypothesis H15 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H1)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H3)
          .
***  Proved C5:  loop__1__i >= rr_type__wirestringtypeindex__first
     using hypothesis H2.
***  Proved C6:  loop__1__i <= rr_type__wirestringtypeindex__last
     using hypothesis H3.
***  Proved C7:  start_byte + 5 + loop__1__i >= 
          dns_types__packet_bytes_range__first
     using hypotheses H5 & H19.
-S-  Applied substitution rule set_ttl_data_rules(23).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New H4:  for_all(i___1 : integer, dns_types__packet_bytes_range__first <= 
          i___1 and i___1 <= dns_types__packet_bytes_range__last -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 
          dns_types__byte__last)
<S>  New C1:  element(fld_domainname(ptr_record), [loop__1__i]) >= 0
<S>  New C3:  element(fld_domainname(ptr_record), [loop__1__i]) >= 0
-S-  Applied substitution rule set_ttl_data_rules(24).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New H4:  for_all(i___1 : integer, dns_types__packet_bytes_range__first <= 
          i___1 and i___1 <= dns_types__packet_bytes_range__last -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
<S>  New C2:  element(fld_domainname(ptr_record), [loop__1__i]) <= 255
<S>  New C4:  element(fld_domainname(ptr_record), [loop__1__i]) <= 255
-S-  Applied substitution rule set_ttl_data_rules(18).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__last by:
          8180.
<S>  New H1:  start_byte <= 8174 - current_name_length
<S>  New H6:  start_byte <= 8180
<S>  New H4:  for_all(i___1 : integer, dns_types__packet_bytes_range__first <= 
          i___1 and i___1 <= 8180 -> 0 <= element(bytes, [i___1]) and element(
          bytes, [i___1]) <= 255)
<S>  New C8:  start_byte + 5 + loop__1__i <= 8180
<S>  New C12:  loop__1__i <= 8180
-S-  Applied substitution rule set_ttl_data_rules(19).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__first by:
          - 2147483648.
<S>  New C9:  start_byte + 5 + loop__1__i >= - 2147483648
<S>  New C13:  start_byte >= - 2147483653
-S-  Applied substitution rule set_ttl_data_rules(20).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__base__last by:
          2147483647.
<S>  New C10:  start_byte + 5 + loop__1__i <= 2147483647
<S>  New C14:  start_byte <= 2147483642
-S-  Applied substitution rule set_ttl_data_rules(17).
     This was achieved by replacing all occurrences of 
          dns_types__packet_bytes_range__first by:
          1.
<S>  New H5:  start_byte >= 1
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 8180 -> 0 <= 
          element(bytes, [i___1]) and element(bytes, [i___1]) <= 255)
<S>  New C11:  loop__1__i >= 1
***  Proved C9:  start_byte + 5 + loop__1__i >= - 2147483648
     using hypotheses H5 & H19.
***  Proved C13:  start_byte >= - 2147483653
     using hypothesis H5.
***  Proved C14:  start_byte <= 2147483642
     using hypothesis H6.
***  Proved C11:  loop__1__i >= 1
     using hypothesis H19.
-S-  Applied substitution rule set_ttl_data_rules(7).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
          ptr_record), [i___1]) <= character__last)
-S-  Applied substitution rule set_ttl_data_rules(8).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H11:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          fld_domainname(ptr_record), [i___1]) and element(fld_domainname(
          ptr_record), [i___1]) <= 255)
-S-  Applied substitution rule set_ttl_data_rules(35).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H7:  fld_ttlinseconds(fld_inherit(ptr_record)) >= 0
-S-  Applied substitution rule set_ttl_data_rules(36).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H8:  fld_ttlinseconds(fld_inherit(ptr_record)) <= 4294967295
-S-  Applied substitution rule set_ttl_data_rules(41).
     This was achieved by replacing all occurrences of 
          rr_type__classtype__first by:
          rr_type__internet.
<S>  New H9:  rr_type__internet <= fld_class(fld_inherit(ptr_record))
-S-  Applied substitution rule set_ttl_data_rules(42).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H10:  fld_class(fld_inherit(ptr_record)) <= rr_type__hs
-S-  Applied substitution rule set_ttl_data_rules(68).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H2:  loop__1__i >= 1
<S>  New H12:  current_name_length >= 1
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(fld_domainname(
          ptr_record), [i___1]) and element(fld_domainname(ptr_record), [i___1])
           <= 255)
-S-  Applied substitution rule set_ttl_data_rules(69).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H3:  loop__1__i <= 129
<S>  New H13:  current_name_length <= 129
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(fld_domainname(ptr_record), [i___1]) and element(
          fld_domainname(ptr_record), [i___1]) <= 255)
***  Proved C1:  element(fld_domainname(ptr_record), [loop__1__i]) >= 0
     using hypotheses H3, H11 & H19.
***  Proved C3:  element(fld_domainname(ptr_record), [loop__1__i]) >= 0
     using hypotheses H3, H11 & H19.
***  Proved C2:  element(fld_domainname(ptr_record), [loop__1__i]) <= 255
     using hypotheses H3, H11 & H19.
***  Proved C4:  element(fld_domainname(ptr_record), [loop__1__i]) <= 255
     using hypotheses H3, H11 & H19.
***  Proved C12:  loop__1__i <= 8180
     using hypothesis H3.
***  Proved C10:  start_byte + 5 + loop__1__i <= 2147483647
     using hypotheses H3 & H6.
---  Eliminated hypothesis H15 (true-hypothesis).
---  Eliminated hypothesis H16 (true-hypothesis).
---  Eliminated hypothesis H17 (true-hypothesis).
---  Eliminated hypothesis H18 (true-hypothesis).
---  Eliminated hypothesis H19 (duplicate of H2).
---  Eliminated hypothesis H6 (redundant, given H1 & H12).
---  Eliminated hypothesis H14 (redundant, given H12).
     +++  New H21:  integer__size >= 0
     +++  New H22:  character__size >= 0
     +++  New H23:  positive__size >= 0
     +++  New H24:  dns_types__packet_bytes_range__size >= 0
     +++  New H25:  unsigned_types__unsigned16__size >= 0
     +++  New H26:  unsigned_types__unsigned32__size >= 0
     +++  New H27:  rr_type__classtype__size >= 0
     +++  New H28:  rr_type__wirestringtypeindex__size >= 0
     +++  New H29:  rr_type__wirestringtype__size >= 0
     +++  New H30:  rr_type__resourcerecordtype__size >= 0
     +++  New H31:  rr_type__ptr_record_type__ptrrecordtype__size >= 0


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


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

