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

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



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

procedure Parser_Utilities.AddToKey






@@@@@@@@@@  VC: procedure_addtokey_1.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
-S-  Applied substitution rule addtokey_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H14:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> character__first <= element(s, [
          i___1]) and element(s, [i___1]) <= character__last)
<S>  New H15:  length >= 1
<S>  New C1:  true
-S-  Applied substitution rule addtokey_rules(66).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H16:  length <= 256
<S>  New H14:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 
          character__first <= element(s, [i___1]) and element(s, [i___1]) <= 
          character__last)
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_2.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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).
***  Proved C1:  1 < length -> 1 >= rr_type__linelengthindex__first and 1 <= 
          rr_type__linelengthindex__last
     using hypotheses H17 & H18.
***  Proved C2:  1 < length -> 1 >= rr_type__linelengthindex__first and 1 <= 
          rr_type__linelengthindex__last
     using hypotheses H17 & H18.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_3.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H16 on reading formula in, to give:
     %%%  H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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).
***  Proved C1:  begidx + 1 < length -> begidx + 1 >= 
          rr_type__linelengthindex__first and begidx + 1 <= 
          rr_type__linelengthindex__last
     using hypotheses H21 & H22.
***  Proved C2:  begidx + 1 < length -> begidx + 1 >= 
          rr_type__linelengthindex__first and begidx + 1 <= 
          rr_type__linelengthindex__last
     using hypotheses H21 & H22.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_4.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H21).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  true
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified C13 on reading formula in, to give:
     %%%  C13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified C16 on reading formula in, to give:
     %%%  C16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
***  Proved C1:  true
***  Proved C2:  1 < length
     using hypothesis H23.
***  Proved C3:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
          unsigned_types__unsigned32__first
     using hypothesis H1.
***  Proved C4:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
          unsigned_types__unsigned32__last
     using hypothesis H2.
***  Proved C5:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
     using hypothesis H3.
***  Proved C6:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__classtype__last
     using hypothesis H4.
***  Proved C7:  fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first
     using hypothesis H5.
***  Proved C8:  fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last
     using hypothesis H6.
***  Proved C9:  fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H7.
***  Proved C10:  fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H8.
***  Proved C11:  fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H9.
***  Proved C12:  fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H10.
***  Proved C13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
     using hypothesis H11.
***  Proved C14:  fld_keylength(dnskey_rec) >= 
          rr_type__dnskey_record_type__keylengthvaluetype__first
     using hypothesis H12.
***  Proved C15:  fld_keylength(dnskey_rec) <= 
          rr_type__dnskey_record_type__keylengthvaluetype__last
     using hypothesis H13.
***  Proved C16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
     using hypothesis H14.
***  Proved C17:  length >= rr_type__linelengthindex__first
     using hypothesis H15.
***  Proved C18:  length <= rr_type__linelengthindex__last
     using hypothesis H16.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_5.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H16 on reading formula in, to give:
     %%%  H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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 H26 has been replaced by "true".  (It is already present, as 
          H25).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  begidx >= 0
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified C13 on reading formula in, to give:
     %%%  C13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified C16 on reading formula in, to give:
     %%%  C16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
***  Proved C1:  begidx >= 0
     using hypothesis H1.
***  Proved C2:  begidx + 1 < length
     using hypothesis H27.
***  Proved C3:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
          unsigned_types__unsigned32__first
     using hypothesis H3.
***  Proved C4:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
          unsigned_types__unsigned32__last
     using hypothesis H4.
***  Proved C5:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
     using hypothesis H5.
***  Proved C6:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__classtype__last
     using hypothesis H6.
***  Proved C7:  fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first
     using hypothesis H7.
***  Proved C8:  fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last
     using hypothesis H8.
***  Proved C9:  fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H9.
***  Proved C10:  fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H10.
***  Proved C11:  fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H11.
***  Proved C12:  fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H12.
***  Proved C13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
     using hypothesis H13.
***  Proved C14:  fld_keylength(dnskey_rec) >= 
          rr_type__dnskey_record_type__keylengthvaluetype__first
     using hypothesis H14.
***  Proved C15:  fld_keylength(dnskey_rec) <= 
          rr_type__dnskey_record_type__keylengthvaluetype__last
     using hypothesis H15.
***  Proved C16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
     using hypothesis H16.
***  Proved C17:  length >= rr_type__linelengthindex__first
     using hypothesis H17.
***  Proved C18:  length <= rr_type__linelengthindex__last
     using hypothesis H18.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_6.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H16 on reading formula in, to give:
     %%%  H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
***  Proved C1:  begidx + 1 >= rr_type__linelengthindex__first
     using hypothesis H19.
-S-  Applied substitution rule addtokey_rules(66).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= 256 -> character__first <= element(s, [i___1]) and 
          element(s, [i___1]) <= character__last)
<S>  New H18:  length <= 256
<S>  New H20:  begidx <= 256
<S>  New C2:  begidx <= 255
***  Proved C2:  begidx <= 255
     using hypotheses H2 & H18.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_7.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H18).
***  Proved C1:  1 >= rr_type__linelengthindex__first
     using hypothesis H17.
***  Proved C2:  1 <= rr_type__linelengthindex__last
     using hypothesis H18.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_8.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H16 on reading formula in, to give:
     %%%  H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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 H26 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H22).
***  Proved C1:  begidx + 1 >= rr_type__linelengthindex__first
     using hypothesis H21.
***  Proved C2:  begidx + 1 <= rr_type__linelengthindex__last
     using hypothesis H22.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_9.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H18).
***  Proved C1:  1 < length -> 1 >= rr_type__linelengthindex__first and 1 <= 
          rr_type__linelengthindex__last
     using hypothesis H21.
***  Proved C2:  1 < length -> 1 >= rr_type__linelengthindex__first and 1 <= 
          rr_type__linelengthindex__last
     using hypothesis H21.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_10.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H16 on reading formula in, to give:
     %%%  H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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 H26 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H22).
***  Proved C1:  begidx + 1 < length -> begidx + 1 >= 
          rr_type__linelengthindex__first and begidx + 1 <= 
          rr_type__linelengthindex__last
     using hypothesis H25.
***  Proved C2:  begidx + 1 < length -> begidx + 1 >= 
          rr_type__linelengthindex__first and begidx + 1 <= 
          rr_type__linelengthindex__last
     using hypothesis H25.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_11.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H18 on reading formula in, to give:
     %%%  H18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__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).
***  Proved C1:  endidx + 1 < length -> endidx + 1 >= 
          rr_type__linelengthindex__first and endidx + 1 <= 
          rr_type__linelengthindex__last
     using hypotheses H23 & H24.
***  Proved C2:  endidx + 1 < length -> endidx + 1 >= 
          rr_type__linelengthindex__first and endidx + 1 <= 
          rr_type__linelengthindex__last
     using hypotheses H23 & H24.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_12.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H21).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  true
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  true
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  true
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified C15 on reading formula in, to give:
     %%%  C15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified C18 on reading formula in, to give:
     %%%  C18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
***  Proved C1:  true
***  Proved C2:  true
***  Proved C3:  true
***  Proved C4:  1 < length
     using hypothesis H32.
***  Proved C5:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
          unsigned_types__unsigned32__first
     using hypothesis H1.
***  Proved C6:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
          unsigned_types__unsigned32__last
     using hypothesis H2.
***  Proved C7:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
     using hypothesis H3.
***  Proved C8:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__classtype__last
     using hypothesis H4.
***  Proved C9:  fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first
     using hypothesis H5.
***  Proved C10:  fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last
     using hypothesis H6.
***  Proved C11:  fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H7.
***  Proved C12:  fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H8.
***  Proved C13:  fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H9.
***  Proved C14:  fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H10.
***  Proved C15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
     using hypothesis H11.
***  Proved C16:  fld_keylength(dnskey_rec) >= 
          rr_type__dnskey_record_type__keylengthvaluetype__first
     using hypothesis H12.
***  Proved C17:  fld_keylength(dnskey_rec) <= 
          rr_type__dnskey_record_type__keylengthvaluetype__last
     using hypothesis H13.
***  Proved C18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
     using hypothesis H14.
***  Proved C19:  length >= rr_type__linelengthindex__first
     using hypothesis H15.
***  Proved C20:  length <= rr_type__linelengthindex__last
     using hypothesis H16.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_13.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H16 on reading formula in, to give:
     %%%  H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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 H26 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H25).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  begidx >= 0
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  true
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  begidx >= 0
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified C15 on reading formula in, to give:
     %%%  C15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified C18 on reading formula in, to give:
     %%%  C18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
***  Proved C1:  begidx >= 0
     using hypothesis H1.
***  Proved C2:  true
***  Proved C3:  begidx >= 0
     using hypothesis H1.
***  Proved C4:  begidx + 1 < length
     using hypothesis H36.
***  Proved C5:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
          unsigned_types__unsigned32__first
     using hypothesis H3.
***  Proved C6:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
          unsigned_types__unsigned32__last
     using hypothesis H4.
***  Proved C7:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
     using hypothesis H5.
***  Proved C8:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__classtype__last
     using hypothesis H6.
***  Proved C9:  fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first
     using hypothesis H7.
***  Proved C10:  fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last
     using hypothesis H8.
***  Proved C11:  fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H9.
***  Proved C12:  fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H10.
***  Proved C13:  fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H11.
***  Proved C14:  fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H12.
***  Proved C15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
     using hypothesis H13.
***  Proved C16:  fld_keylength(dnskey_rec) >= 
          rr_type__dnskey_record_type__keylengthvaluetype__first
     using hypothesis H14.
***  Proved C17:  fld_keylength(dnskey_rec) <= 
          rr_type__dnskey_record_type__keylengthvaluetype__last
     using hypothesis H15.
***  Proved C18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
     using hypothesis H16.
***  Proved C19:  length >= rr_type__linelengthindex__first
     using hypothesis H17.
***  Proved C20:  length <= rr_type__linelengthindex__last
     using hypothesis H18.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_14.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H18 on reading formula in, to give:
     %%%  H18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__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).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H27).
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  endidx >= 0
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified C15 on reading formula in, to give:
     %%%  C15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified C18 on reading formula in, to give:
     %%%  C18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
***  Proved C1:  begidx >= 1
     using hypothesis H1.
***  Proved C2:  begidx <= endidx + 1
     using hypothesis H2.
***  Proved C3:  endidx >= 0
     using hypothesis H3.
***  Proved C4:  endidx + 1 < length
     using hypothesis H29.
***  Proved C5:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
          unsigned_types__unsigned32__first
     using hypothesis H5.
***  Proved C6:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
          unsigned_types__unsigned32__last
     using hypothesis H6.
***  Proved C7:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
     using hypothesis H7.
***  Proved C8:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__classtype__last
     using hypothesis H8.
***  Proved C9:  fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first
     using hypothesis H9.
***  Proved C10:  fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last
     using hypothesis H10.
***  Proved C11:  fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H11.
***  Proved C12:  fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H12.
***  Proved C13:  fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H13.
***  Proved C14:  fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H14.
***  Proved C15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
     using hypothesis H15.
***  Proved C16:  fld_keylength(dnskey_rec) >= 
          rr_type__dnskey_record_type__keylengthvaluetype__first
     using hypothesis H16.
***  Proved C17:  fld_keylength(dnskey_rec) <= 
          rr_type__dnskey_record_type__keylengthvaluetype__last
     using hypothesis H17.
***  Proved C18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
     using hypothesis H18.
***  Proved C19:  length >= rr_type__linelengthindex__first
     using hypothesis H19.
***  Proved C20:  length <= rr_type__linelengthindex__last
     using hypothesis H20.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_15.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H18 on reading formula in, to give:
     %%%  H18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
***  Proved C1:  endidx + 1 >= rr_type__linelengthindex__first
     using hypothesis H21.
-S-  Applied substitution rule addtokey_rules(66).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= 256 -> character__first <= element(s, [i___1]) and 
          element(s, [i___1]) <= character__last)
<S>  New H20:  length <= 256
<S>  New H22:  endidx <= 256
<S>  New C2:  endidx <= 255
***  Proved C2:  endidx <= 255
     using hypotheses H4 & H20.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_16.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  fld_keylength(dnskey_rec) + 1 >= integer__base__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  fld_keylength(dnskey_rec) + 1 <= integer__base__last
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  1 >= integer__base__first
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  1 <= integer__base__last
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  0 >= integer__base__first
%%%  Simplified C6 on reading formula in, to give:
     %%%  C6:  0 <= integer__base__last
-S-  Applied substitution rule addtokey_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C1:  fld_keylength(dnskey_rec) >= - 2147483649
<S>  New C3:  true
<S>  New C5:  true
-S-  Applied substitution rule addtokey_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C2:  fld_keylength(dnskey_rec) <= 2147483646
<S>  New C4:  true
<S>  New C6:  true
***  Proved C3:  true
***  Proved C5:  true
***  Proved C4:  true
***  Proved C6:  true
>>>  Restructured hypothesis H23 into:
     >>>  H23:  length <= 1 or element(s, [1]) <> blank and element(s, [1]) <> 
          tab
>>>  Restructured hypothesis H32 into:
     >>>  H32:  length <= 1 or (element(s, [1]) = blank or element(s, [1]) = 
          tab)
-S-  Applied substitution rule addtokey_rules(2).
     This was achieved by replacing all occurrences of blank by:
          32.
<S>  New H23:  length <= 1 or element(s, [1]) <> 32 and element(s, [1]) <> tab
<S>  New H32:  length <= 1 or (element(s, [1]) = 32 or element(s, [1]) = tab)
-S-  Applied substitution rule addtokey_rules(3).
     This was achieved by replacing all occurrences of tab by:
          9.
<S>  New H23:  length <= 1 or element(s, [1]) <> 32 and element(s, [1]) <> 9
<S>  New H32:  length <= 1 or (element(s, [1]) = 32 or element(s, [1]) = 9)
-S-  Applied substitution rule addtokey_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H11:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= character__last)
<S>  New H14:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= character__last)
-S-  Applied substitution rule addtokey_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H11:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= 255)
<S>  New H14:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(20).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__first by:
          0.
<S>  New H7:  fld_protocol(dnskey_rec) >= 0
<S>  New H9:  fld_algorithm(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(21).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__last by:
          255.
<S>  New H8:  fld_protocol(dnskey_rec) <= 255
<S>  New H10:  fld_algorithm(dnskey_rec) <= 255
-S-  Applied substitution rule addtokey_rules(26).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New H5:  fld_flags(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New H6:  fld_flags(dnskey_rec) <= 65535
-S-  Applied substitution rule addtokey_rules(32).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H1:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 0
-S-  Applied substitution rule addtokey_rules(33).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H2:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 4294967295
-S-  Applied substitution rule addtokey_rules(38).
     This was achieved by replacing all occurrences of 
          rr_type__classtype__first by:
          rr_type__internet.
<S>  New H3:  rr_type__internet <= fld_class(fld_inherit(dnskey_rec))
-S-  Applied substitution rule addtokey_rules(39).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H4:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__hs
-S-  Applied substitution rule addtokey_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H15:  length >= 1
<S>  New H17:  true
<S>  New H21:  1 < length -> 1 <= rr_type__linelengthindex__last
<S>  New H14:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(s, [i___1]) and 
          element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(66).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H16:  length <= 256
<S>  New H18:  true
<S>  New H21:  true
<S>  New H14:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(s, [i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(72).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__first by:
          0.
<S>  New H12:  fld_keylength(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(73).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__last by:
          1365.
<S>  New H13:  fld_keylength(dnskey_rec) <= 1365
-S-  Applied substitution rule addtokey_rules(77).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first by:
          1.
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(78).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last by:
          1365.
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
***  Proved C1:  fld_keylength(dnskey_rec) >= - 2147483649
     using hypothesis H12.
***  Proved C2:  fld_keylength(dnskey_rec) <= 2147483646
     using hypothesis H13.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_17.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H16 on reading formula in, to give:
     %%%  H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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 H26 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H22).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  fld_keylength(dnskey_rec) + 1 >= integer__base__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  fld_keylength(dnskey_rec) + 1 <= integer__base__last
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  1 >= integer__base__first
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  1 <= integer__base__last
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  0 >= integer__base__first
%%%  Simplified C6 on reading formula in, to give:
     %%%  C6:  0 <= integer__base__last
-S-  Applied substitution rule addtokey_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C1:  fld_keylength(dnskey_rec) >= - 2147483649
<S>  New C3:  true
<S>  New C5:  true
-S-  Applied substitution rule addtokey_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C2:  fld_keylength(dnskey_rec) <= 2147483646
<S>  New C4:  true
<S>  New C6:  true
***  Proved C3:  true
***  Proved C5:  true
***  Proved C4:  true
***  Proved C6:  true
>>>  Restructured hypothesis H27 into:
     >>>  H27:  length <= begidx + 1 or element(s, [begidx + 1]) <> blank and 
          element(s, [begidx + 1]) <> tab
>>>  Restructured hypothesis H36 into:
     >>>  H36:  length <= begidx + 1 or (element(s, [begidx + 1]) = blank or 
          element(s, [begidx + 1]) = tab)
-S-  Applied substitution rule addtokey_rules(2).
     This was achieved by replacing all occurrences of blank by:
          32.
<S>  New H27:  length <= begidx + 1 or element(s, [begidx + 1]) <> 32 and 
          element(s, [begidx + 1]) <> tab
<S>  New H36:  length <= begidx + 1 or (element(s, [begidx + 1]) = 32 or 
          element(s, [begidx + 1]) = tab)
-S-  Applied substitution rule addtokey_rules(3).
     This was achieved by replacing all occurrences of tab by:
          9.
<S>  New H27:  length <= begidx + 1 or element(s, [begidx + 1]) <> 32 and 
          element(s, [begidx + 1]) <> 9
<S>  New H36:  length <= begidx + 1 or (element(s, [begidx + 1]) = 32 or 
          element(s, [begidx + 1]) = 9)
-S-  Applied substitution rule addtokey_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= character__last)
<S>  New H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= character__last)
-S-  Applied substitution rule addtokey_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= 255)
<S>  New H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(20).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__first by:
          0.
<S>  New H9:  fld_protocol(dnskey_rec) >= 0
<S>  New H11:  fld_algorithm(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(21).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__last by:
          255.
<S>  New H10:  fld_protocol(dnskey_rec) <= 255
<S>  New H12:  fld_algorithm(dnskey_rec) <= 255
-S-  Applied substitution rule addtokey_rules(26).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New H7:  fld_flags(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New H8:  fld_flags(dnskey_rec) <= 65535
-S-  Applied substitution rule addtokey_rules(32).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H3:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 0
-S-  Applied substitution rule addtokey_rules(33).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H4:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 4294967295
-S-  Applied substitution rule addtokey_rules(38).
     This was achieved by replacing all occurrences of 
          rr_type__classtype__first by:
          rr_type__internet.
<S>  New H5:  rr_type__internet <= fld_class(fld_inherit(dnskey_rec))
-S-  Applied substitution rule addtokey_rules(39).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H6:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__hs
-S-  Applied substitution rule addtokey_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H17:  length >= 1
<S>  New H19:  begidx >= 1
<S>  New H21:  begidx >= 0
<S>  New H25:  begidx + 1 < length -> begidx >= 0 and begidx + 1 <= 
          rr_type__linelengthindex__last
<S>  New H16:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(s, [i___1]) and 
          element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(66).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H18:  length <= 256
<S>  New H20:  begidx <= 256
<S>  New H22:  begidx <= 255
<S>  New H25:  begidx + 1 < length -> begidx >= 0 and begidx <= 255
<S>  New H16:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(s, [i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(72).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__first by:
          0.
<S>  New H14:  fld_keylength(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(73).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__last by:
          1365.
<S>  New H15:  fld_keylength(dnskey_rec) <= 1365
-S-  Applied substitution rule addtokey_rules(77).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first by:
          1.
<S>  New H13:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(78).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last by:
          1365.
<S>  New H13:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
***  Proved C1:  fld_keylength(dnskey_rec) >= - 2147483649
     using hypothesis H14.
***  Proved C2:  fld_keylength(dnskey_rec) <= 2147483646
     using hypothesis H15.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_18.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H18 on reading formula in, to give:
     %%%  H18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__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).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H24).
-S-  Applied substitution rule addtokey_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C1:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) >= - 
          2147483648
<S>  New C3:  endidx + 1 - begidx >= - 2147483649
<S>  New C5:  endidx + 1 - begidx >= - 2147483648
-S-  Applied substitution rule addtokey_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C2:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 
          2147483647
<S>  New C4:  endidx + 1 - begidx <= 2147483646
<S>  New C6:  endidx + 1 - begidx <= 2147483647
***  Proved C3:  endidx + 1 - begidx >= - 2147483649
     using hypothesis H2.
***  Proved C5:  endidx + 1 - begidx >= - 2147483648
     using hypothesis H2.
>>>  Restructured hypothesis H29 into:
     >>>  H29:  length <= endidx + 1 or (element(s, [endidx + 1]) = blank or 
          element(s, [endidx + 1]) = tab)
-S-  Applied substitution rule addtokey_rules(2).
     This was achieved by replacing all occurrences of blank by:
          32.
<S>  New H29:  length <= endidx + 1 or (element(s, [endidx + 1]) = 32 or 
          element(s, [endidx + 1]) = tab)
-S-  Applied substitution rule addtokey_rules(3).
     This was achieved by replacing all occurrences of tab by:
          9.
<S>  New H29:  length <= endidx + 1 or (element(s, [endidx + 1]) = 32 or 
          element(s, [endidx + 1]) = 9)
-S-  Applied substitution rule addtokey_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= character__last)
<S>  New H18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= character__last)
-S-  Applied substitution rule addtokey_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= 255)
<S>  New H18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(20).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__first by:
          0.
<S>  New H11:  fld_protocol(dnskey_rec) >= 0
<S>  New H13:  fld_algorithm(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(21).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__last by:
          255.
<S>  New H12:  fld_protocol(dnskey_rec) <= 255
<S>  New H14:  fld_algorithm(dnskey_rec) <= 255
-S-  Applied substitution rule addtokey_rules(26).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New H9:  fld_flags(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New H10:  fld_flags(dnskey_rec) <= 65535
-S-  Applied substitution rule addtokey_rules(32).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H5:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 0
-S-  Applied substitution rule addtokey_rules(33).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H6:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 4294967295
-S-  Applied substitution rule addtokey_rules(38).
     This was achieved by replacing all occurrences of 
          rr_type__classtype__first by:
          rr_type__internet.
<S>  New H7:  rr_type__internet <= fld_class(fld_inherit(dnskey_rec))
-S-  Applied substitution rule addtokey_rules(39).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H8:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__hs
-S-  Applied substitution rule addtokey_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H19:  length >= 1
<S>  New H21:  endidx >= 1
<S>  New H23:  endidx >= 0
<S>  New H27:  endidx + 1 < length -> endidx >= 0 and endidx + 1 <= 
          rr_type__linelengthindex__last
<S>  New H30:  begidx >= 1
<S>  New H18:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(s, [i___1]) and 
          element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(66).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H20:  length <= 256
<S>  New H22:  endidx <= 256
<S>  New H24:  endidx <= 255
<S>  New H31:  begidx <= 256
<S>  New H27:  endidx + 1 < length -> endidx >= 0 and endidx <= 255
<S>  New H18:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(s, [i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(72).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__first by:
          0.
<S>  New H16:  fld_keylength(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(73).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__last by:
          1365.
<S>  New H17:  fld_keylength(dnskey_rec) <= 1365
-S-  Applied substitution rule addtokey_rules(77).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first by:
          1.
<S>  New H15:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(78).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last by:
          1365.
<S>  New H15:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
***  Proved C1:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) >= - 
          2147483648
     using hypotheses H2 & H16.
***  Proved C2:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 
          2147483647
     using hypotheses H1, H17 & H22.
***  Proved C4:  endidx + 1 - begidx <= 2147483646
     using hypotheses H1 & H22.
***  Proved C6:  endidx + 1 - begidx <= 2147483647
     using hypotheses H1 & H22.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_19.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified H37 on reading formula in, to give:
     %%%  H37:  fld_keylength(dnskey_rec) + 1 >= integer__base__first
%%%  Simplified H38 on reading formula in, to give:
     %%%  H38:  fld_keylength(dnskey_rec) + 1 <= integer__base__last
%%%  Simplified H39 on reading formula in, to give:
     %%%  H39:  1 >= integer__base__first
%%%  Simplified H40 on reading formula in, to give:
     %%%  H40:  1 <= integer__base__last
%%%  Simplified H41 on reading formula in, to give:
     %%%  H41:  0 >= integer__base__first
%%%  Simplified H42 on reading formula in, to give:
     %%%  H42:  0 <= integer__base__last
%%%  Simplified H43 on reading formula in, to give:
     %%%  H43:  not fld_keylength(dnskey_rec) + 1 > 
          rr_type__dnskey_record_type__maxdnskeylength
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H18).
-S-  Applied substitution rule addtokey_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C1:  true
<S>  New C3:  true
-S-  Applied substitution rule addtokey_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C2:  true
<S>  New C4:  true
***  Proved C1:  true
***  Proved C3:  true
***  Proved C2:  true
***  Proved C4:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_20.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H16 on reading formula in, to give:
     %%%  H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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 H26 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H22).
%%%  Simplified H41 on reading formula in, to give:
     %%%  H41:  fld_keylength(dnskey_rec) + 1 >= integer__base__first
%%%  Simplified H42 on reading formula in, to give:
     %%%  H42:  fld_keylength(dnskey_rec) + 1 <= integer__base__last
%%%  Simplified H43 on reading formula in, to give:
     %%%  H43:  1 >= integer__base__first
%%%  Simplified H44 on reading formula in, to give:
     %%%  H44:  1 <= integer__base__last
%%%  Simplified H45 on reading formula in, to give:
     %%%  H45:  0 >= integer__base__first
%%%  Simplified H46 on reading formula in, to give:
     %%%  H46:  0 <= integer__base__last
%%%  Simplified H47 on reading formula in, to give:
     %%%  H47:  not fld_keylength(dnskey_rec) + 1 > 
          rr_type__dnskey_record_type__maxdnskeylength
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H22).
-S-  Applied substitution rule addtokey_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C1:  begidx >= - 2147483649
<S>  New C3:  begidx >= - 2147483649
-S-  Applied substitution rule addtokey_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C2:  begidx <= 2147483646
<S>  New C4:  begidx <= 2147483646
***  Proved C1:  begidx >= - 2147483649
     using hypothesis H1.
***  Proved C3:  begidx >= - 2147483649
     using hypothesis H1.
>>>  Restructured hypothesis H27 into:
     >>>  H27:  length <= begidx + 1 or element(s, [begidx + 1]) <> blank and 
          element(s, [begidx + 1]) <> tab
>>>  Restructured hypothesis H36 into:
     >>>  H36:  length <= begidx + 1 or (element(s, [begidx + 1]) = blank or 
          element(s, [begidx + 1]) = tab)
>>>  Restructured hypothesis H47 into:
     >>>  H47:  fld_keylength(dnskey_rec) + 1 <= 
          rr_type__dnskey_record_type__maxdnskeylength
-S-  Applied substitution rule addtokey_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__maxdnskeylength by:
          1365.
<S>  New H47:  fld_keylength(dnskey_rec) <= 1364
-S-  Applied substitution rule addtokey_rules(2).
     This was achieved by replacing all occurrences of blank by:
          32.
<S>  New H27:  length <= begidx + 1 or element(s, [begidx + 1]) <> 32 and 
          element(s, [begidx + 1]) <> tab
<S>  New H36:  length <= begidx + 1 or (element(s, [begidx + 1]) = 32 or 
          element(s, [begidx + 1]) = tab)
-S-  Applied substitution rule addtokey_rules(3).
     This was achieved by replacing all occurrences of tab by:
          9.
<S>  New H27:  length <= begidx + 1 or element(s, [begidx + 1]) <> 32 and 
          element(s, [begidx + 1]) <> 9
<S>  New H36:  length <= begidx + 1 or (element(s, [begidx + 1]) = 32 or 
          element(s, [begidx + 1]) = 9)
-S-  Applied substitution rule addtokey_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H41:  fld_keylength(dnskey_rec) >= - 2147483649
<S>  New H43:  true
<S>  New H45:  true
-S-  Applied substitution rule addtokey_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H42:  fld_keylength(dnskey_rec) <= 2147483646
<S>  New H44:  true
<S>  New H46:  true
-S-  Applied substitution rule addtokey_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= character__last)
<S>  New H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= character__last)
-S-  Applied substitution rule addtokey_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= 255)
<S>  New H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(20).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__first by:
          0.
<S>  New H9:  fld_protocol(dnskey_rec) >= 0
<S>  New H11:  fld_algorithm(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(21).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__last by:
          255.
<S>  New H10:  fld_protocol(dnskey_rec) <= 255
<S>  New H12:  fld_algorithm(dnskey_rec) <= 255
-S-  Applied substitution rule addtokey_rules(26).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New H7:  fld_flags(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New H8:  fld_flags(dnskey_rec) <= 65535
-S-  Applied substitution rule addtokey_rules(32).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H3:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 0
-S-  Applied substitution rule addtokey_rules(33).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H4:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 4294967295
-S-  Applied substitution rule addtokey_rules(38).
     This was achieved by replacing all occurrences of 
          rr_type__classtype__first by:
          rr_type__internet.
<S>  New H5:  rr_type__internet <= fld_class(fld_inherit(dnskey_rec))
-S-  Applied substitution rule addtokey_rules(39).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H6:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__hs
-S-  Applied substitution rule addtokey_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H17:  length >= 1
<S>  New H19:  begidx >= 1
<S>  New H21:  begidx >= 0
<S>  New H25:  begidx + 1 < length -> begidx >= 0 and begidx + 1 <= 
          rr_type__linelengthindex__last
<S>  New H16:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(s, [i___1]) and 
          element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(66).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H18:  length <= 256
<S>  New H20:  begidx <= 256
<S>  New H22:  begidx <= 255
<S>  New H25:  begidx + 1 < length -> begidx >= 0 and begidx <= 255
<S>  New H16:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(s, [i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(72).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__first by:
          0.
<S>  New H14:  fld_keylength(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(73).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__last by:
          1365.
<S>  New H15:  fld_keylength(dnskey_rec) <= 1365
-S-  Applied substitution rule addtokey_rules(77).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first by:
          1.
<S>  New H13:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(78).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last by:
          1365.
<S>  New H13:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
***  Proved C2:  begidx <= 2147483646
     using hypothesis H20.
***  Proved C4:  begidx <= 2147483646
     using hypothesis H20.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_21.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H18 on reading formula in, to give:
     %%%  H18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__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).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H24).
-S-  Applied substitution rule addtokey_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C1:  endidx >= - 2147483649
<S>  New C3:  begidx >= - 2147483648
-S-  Applied substitution rule addtokey_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C2:  endidx <= 2147483646
<S>  New C4:  begidx <= 2147483647
***  Proved C1:  endidx >= - 2147483649
     using hypothesis H3.
***  Proved C3:  begidx >= - 2147483648
     using hypothesis H1.
>>>  Restructured hypothesis H29 into:
     >>>  H29:  length <= endidx + 1 or (element(s, [endidx + 1]) = blank or 
          element(s, [endidx + 1]) = tab)
>>>  Restructured hypothesis H40 into:
     >>>  H40:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 
          rr_type__dnskey_record_type__maxdnskeylength
-S-  Applied substitution rule addtokey_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__maxdnskeylength by:
          1365.
<S>  New H40:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 1365
-S-  Applied substitution rule addtokey_rules(2).
     This was achieved by replacing all occurrences of blank by:
          32.
<S>  New H29:  length <= endidx + 1 or (element(s, [endidx + 1]) = 32 or 
          element(s, [endidx + 1]) = tab)
-S-  Applied substitution rule addtokey_rules(3).
     This was achieved by replacing all occurrences of tab by:
          9.
<S>  New H29:  length <= endidx + 1 or (element(s, [endidx + 1]) = 32 or 
          element(s, [endidx + 1]) = 9)
-S-  Applied substitution rule addtokey_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H34:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) >= - 
          2147483648
<S>  New H36:  endidx + 1 - begidx >= - 2147483649
<S>  New H38:  endidx + 1 - begidx >= - 2147483648
-S-  Applied substitution rule addtokey_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H35:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 
          2147483647
<S>  New H37:  endidx + 1 - begidx <= 2147483646
<S>  New H39:  endidx + 1 - begidx <= 2147483647
-S-  Applied substitution rule addtokey_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= character__last)
<S>  New H18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= character__last)
-S-  Applied substitution rule addtokey_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= 255)
<S>  New H18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(20).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__first by:
          0.
<S>  New H11:  fld_protocol(dnskey_rec) >= 0
<S>  New H13:  fld_algorithm(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(21).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__last by:
          255.
<S>  New H12:  fld_protocol(dnskey_rec) <= 255
<S>  New H14:  fld_algorithm(dnskey_rec) <= 255
-S-  Applied substitution rule addtokey_rules(26).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New H9:  fld_flags(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New H10:  fld_flags(dnskey_rec) <= 65535
-S-  Applied substitution rule addtokey_rules(32).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H5:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 0
-S-  Applied substitution rule addtokey_rules(33).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H6:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 4294967295
-S-  Applied substitution rule addtokey_rules(38).
     This was achieved by replacing all occurrences of 
          rr_type__classtype__first by:
          rr_type__internet.
<S>  New H7:  rr_type__internet <= fld_class(fld_inherit(dnskey_rec))
-S-  Applied substitution rule addtokey_rules(39).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H8:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__hs
-S-  Applied substitution rule addtokey_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H19:  length >= 1
<S>  New H21:  endidx >= 1
<S>  New H23:  endidx >= 0
<S>  New H27:  endidx + 1 < length -> endidx >= 0 and endidx + 1 <= 
          rr_type__linelengthindex__last
<S>  New H30:  begidx >= 1
<S>  New H18:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(s, [i___1]) and 
          element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(66).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H20:  length <= 256
<S>  New H22:  endidx <= 256
<S>  New H24:  endidx <= 255
<S>  New H31:  begidx <= 256
<S>  New H27:  endidx + 1 < length -> endidx >= 0 and endidx <= 255
<S>  New H18:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(s, [i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(72).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__first by:
          0.
<S>  New H16:  fld_keylength(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(73).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__last by:
          1365.
<S>  New H17:  fld_keylength(dnskey_rec) <= 1365
-S-  Applied substitution rule addtokey_rules(77).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first by:
          1.
<S>  New H15:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(78).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last by:
          1365.
<S>  New H15:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
***  Proved C2:  endidx <= 2147483646
     using hypothesis H22.
***  Proved C4:  begidx <= 2147483647
     using hypothesis H31.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_22.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified H37 on reading formula in, to give:
     %%%  H37:  fld_keylength(dnskey_rec) + 1 >= integer__base__first
%%%  Simplified H38 on reading formula in, to give:
     %%%  H38:  fld_keylength(dnskey_rec) + 1 <= integer__base__last
%%%  Simplified H39 on reading formula in, to give:
     %%%  H39:  1 >= integer__base__first
%%%  Simplified H40 on reading formula in, to give:
     %%%  H40:  1 <= integer__base__last
%%%  Simplified H41 on reading formula in, to give:
     %%%  H41:  0 >= integer__base__first
%%%  Simplified H42 on reading formula in, to give:
     %%%  H42:  0 <= integer__base__last
%%%  Simplified H43 on reading formula in, to give:
     %%%  H43:  not fld_keylength(dnskey_rec) + 1 > 
          rr_type__dnskey_record_type__maxdnskeylength
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H49).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  1 >= integer__first and 1 <= integer__last
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  1 >= integer__first and 1 <= integer__last
***  Proved C1:  1 >= integer__first and 1 <= integer__last
     using hypotheses H48 & H49.
***  Proved C2:  1 >= integer__first and 1 <= integer__last
     using hypotheses H48 & H49.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_23.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H16 on reading formula in, to give:
     %%%  H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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 H26 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H22).
%%%  Simplified H41 on reading formula in, to give:
     %%%  H41:  fld_keylength(dnskey_rec) + 1 >= integer__base__first
%%%  Simplified H42 on reading formula in, to give:
     %%%  H42:  fld_keylength(dnskey_rec) + 1 <= integer__base__last
%%%  Simplified H43 on reading formula in, to give:
     %%%  H43:  1 >= integer__base__first
%%%  Simplified H44 on reading formula in, to give:
     %%%  H44:  1 <= integer__base__last
%%%  Simplified H45 on reading formula in, to give:
     %%%  H45:  0 >= integer__base__first
%%%  Simplified H46 on reading formula in, to give:
     %%%  H46:  0 <= integer__base__last
%%%  Simplified H47 on reading formula in, to give:
     %%%  H47:  not fld_keylength(dnskey_rec) + 1 > 
          rr_type__dnskey_record_type__maxdnskeylength
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H53).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  begidx + 1 >= integer__first and begidx + 1 <= integer__last
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  begidx + 1 >= integer__first and begidx + 1 <= integer__last
***  Proved C1:  begidx + 1 >= integer__first and begidx + 1 <= integer__last
     using hypotheses H52 & H53.
***  Proved C2:  begidx + 1 >= integer__first and begidx + 1 <= integer__last
     using hypotheses H52 & H53.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_24.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H18 on reading formula in, to give:
     %%%  H18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__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).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H24).
***  Proved C1:  begidx <= endidx + 1 -> endidx + 1 >= integer__first and 
          endidx + 1 <= integer__last
     using hypotheses H45 & H46.
***  Proved C2:  begidx <= endidx + 1 -> begidx >= integer__first and begidx <= 
          integer__last
     using hypotheses H47 & H48.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_25.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified H37 on reading formula in, to give:
     %%%  H37:  fld_keylength(dnskey_rec) + 1 >= integer__base__first
%%%  Simplified H38 on reading formula in, to give:
     %%%  H38:  fld_keylength(dnskey_rec) + 1 <= integer__base__last
%%%  Simplified H39 on reading formula in, to give:
     %%%  H39:  1 >= integer__base__first
%%%  Simplified H40 on reading formula in, to give:
     %%%  H40:  1 <= integer__base__last
%%%  Simplified H41 on reading formula in, to give:
     %%%  H41:  0 >= integer__base__first
%%%  Simplified H42 on reading formula in, to give:
     %%%  H42:  0 <= integer__base__last
%%%  Simplified H43 on reading formula in, to give:
     %%%  H43:  not fld_keylength(dnskey_rec) + 1 > 
          rr_type__dnskey_record_type__maxdnskeylength
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H49).
%%%  Simplified H52 on reading formula in, to give:
     %%%  H52:  1 >= integer__first and 1 <= integer__last
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified H58 on reading formula in, to give:
     %%%  H58:  true
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  true
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  true
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  true
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  true
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  true
%%%  Simplified C6 on reading formula in, to give:
     %%%  C6:  fld_keylength(dnskey_rec) + 1 <= 
          rr_type__dnskey_record_type__maxdnskeylength
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified C17 on reading formula in, to give:
     %%%  C17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified C20 on reading formula in, to give:
     %%%  C20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
%%%  Simplified C25 on reading formula in, to give:
     %%%  C25:  true
%%%  Simplified C26 on reading formula in, to give:
     %%%  C26:  true
***  Proved C1:  true
***  Proved C2:  true
***  Proved C3:  true
***  Proved C4:  true
***  Proved C5:  true
***  Proved C6:  fld_keylength(dnskey_rec) + 1 <= 
          rr_type__dnskey_record_type__maxdnskeylength
     using hypothesis H43.
***  Proved C7:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
          unsigned_types__unsigned32__first
     using hypothesis H1.
***  Proved C8:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
          unsigned_types__unsigned32__last
     using hypothesis H2.
***  Proved C9:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
     using hypothesis H3.
***  Proved C10:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__classtype__last
     using hypothesis H4.
***  Proved C11:  fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first
     using hypothesis H5.
***  Proved C12:  fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last
     using hypothesis H6.
***  Proved C13:  fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H7.
***  Proved C14:  fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H8.
***  Proved C15:  fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H9.
***  Proved C16:  fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H10.
***  Proved C17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
     using hypothesis H11.
***  Proved C18:  fld_keylength(dnskey_rec) >= 
          rr_type__dnskey_record_type__keylengthvaluetype__first
     using hypothesis H12.
***  Proved C19:  fld_keylength(dnskey_rec) <= 
          rr_type__dnskey_record_type__keylengthvaluetype__last
     using hypothesis H13.
***  Proved C20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
     using hypothesis H14.
***  Proved C21:  length >= rr_type__linelengthindex__first
     using hypothesis H15.
***  Proved C22:  length <= rr_type__linelengthindex__last
     using hypothesis H16.
***  Proved C23:  1 >= integer__first
     using hypothesis H48.
***  Proved C24:  1 <= integer__last
     using hypothesis H49.
***  Proved C25:  true
***  Proved C26:  true
***  Proved C27:  1 >= rr_type__linelengthindex__first
     using hypothesis H17.
***  Proved C28:  1 <= rr_type__linelengthindex__last
     using hypothesis H18.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_26.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H16 on reading formula in, to give:
     %%%  H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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 H26 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H22).
%%%  Simplified H41 on reading formula in, to give:
     %%%  H41:  fld_keylength(dnskey_rec) + 1 >= integer__base__first
%%%  Simplified H42 on reading formula in, to give:
     %%%  H42:  fld_keylength(dnskey_rec) + 1 <= integer__base__last
%%%  Simplified H43 on reading formula in, to give:
     %%%  H43:  1 >= integer__base__first
%%%  Simplified H44 on reading formula in, to give:
     %%%  H44:  1 <= integer__base__last
%%%  Simplified H45 on reading formula in, to give:
     %%%  H45:  0 >= integer__base__first
%%%  Simplified H46 on reading formula in, to give:
     %%%  H46:  0 <= integer__base__last
%%%  Simplified H47 on reading formula in, to give:
     %%%  H47:  not fld_keylength(dnskey_rec) + 1 > 
          rr_type__dnskey_record_type__maxdnskeylength
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H53).
%%%  Simplified H56 on reading formula in, to give:
     %%%  H56:  begidx + 1 >= integer__first and begidx + 1 <= integer__last
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H56).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H22).
%%%  Simplified H62 on reading formula in, to give:
     %%%  H62:  true
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  true
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  true
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  true
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  true
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  begidx >= 0
%%%  Simplified C6 on reading formula in, to give:
     %%%  C6:  fld_keylength(dnskey_rec) + 1 <= 
          rr_type__dnskey_record_type__maxdnskeylength
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified C17 on reading formula in, to give:
     %%%  C17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified C20 on reading formula in, to give:
     %%%  C20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
%%%  Simplified C25 on reading formula in, to give:
     %%%  C25:  true
%%%  Simplified C26 on reading formula in, to give:
     %%%  C26:  true
***  Proved C1:  true
***  Proved C2:  true
***  Proved C3:  true
***  Proved C4:  true
***  Proved C5:  begidx >= 0
     using hypothesis H1.
***  Proved C6:  fld_keylength(dnskey_rec) + 1 <= 
          rr_type__dnskey_record_type__maxdnskeylength
     using hypothesis H47.
***  Proved C7:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
          unsigned_types__unsigned32__first
     using hypothesis H3.
***  Proved C8:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
          unsigned_types__unsigned32__last
     using hypothesis H4.
***  Proved C9:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
     using hypothesis H5.
***  Proved C10:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__classtype__last
     using hypothesis H6.
***  Proved C11:  fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first
     using hypothesis H7.
***  Proved C12:  fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last
     using hypothesis H8.
***  Proved C13:  fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H9.
***  Proved C14:  fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H10.
***  Proved C15:  fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H11.
***  Proved C16:  fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H12.
***  Proved C17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
     using hypothesis H13.
***  Proved C18:  fld_keylength(dnskey_rec) >= 
          rr_type__dnskey_record_type__keylengthvaluetype__first
     using hypothesis H14.
***  Proved C19:  fld_keylength(dnskey_rec) <= 
          rr_type__dnskey_record_type__keylengthvaluetype__last
     using hypothesis H15.
***  Proved C20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
     using hypothesis H16.
***  Proved C21:  length >= rr_type__linelengthindex__first
     using hypothesis H17.
***  Proved C22:  length <= rr_type__linelengthindex__last
     using hypothesis H18.
***  Proved C23:  begidx + 1 >= integer__first
     using hypothesis H52.
***  Proved C24:  begidx + 1 <= integer__last
     using hypothesis H53.
***  Proved C25:  true
***  Proved C26:  true
***  Proved C27:  begidx + 1 >= rr_type__linelengthindex__first
     using hypothesis H21.
***  Proved C28:  begidx + 1 <= rr_type__linelengthindex__last
     using hypothesis H22.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_27.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H18 on reading formula in, to give:
     %%%  H18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__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).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H24).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  true
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  true
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  true
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified C17 on reading formula in, to give:
     %%%  C17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified C20 on reading formula in, to give:
     %%%  C20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
%%%  Simplified C25 on reading formula in, to give:
     %%%  C25:  true
***  Proved C1:  true
***  Proved C2:  true
***  Proved C3:  true
***  Proved C4:  begidx <= endidx + 1
     using hypothesis H55.
***  Proved C5:  begidx >= 1
     using hypothesis H1.
***  Proved C6:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 
          rr_type__dnskey_record_type__maxdnskeylength
     using hypothesis H40.
***  Proved C7:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
          unsigned_types__unsigned32__first
     using hypothesis H5.
***  Proved C8:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
          unsigned_types__unsigned32__last
     using hypothesis H6.
***  Proved C9:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
     using hypothesis H7.
***  Proved C10:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__classtype__last
     using hypothesis H8.
***  Proved C11:  fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first
     using hypothesis H9.
***  Proved C12:  fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last
     using hypothesis H10.
***  Proved C13:  fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H11.
***  Proved C14:  fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H12.
***  Proved C15:  fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H13.
***  Proved C16:  fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H14.
***  Proved C17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
     using hypothesis H15.
***  Proved C18:  fld_keylength(dnskey_rec) >= 
          rr_type__dnskey_record_type__keylengthvaluetype__first
     using hypothesis H16.
***  Proved C19:  fld_keylength(dnskey_rec) <= 
          rr_type__dnskey_record_type__keylengthvaluetype__last
     using hypothesis H17.
***  Proved C20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
     using hypothesis H18.
***  Proved C21:  length >= rr_type__linelengthindex__first
     using hypothesis H19.
***  Proved C22:  length <= rr_type__linelengthindex__last
     using hypothesis H20.
***  Proved C23:  begidx >= integer__first
     using hypothesis H47.
***  Proved C24:  begidx <= integer__last
     using hypothesis H48.
***  Proved C25:  true
***  Proved C26:  begidx <= endidx + 1
     using hypothesis H55.
***  Proved C27:  endidx + 1 >= rr_type__linelengthindex__first
     using hypothesis H23.
***  Proved C28:  endidx + 1 <= rr_type__linelengthindex__last
     using hypothesis H24.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_28.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  true
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H17 on reading formula in, to give:
     %%%  H17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H20 on reading formula in, to give:
     %%%  H20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  Hypothesis H25 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  true
%%%  Simplified C6 on reading formula in, to give:
     %%%  C6:  fld_keylength(dnskey_rec) + (endidx - begidx + 1) <= 
          rr_type__dnskey_record_type__maxdnskeylength
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
          unsigned_types__unsigned32__first
%%%  Simplified C8 on reading formula in, to give:
     %%%  C8:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
          unsigned_types__unsigned32__last
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified C10 on reading formula in, to give:
     %%%  C10:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__classtype__last
%%%  Simplified C11 on reading formula in, to give:
     %%%  C11:  fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first
%%%  Simplified C12 on reading formula in, to give:
     %%%  C12:  fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last
%%%  Simplified C13 on reading formula in, to give:
     %%%  C13:  fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first
%%%  Simplified C14 on reading formula in, to give:
     %%%  C14:  fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last
%%%  Simplified C15 on reading formula in, to give:
     %%%  C15:  fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first
%%%  Simplified C16 on reading formula in, to give:
     %%%  C16:  fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last
%%%  Simplified C17 on reading formula in, to give:
     %%%  C17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(update(fld_key(dnskey_rec), [
          fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1)], element(s, [
          loop__3__i])), [i___1]) and element(update(fld_key(dnskey_rec), [
          fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1)], element(s, [
          loop__3__i])), [i___1]) <= character__last)
%%%  Simplified C18 on reading formula in, to give:
     %%%  C18:  fld_keylength(dnskey_rec) >= 
          rr_type__dnskey_record_type__keylengthvaluetype__first
%%%  Simplified C19 on reading formula in, to give:
     %%%  C19:  fld_keylength(dnskey_rec) <= 
          rr_type__dnskey_record_type__keylengthvaluetype__last
%%%  Simplified C20 on reading formula in, to give:
     %%%  C20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
***  Proved C1:  true
***  Proved C2:  endidx = endidx__entry__loop__3
     using hypothesis H2.
***  Proved C3:  loop__3__i + 1 >= begidx
     using hypothesis H3.
***  Proved C5:  begidx >= 1
     using hypothesis H5.
***  Proved C6:  fld_keylength(dnskey_rec) + (endidx - begidx + 1) <= 
          rr_type__dnskey_record_type__maxdnskeylength
     using hypothesis H6.
***  Proved C7:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 
          unsigned_types__unsigned32__first
     using hypothesis H7.
***  Proved C8:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 
          unsigned_types__unsigned32__last
     using hypothesis H8.
***  Proved C9:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
     using hypothesis H9.
***  Proved C10:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__classtype__last
     using hypothesis H10.
***  Proved C11:  fld_flags(dnskey_rec) >= unsigned_types__unsigned16__first
     using hypothesis H11.
***  Proved C12:  fld_flags(dnskey_rec) <= unsigned_types__unsigned16__last
     using hypothesis H12.
***  Proved C13:  fld_protocol(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H13.
***  Proved C14:  fld_protocol(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H14.
***  Proved C15:  fld_algorithm(dnskey_rec) >= unsigned_types__unsigned8__first
     using hypothesis H15.
***  Proved C16:  fld_algorithm(dnskey_rec) <= unsigned_types__unsigned8__last
     using hypothesis H16.
***  Proved C17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(update(fld_key(dnskey_rec), [
          fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1)], element(s, [
          loop__3__i])), [i___1]) and element(update(fld_key(dnskey_rec), [
          fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1)], element(s, [
          loop__3__i])), [i___1]) <= character__last)
     using hypotheses H17, H29, H30, H33 & H34.
***  Proved C18:  fld_keylength(dnskey_rec) >= 
          rr_type__dnskey_record_type__keylengthvaluetype__first
     using hypothesis H18.
***  Proved C19:  fld_keylength(dnskey_rec) <= 
          rr_type__dnskey_record_type__keylengthvaluetype__last
     using hypothesis H19.
***  Proved C20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
     using hypothesis H20.
***  Proved C21:  length >= rr_type__linelengthindex__first
     using hypothesis H21.
***  Proved C22:  length <= rr_type__linelengthindex__last
     using hypothesis H22.
***  Proved C23:  loop__3__i + 1 >= integer__first
     using hypothesis H23.
***  Proved C25:  loop__3__i + 1 >= begidx
     using hypothesis H3.
***  Proved C27:  endidx__entry__loop__3 >= rr_type__linelengthindex__first
     using hypothesis H27.
***  Proved C28:  endidx__entry__loop__3 <= rr_type__linelengthindex__last
     using hypothesis H28.
-S-  Applied substitution rule addtokey_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H24:  loop__3__i <= 2147483647
<S>  New C24:  loop__3__i <= 2147483646
>>>  Restructured hypothesis H41 into:
     >>>  H41:  loop__3__i <> endidx__entry__loop__3
-S-  Applied substitution rule addtokey_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__maxdnskeylength by:
          1365.
<S>  New H6:  fld_keylength(dnskey_rec) + (endidx - begidx + 1) <= 1365
-S-  Applied substitution rule addtokey_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H23:  loop__3__i >= - 2147483648
-S-  Applied substitution rule addtokey_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H35:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) >= - 
          2147483648
<S>  New H37:  loop__3__i - begidx >= - 2147483649
<S>  New H39:  loop__3__i - begidx >= - 2147483648
-S-  Applied substitution rule addtokey_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H36:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) <= 
          2147483647
<S>  New H38:  loop__3__i - begidx <= 2147483646
<S>  New H40:  loop__3__i - begidx <= 2147483647
-S-  Applied substitution rule addtokey_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= character__last)
<S>  New H20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= character__last)
<S>  New H29:  element(s, [loop__3__i]) >= 0
-S-  Applied substitution rule addtokey_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H30:  element(s, [loop__3__i]) <= 255
<S>  New H17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= 255)
<S>  New H20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(20).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__first by:
          0.
<S>  New H13:  fld_protocol(dnskey_rec) >= 0
<S>  New H15:  fld_algorithm(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(21).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__last by:
          255.
<S>  New H14:  fld_protocol(dnskey_rec) <= 255
<S>  New H16:  fld_algorithm(dnskey_rec) <= 255
-S-  Applied substitution rule addtokey_rules(26).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New H11:  fld_flags(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New H12:  fld_flags(dnskey_rec) <= 65535
-S-  Applied substitution rule addtokey_rules(32).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H7:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 0
-S-  Applied substitution rule addtokey_rules(33).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H8:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 4294967295
-S-  Applied substitution rule addtokey_rules(38).
     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(dnskey_rec))
-S-  Applied substitution rule addtokey_rules(39).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H10:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__hs
-S-  Applied substitution rule addtokey_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H21:  length >= 1
<S>  New H27:  endidx__entry__loop__3 >= 1
<S>  New H31:  loop__3__i >= 1
<S>  New H20:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(s, [i___1]) and 
          element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(66).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H22:  length <= 256
<S>  New H28:  endidx__entry__loop__3 <= 256
<S>  New H32:  loop__3__i <= 256
<S>  New H20:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(s, [i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(72).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__first by:
          0.
<S>  New H18:  fld_keylength(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(73).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__last by:
          1365.
<S>  New H19:  fld_keylength(dnskey_rec) <= 1365
-S-  Applied substitution rule addtokey_rules(77).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first by:
          1.
<S>  New H33:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) >= 1
<S>  New H17:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(78).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last by:
          1365.
<S>  New H34:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) <= 1365
<S>  New H17:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
%%%  Hypotheses H26 & H41 together imply that
          loop__3__i < endidx__entry__loop__3.
     H26 & H41 have therefore been deleted and a new H42 added to this effect.
***  Proved C4:  loop__3__i + 1 <= endidx
     via its standard form, which is:
     Std.Fm C4:  endidx - loop__3__i > 0
     using hypotheses H2 & H42.
***  Proved C26:  loop__3__i + 1 <= endidx__entry__loop__3
     via its standard form, which is:
     Std.Fm C26:  endidx__entry__loop__3 - loop__3__i > 0
     using hypothesis H42.
***  Proved C24:  loop__3__i <= 2147483646
     using hypothesis H32.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_29.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  true
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H17 on reading formula in, to give:
     %%%  H17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H20 on reading formula in, to give:
     %%%  H20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  Hypothesis H25 has been replaced by "true".  (It is already present, as H3)
          .
***  Proved C4:  loop__3__i <= rr_type__linelengthindex__last
     using hypotheses H2, H4 & H28.
-S-  Applied substitution rule addtokey_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= character__last)
<S>  New H20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= character__last)
<S>  New C1:  element(s, [loop__3__i]) >= 0
-S-  Applied substitution rule addtokey_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= 255)
<S>  New H20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= 255)
<S>  New C2:  element(s, [loop__3__i]) <= 255
-S-  Applied substitution rule addtokey_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H21:  length >= 1
<S>  New H27:  endidx__entry__loop__3 >= 1
<S>  New H20:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(s, [i___1]) and 
          element(s, [i___1]) <= 255)
<S>  New C3:  loop__3__i >= 1
-S-  Applied substitution rule addtokey_rules(77).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first by:
          1.
<S>  New H17:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
<S>  New C5:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) >= 1
-S-  Applied substitution rule addtokey_rules(78).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last by:
          1365.
<S>  New H17:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
<S>  New C6:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) <= 1365
-S-  Applied substitution rule addtokey_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C7:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) >= - 
          2147483648
<S>  New C9:  loop__3__i - begidx >= - 2147483649
<S>  New C11:  loop__3__i - begidx >= - 2147483648
-S-  Applied substitution rule addtokey_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C8:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) <= 
          2147483647
<S>  New C10:  loop__3__i - begidx <= 2147483646
<S>  New C12:  loop__3__i - begidx <= 2147483647
***  Proved C1:  element(s, [loop__3__i]) >= 0
     using hypotheses H2, H3, H4, H5, H20 & H28.
***  Proved C2:  element(s, [loop__3__i]) <= 255
     using hypotheses H2, H3, H4, H5, H20 & H28.
***  Proved C3:  loop__3__i >= 1
     using hypotheses H3 & H5.
***  Proved C9:  loop__3__i - begidx >= - 2147483649
     using hypothesis H3.
***  Proved C11:  loop__3__i - begidx >= - 2147483648
     using hypothesis H3.
-S-  Applied substitution rule addtokey_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__maxdnskeylength by:
          1365.
<S>  New H6:  fld_keylength(dnskey_rec) + (endidx - begidx + 1) <= 1365
-S-  Applied substitution rule addtokey_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H23:  loop__3__i >= - 2147483648
-S-  Applied substitution rule addtokey_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H24:  loop__3__i <= 2147483647
-S-  Applied substitution rule addtokey_rules(20).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__first by:
          0.
<S>  New H13:  fld_protocol(dnskey_rec) >= 0
<S>  New H15:  fld_algorithm(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(21).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__last by:
          255.
<S>  New H14:  fld_protocol(dnskey_rec) <= 255
<S>  New H16:  fld_algorithm(dnskey_rec) <= 255
-S-  Applied substitution rule addtokey_rules(26).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New H11:  fld_flags(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New H12:  fld_flags(dnskey_rec) <= 65535
-S-  Applied substitution rule addtokey_rules(32).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H7:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 0
-S-  Applied substitution rule addtokey_rules(33).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H8:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 4294967295
-S-  Applied substitution rule addtokey_rules(38).
     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(dnskey_rec))
-S-  Applied substitution rule addtokey_rules(39).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H10:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__hs
-S-  Applied substitution rule addtokey_rules(66).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H20:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(s, [i___1]) and element(s, [i___1]) <= 255)
<S>  New H22:  length <= 256
<S>  New H28:  endidx__entry__loop__3 <= 256
-S-  Applied substitution rule addtokey_rules(72).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__first by:
          0.
<S>  New H18:  fld_keylength(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(73).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__last by:
          1365.
<S>  New H19:  fld_keylength(dnskey_rec) <= 1365
***  Proved C5:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) >= 1
     using hypotheses H3 & H18.
***  Proved C7:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) >= - 
          2147483648
     using hypotheses H3 & H18.
***  Proved C8:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) <= 
          2147483647
     using hypotheses H2, H4, H5, H19 & H28.
***  Proved C10:  loop__3__i - begidx <= 2147483646
     using hypotheses H5 & H24.
***  Proved C12:  loop__3__i - begidx <= 2147483647
     using hypotheses H5 & H24.
---  Eliminated hypothesis H1 (true-hypothesis).
---  Eliminated hypothesis H25 (true-hypothesis).
---  Eliminated hypothesis H19 (redundant, given H3, H4 & H6).
---  Eliminated hypothesis H23 (redundant, given H3 & H5).
---  Eliminated hypothesis H24 (redundant, given H26 & H28).
-S-  Eliminated hypothesis H2.
     This was achieved by replacing all occurrences of endidx by:
          endidx__entry__loop__3.
<S>  New H4:  loop__3__i <= endidx__entry__loop__3
<S>  New H6:  fld_keylength(dnskey_rec) + (endidx__entry__loop__3 - begidx + 1) 
          <= 1365
***  Proved C6:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) <= 1365
     via its standard form, which is:
     Std.Fm C6:  begidx - loop__3__i - fld_keylength(dnskey_rec) > - 1365
     using hypotheses H4 & H6.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_30.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified H37 on reading formula in, to give:
     %%%  H37:  fld_keylength(dnskey_rec) + 1 >= integer__base__first
%%%  Simplified H38 on reading formula in, to give:
     %%%  H38:  fld_keylength(dnskey_rec) + 1 <= integer__base__last
%%%  Simplified H39 on reading formula in, to give:
     %%%  H39:  1 >= integer__base__first
%%%  Simplified H40 on reading formula in, to give:
     %%%  H40:  1 <= integer__base__last
%%%  Simplified H41 on reading formula in, to give:
     %%%  H41:  0 >= integer__base__first
%%%  Simplified H42 on reading formula in, to give:
     %%%  H42:  0 <= integer__base__last
%%%  Simplified H43 on reading formula in, to give:
     %%%  H43:  not fld_keylength(dnskey_rec) + 1 > 
          rr_type__dnskey_record_type__maxdnskeylength
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H49).
%%%  Simplified H52 on reading formula in, to give:
     %%%  H52:  1 >= integer__first and 1 <= integer__last
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified H58 on reading formula in, to give:
     %%%  H58:  false
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H18).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  fld_keylength(dnskey_rec) + 1 >= 
          rr_type__dnskey_record_type__keylengthvaluetype__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  fld_keylength(dnskey_rec) + 1 <= 
          rr_type__dnskey_record_type__keylengthvaluetype__last
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  1 >= integer__base__first
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  1 <= integer__base__last
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  0 >= integer__base__first
%%%  Simplified C6 on reading formula in, to give:
     %%%  C6:  0 <= integer__base__last
***  Proved C1:  fld_keylength(dnskey_rec) + 1 >= 
          rr_type__dnskey_record_type__keylengthvaluetype__first
     using hypothesis H12.
***  Proved C3:  1 >= integer__base__first
     using hypothesis H39.
***  Proved C4:  1 <= integer__base__last
     using hypothesis H40.
***  Proved C5:  0 >= integer__base__first
     using hypothesis H41.
***  Proved C6:  0 <= integer__base__last
     using hypothesis H42.
-S-  Applied substitution rule addtokey_rules(73).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__last by:
          1365.
<S>  New H13:  fld_keylength(dnskey_rec) <= 1365
<S>  New C2:  fld_keylength(dnskey_rec) <= 1364
>>>  Restructured hypothesis H23 into:
     >>>  H23:  length <= 1 or element(s, [1]) <> blank and element(s, [1]) <> 
          tab
>>>  Restructured hypothesis H32 into:
     >>>  H32:  length <= 1 or (element(s, [1]) = blank or element(s, [1]) = 
          tab)
>>>  Restructured hypothesis H43 into:
     >>>  H43:  fld_keylength(dnskey_rec) + 1 <= 
          rr_type__dnskey_record_type__maxdnskeylength
---  Attempted addition of new hypothesis:
          1 >= integer__first
     eliminated: this already exists (as H48).
---  Attempted addition of new hypothesis:
          1 <= integer__last
     eliminated: this already exists (as H49).
>>>  Hypothesis H52 has now been split into two, giving:
     >>>  H48:  1 >= integer__first
     >>>  H49:  1 <= integer__last
-S-  Applied substitution rule addtokey_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__maxdnskeylength by:
          1365.
<S>  New H43:  fld_keylength(dnskey_rec) <= 1364
-S-  Applied substitution rule addtokey_rules(2).
     This was achieved by replacing all occurrences of blank by:
          32.
<S>  New H23:  length <= 1 or element(s, [1]) <> 32 and element(s, [1]) <> tab
<S>  New H32:  length <= 1 or (element(s, [1]) = 32 or element(s, [1]) = tab)
-S-  Applied substitution rule addtokey_rules(3).
     This was achieved by replacing all occurrences of tab by:
          9.
<S>  New H23:  length <= 1 or element(s, [1]) <> 32 and element(s, [1]) <> 9
<S>  New H32:  length <= 1 or (element(s, [1]) = 32 or element(s, [1]) = 9)
-S-  Applied substitution rule addtokey_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H48:  true
-S-  Applied substitution rule addtokey_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H49:  true
-S-  Applied substitution rule addtokey_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H37:  fld_keylength(dnskey_rec) >= - 2147483649
<S>  New H39:  true
<S>  New H41:  true
-S-  Applied substitution rule addtokey_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H38:  fld_keylength(dnskey_rec) <= 2147483646
<S>  New H40:  true
<S>  New H42:  true
-S-  Applied substitution rule addtokey_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H11:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= character__last)
<S>  New H14:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= character__last)
-S-  Applied substitution rule addtokey_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H11:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= 255)
<S>  New H14:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(20).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__first by:
          0.
<S>  New H7:  fld_protocol(dnskey_rec) >= 0
<S>  New H9:  fld_algorithm(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(21).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__last by:
          255.
<S>  New H8:  fld_protocol(dnskey_rec) <= 255
<S>  New H10:  fld_algorithm(dnskey_rec) <= 255
-S-  Applied substitution rule addtokey_rules(26).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New H5:  fld_flags(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New H6:  fld_flags(dnskey_rec) <= 65535
-S-  Applied substitution rule addtokey_rules(32).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H1:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 0
-S-  Applied substitution rule addtokey_rules(33).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H2:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 4294967295
-S-  Applied substitution rule addtokey_rules(38).
     This was achieved by replacing all occurrences of 
          rr_type__classtype__first by:
          rr_type__internet.
<S>  New H3:  rr_type__internet <= fld_class(fld_inherit(dnskey_rec))
-S-  Applied substitution rule addtokey_rules(39).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H4:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__hs
-S-  Applied substitution rule addtokey_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H15:  length >= 1
<S>  New H17:  true
<S>  New H21:  1 < length -> 1 <= rr_type__linelengthindex__last
<S>  New H14:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(s, [i___1]) and 
          element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(66).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H16:  length <= 256
<S>  New H18:  true
<S>  New H21:  true
<S>  New H14:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(s, [i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(72).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__first by:
          0.
<S>  New H12:  fld_keylength(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(77).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first by:
          1.
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(78).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last by:
          1365.
<S>  New H11:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
***  Proved C2:  fld_keylength(dnskey_rec) <= 1364
     using hypothesis H43.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_31.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H16 on reading formula in, to give:
     %%%  H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  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 H26 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H22).
%%%  Simplified H41 on reading formula in, to give:
     %%%  H41:  fld_keylength(dnskey_rec) + 1 >= integer__base__first
%%%  Simplified H42 on reading formula in, to give:
     %%%  H42:  fld_keylength(dnskey_rec) + 1 <= integer__base__last
%%%  Simplified H43 on reading formula in, to give:
     %%%  H43:  1 >= integer__base__first
%%%  Simplified H44 on reading formula in, to give:
     %%%  H44:  1 <= integer__base__last
%%%  Simplified H45 on reading formula in, to give:
     %%%  H45:  0 >= integer__base__first
%%%  Simplified H46 on reading formula in, to give:
     %%%  H46:  0 <= integer__base__last
%%%  Simplified H47 on reading formula in, to give:
     %%%  H47:  not fld_keylength(dnskey_rec) + 1 > 
          rr_type__dnskey_record_type__maxdnskeylength
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H55 has been replaced by "true".  (It is already present, as 
          H53).
%%%  Simplified H56 on reading formula in, to give:
     %%%  H56:  begidx + 1 >= integer__first and begidx + 1 <= integer__last
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H56).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H22).
%%%  Simplified H62 on reading formula in, to give:
     %%%  H62:  false
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H66 has been replaced by "true".  (It is already present, as 
          H22).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  fld_keylength(dnskey_rec) + 1 >= 
          rr_type__dnskey_record_type__keylengthvaluetype__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  fld_keylength(dnskey_rec) + 1 <= 
          rr_type__dnskey_record_type__keylengthvaluetype__last
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  1 >= integer__base__first
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  1 <= integer__base__last
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  0 >= integer__base__first
%%%  Simplified C6 on reading formula in, to give:
     %%%  C6:  0 <= integer__base__last
***  Proved C1:  fld_keylength(dnskey_rec) + 1 >= 
          rr_type__dnskey_record_type__keylengthvaluetype__first
     using hypothesis H14.
***  Proved C3:  1 >= integer__base__first
     using hypothesis H43.
***  Proved C4:  1 <= integer__base__last
     using hypothesis H44.
***  Proved C5:  0 >= integer__base__first
     using hypothesis H45.
***  Proved C6:  0 <= integer__base__last
     using hypothesis H46.
-S-  Applied substitution rule addtokey_rules(73).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__last by:
          1365.
<S>  New H15:  fld_keylength(dnskey_rec) <= 1365
<S>  New C2:  fld_keylength(dnskey_rec) <= 1364
>>>  Restructured hypothesis H27 into:
     >>>  H27:  length <= begidx + 1 or element(s, [begidx + 1]) <> blank and 
          element(s, [begidx + 1]) <> tab
>>>  Restructured hypothesis H36 into:
     >>>  H36:  length <= begidx + 1 or (element(s, [begidx + 1]) = blank or 
          element(s, [begidx + 1]) = tab)
>>>  Restructured hypothesis H47 into:
     >>>  H47:  fld_keylength(dnskey_rec) + 1 <= 
          rr_type__dnskey_record_type__maxdnskeylength
---  Attempted addition of new hypothesis:
          begidx + 1 >= integer__first
     eliminated: this already exists (as H52).
---  Attempted addition of new hypothesis:
          begidx + 1 <= integer__last
     eliminated: this already exists (as H53).
>>>  Hypothesis H56 has now been split into two, giving:
     >>>  H52:  begidx + 1 >= integer__first
     >>>  H53:  begidx + 1 <= integer__last
-S-  Applied substitution rule addtokey_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__maxdnskeylength by:
          1365.
<S>  New H47:  fld_keylength(dnskey_rec) <= 1364
-S-  Applied substitution rule addtokey_rules(2).
     This was achieved by replacing all occurrences of blank by:
          32.
<S>  New H27:  length <= begidx + 1 or element(s, [begidx + 1]) <> 32 and 
          element(s, [begidx + 1]) <> tab
<S>  New H36:  length <= begidx + 1 or (element(s, [begidx + 1]) = 32 or 
          element(s, [begidx + 1]) = tab)
-S-  Applied substitution rule addtokey_rules(3).
     This was achieved by replacing all occurrences of tab by:
          9.
<S>  New H27:  length <= begidx + 1 or element(s, [begidx + 1]) <> 32 and 
          element(s, [begidx + 1]) <> 9
<S>  New H36:  length <= begidx + 1 or (element(s, [begidx + 1]) = 32 or 
          element(s, [begidx + 1]) = 9)
-S-  Applied substitution rule addtokey_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H52:  begidx >= - 2147483649
-S-  Applied substitution rule addtokey_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H53:  begidx <= 2147483646
-S-  Applied substitution rule addtokey_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H41:  fld_keylength(dnskey_rec) >= - 2147483649
<S>  New H43:  true
<S>  New H45:  true
-S-  Applied substitution rule addtokey_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H42:  fld_keylength(dnskey_rec) <= 2147483646
<S>  New H44:  true
<S>  New H46:  true
-S-  Applied substitution rule addtokey_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= character__last)
<S>  New H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= character__last)
-S-  Applied substitution rule addtokey_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H13:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= 255)
<S>  New H16:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(20).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__first by:
          0.
<S>  New H9:  fld_protocol(dnskey_rec) >= 0
<S>  New H11:  fld_algorithm(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(21).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__last by:
          255.
<S>  New H10:  fld_protocol(dnskey_rec) <= 255
<S>  New H12:  fld_algorithm(dnskey_rec) <= 255
-S-  Applied substitution rule addtokey_rules(26).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New H7:  fld_flags(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New H8:  fld_flags(dnskey_rec) <= 65535
-S-  Applied substitution rule addtokey_rules(32).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H3:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 0
-S-  Applied substitution rule addtokey_rules(33).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H4:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 4294967295
-S-  Applied substitution rule addtokey_rules(38).
     This was achieved by replacing all occurrences of 
          rr_type__classtype__first by:
          rr_type__internet.
<S>  New H5:  rr_type__internet <= fld_class(fld_inherit(dnskey_rec))
-S-  Applied substitution rule addtokey_rules(39).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H6:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__hs
-S-  Applied substitution rule addtokey_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H17:  length >= 1
<S>  New H19:  begidx >= 1
<S>  New H21:  begidx >= 0
<S>  New H25:  begidx + 1 < length -> begidx >= 0 and begidx + 1 <= 
          rr_type__linelengthindex__last
<S>  New H16:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(s, [i___1]) and 
          element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(66).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H18:  length <= 256
<S>  New H20:  begidx <= 256
<S>  New H22:  begidx <= 255
<S>  New H25:  begidx + 1 < length -> begidx >= 0 and begidx <= 255
<S>  New H16:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(s, [i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(72).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__first by:
          0.
<S>  New H14:  fld_keylength(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(77).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first by:
          1.
<S>  New H13:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(78).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last by:
          1365.
<S>  New H13:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
***  Proved C2:  fld_keylength(dnskey_rec) <= 1364
     using hypothesis H47.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_32.  @@@@@@@@@@
%%%  Simplified H7 on reading formula in, to give:
     %%%  H7:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H15 on reading formula in, to give:
     %%%  H15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H18 on reading formula in, to give:
     %%%  H18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__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).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H51 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H24).
***  Proved C3:  endidx + 1 - begidx + 1 >= integer__base__first
     using hypothesis H36.
***  Proved C4:  endidx + 1 - begidx + 1 <= integer__base__last
     using hypothesis H37.
***  Proved C5:  endidx + 1 - begidx >= integer__base__first
     using hypothesis H38.
***  Proved C6:  endidx + 1 - begidx <= integer__base__last
     using hypothesis H39.
-S-  Applied substitution rule addtokey_rules(72).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__first by:
          0.
<S>  New H16:  fld_keylength(dnskey_rec) >= 0
<S>  New C1:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) >= 0
-S-  Applied substitution rule addtokey_rules(73).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__last by:
          1365.
<S>  New H17:  fld_keylength(dnskey_rec) <= 1365
<S>  New C2:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 1365
***  Proved C1:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) >= 0
     using hypotheses H2 & H16.
>>>  Restructured hypothesis H29 into:
     >>>  H29:  length <= endidx + 1 or (element(s, [endidx + 1]) = blank or 
          element(s, [endidx + 1]) = tab)
>>>  Restructured hypothesis H40 into:
     >>>  H40:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 
          rr_type__dnskey_record_type__maxdnskeylength
>>>  Restructured hypothesis H55 into:
     >>>  H55:  endidx + 1 < begidx
-S-  Applied substitution rule addtokey_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__maxdnskeylength by:
          1365.
<S>  New H40:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 1365
-S-  Applied substitution rule addtokey_rules(2).
     This was achieved by replacing all occurrences of blank by:
          32.
<S>  New H29:  length <= endidx + 1 or (element(s, [endidx + 1]) = 32 or 
          element(s, [endidx + 1]) = tab)
-S-  Applied substitution rule addtokey_rules(3).
     This was achieved by replacing all occurrences of tab by:
          9.
<S>  New H29:  length <= endidx + 1 or (element(s, [endidx + 1]) = 32 or 
          element(s, [endidx + 1]) = 9)
-S-  Applied substitution rule addtokey_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H45:  endidx >= - 2147483649
<S>  New H47:  begidx >= - 2147483648
<S>  New H49:  begidx <= endidx + 1 -> endidx >= - 2147483649 and endidx + 1 <= 
          integer__last
<S>  New H50:  begidx <= endidx + 1 -> begidx >= - 2147483648 and begidx <= 
          integer__last
-S-  Applied substitution rule addtokey_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H46:  endidx <= 2147483646
<S>  New H48:  begidx <= 2147483647
<S>  New H49:  begidx <= endidx + 1 -> endidx >= - 2147483649 and endidx <= 
          2147483646
<S>  New H50:  begidx <= endidx + 1 -> begidx >= - 2147483648 and begidx <= 
          2147483647
-S-  Applied substitution rule addtokey_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H34:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) >= - 
          2147483648
<S>  New H36:  endidx + 1 - begidx >= - 2147483649
<S>  New H38:  endidx + 1 - begidx >= - 2147483648
-S-  Applied substitution rule addtokey_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H35:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 
          2147483647
<S>  New H37:  endidx + 1 - begidx <= 2147483646
<S>  New H39:  endidx + 1 - begidx <= 2147483647
-S-  Applied substitution rule addtokey_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= character__last)
<S>  New H18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= character__last)
-S-  Applied substitution rule addtokey_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H15:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= 255)
<S>  New H18:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(20).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__first by:
          0.
<S>  New H11:  fld_protocol(dnskey_rec) >= 0
<S>  New H13:  fld_algorithm(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(21).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__last by:
          255.
<S>  New H12:  fld_protocol(dnskey_rec) <= 255
<S>  New H14:  fld_algorithm(dnskey_rec) <= 255
-S-  Applied substitution rule addtokey_rules(26).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New H9:  fld_flags(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New H10:  fld_flags(dnskey_rec) <= 65535
-S-  Applied substitution rule addtokey_rules(32).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H5:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 0
-S-  Applied substitution rule addtokey_rules(33).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H6:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 4294967295
-S-  Applied substitution rule addtokey_rules(38).
     This was achieved by replacing all occurrences of 
          rr_type__classtype__first by:
          rr_type__internet.
<S>  New H7:  rr_type__internet <= fld_class(fld_inherit(dnskey_rec))
-S-  Applied substitution rule addtokey_rules(39).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H8:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__hs
-S-  Applied substitution rule addtokey_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H19:  length >= 1
<S>  New H21:  endidx >= 1
<S>  New H23:  endidx >= 0
<S>  New H27:  endidx + 1 < length -> endidx >= 0 and endidx + 1 <= 
          rr_type__linelengthindex__last
<S>  New H30:  begidx >= 1
<S>  New H18:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(s, [i___1]) and 
          element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(66).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H20:  length <= 256
<S>  New H22:  endidx <= 256
<S>  New H24:  endidx <= 255
<S>  New H31:  begidx <= 256
<S>  New H27:  endidx + 1 < length -> endidx >= 0 and endidx <= 255
<S>  New H18:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(s, [i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(77).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first by:
          1.
<S>  New H15:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(78).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last by:
          1365.
<S>  New H15:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
***  Proved C2:  fld_keylength(dnskey_rec) + (endidx + 1 - begidx + 1) <= 1365
     using hypothesis H40.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_addtokey_33.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  true
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  rr_type__classtype__first <= fld_class(fld_inherit(dnskey_rec))
%%%  Simplified H17 on reading formula in, to give:
     %%%  H17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> character__first <= element(fld_key(dnskey_rec), [i___1]) and 
          element(fld_key(dnskey_rec), [i___1]) <= character__last)
%%%  Simplified H20 on reading formula in, to give:
     %%%  H20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  Hypothesis H25 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  fld_keylength(dnskey_rec) + (endidx - begidx + 1) >= 
          rr_type__dnskey_record_type__keylengthvaluetype__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  fld_keylength(dnskey_rec) + (endidx - begidx + 1) <= 
          rr_type__dnskey_record_type__keylengthvaluetype__last
-S-  Applied substitution rule addtokey_rules(72).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__first by:
          0.
<S>  New H18:  fld_keylength(dnskey_rec) >= 0
<S>  New C1:  fld_keylength(dnskey_rec) + (endidx - begidx + 1) >= 0
-S-  Applied substitution rule addtokey_rules(73).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__keylengthvaluetype__last by:
          1365.
<S>  New H19:  fld_keylength(dnskey_rec) <= 1365
<S>  New C2:  fld_keylength(dnskey_rec) + (endidx - begidx + 1) <= 1365
-S-  Applied substitution rule addtokey_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H35:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) >= - 
          2147483648
<S>  New H37:  loop__3__i - begidx >= - 2147483649
<S>  New H39:  loop__3__i - begidx >= - 2147483648
<S>  New C3:  endidx - begidx >= - 2147483649
<S>  New C5:  endidx - begidx >= - 2147483648
-S-  Applied substitution rule addtokey_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H36:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) <= 
          2147483647
<S>  New H38:  loop__3__i - begidx <= 2147483646
<S>  New H40:  loop__3__i - begidx <= 2147483647
<S>  New C4:  endidx - begidx <= 2147483646
<S>  New C6:  endidx - begidx <= 2147483647
***  Proved C1:  fld_keylength(dnskey_rec) + (endidx - begidx + 1) >= 0
     using hypotheses H3, H4 & H18.
***  Proved C3:  endidx - begidx >= - 2147483649
     using hypotheses H3 & H4.
***  Proved C5:  endidx - begidx >= - 2147483648
     using hypotheses H3 & H4.
-S-  Applied substitution rule addtokey_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__maxdnskeylength by:
          1365.
<S>  New H6:  fld_keylength(dnskey_rec) + (endidx - begidx + 1) <= 1365
-S-  Applied substitution rule addtokey_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H23:  loop__3__i >= - 2147483648
-S-  Applied substitution rule addtokey_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H24:  loop__3__i <= 2147483647
-S-  Applied substitution rule addtokey_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= character__last)
<S>  New H20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= character__last)
<S>  New H29:  element(s, [loop__3__i]) >= 0
-S-  Applied substitution rule addtokey_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H30:  element(s, [loop__3__i]) <= 255
<S>  New H17:  for_all(i___1 : integer, 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first <= i___1 
          and i___1 <= rr_type__dnskey_record_type__dnskeystringtypeindex__last 
          -> 0 <= element(fld_key(dnskey_rec), [i___1]) and element(fld_key(
          dnskey_rec), [i___1]) <= 255)
<S>  New H20:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [
          i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(20).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__first by:
          0.
<S>  New H13:  fld_protocol(dnskey_rec) >= 0
<S>  New H15:  fld_algorithm(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(21).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned8__last by:
          255.
<S>  New H14:  fld_protocol(dnskey_rec) <= 255
<S>  New H16:  fld_algorithm(dnskey_rec) <= 255
-S-  Applied substitution rule addtokey_rules(26).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__first by:
          0.
<S>  New H11:  fld_flags(dnskey_rec) >= 0
-S-  Applied substitution rule addtokey_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned16__last by:
          65535.
<S>  New H12:  fld_flags(dnskey_rec) <= 65535
-S-  Applied substitution rule addtokey_rules(32).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H7:  fld_ttlinseconds(fld_inherit(dnskey_rec)) >= 0
-S-  Applied substitution rule addtokey_rules(33).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H8:  fld_ttlinseconds(fld_inherit(dnskey_rec)) <= 4294967295
-S-  Applied substitution rule addtokey_rules(38).
     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(dnskey_rec))
-S-  Applied substitution rule addtokey_rules(39).
     This was achieved by replacing all occurrences of rr_type__classtype__last 
          by:
          rr_type__hs.
<S>  New H10:  fld_class(fld_inherit(dnskey_rec)) <= rr_type__hs
-S-  Applied substitution rule addtokey_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H21:  length >= 1
<S>  New H27:  endidx__entry__loop__3 >= 1
<S>  New H31:  loop__3__i >= 1
<S>  New H42:  begidx >= 1
<S>  New H44:  endidx >= 1
<S>  New H20:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(s, [i___1]) and 
          element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(66).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H22:  length <= 256
<S>  New H28:  endidx__entry__loop__3 <= 256
<S>  New H32:  loop__3__i <= 256
<S>  New H43:  begidx <= 256
<S>  New H45:  endidx <= 256
<S>  New H20:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(s, [i___1]) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(77).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__first by:
          1.
<S>  New H33:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) >= 1
<S>  New H17:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
-S-  Applied substitution rule addtokey_rules(78).
     This was achieved by replacing all occurrences of 
          rr_type__dnskey_record_type__dnskeystringtypeindex__last by:
          1365.
<S>  New H34:  fld_keylength(dnskey_rec) + (loop__3__i - begidx + 1) <= 1365
<S>  New H17:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 1365 -> 0 <= 
          element(fld_key(dnskey_rec), [i___1]) and element(fld_key(dnskey_rec)
          , [i___1]) <= 255)
***  Proved C2:  fld_keylength(dnskey_rec) + (endidx - begidx + 1) <= 1365
     using hypothesis H6.
***  Proved C4:  endidx - begidx <= 2147483646
     using hypotheses H5 & H45.
***  Proved C6:  endidx - begidx <= 2147483647
     using hypotheses H5 & H45.
***  PROVED VC.


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


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


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


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


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


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


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

