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

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



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

procedure Zone_File_Parser.parseDomainName






@@@@@@@@@@  VC: procedure_parsedomainname_1.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
***  Proved C1:  1 >= rr_type__linelengthindex__first
     using hypothesis H4.
***  Proved C2:  1 <= rr_type__linelengthindex__last
     using hypothesis H5.
***  Proved C3:  zlength >= rr_type__linelengthindex__first
     using hypothesis H2.
***  Proved C4:  zlength <= rr_type__linelengthindex__last
     using hypothesis H3.
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H2:  zlength >= 1
<S>  New H4:  true
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H3:  zlength <= 256
<S>  New H5:  true
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C5:  1 <= zlength
     using hypothesis H2.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_2.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H4).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H3).
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  rr_type__rritemtype__first <= foundtype__1
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  rr_type__rritemtype__first <= foundtype__1
***  Proved C1:  rr_type__rritemtype__first <= foundtype__1
     using hypothesis H19.
***  Proved C2:  foundtype__1 <= rr_type__rritemtype__last
     using hypothesis H20.
***  Proved C3:  endidx__1 >= rr_type__linelengthindex__first
     using hypothesis H17.
***  Proved C4:  endidx__1 <= rr_type__linelengthindex__last
     using hypothesis H18.
***  Proved C5:  begidx__1 >= rr_type__linelengthindex__first
     using hypothesis H15.
***  Proved C6:  begidx__1 <= rr_type__linelengthindex__last
     using hypothesis H16.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_3.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H4).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H3).
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  rr_type__rritemtype__first <= foundtype__1
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H20).
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
***  Proved C1:  endidx__1 < zlength
     using hypothesis H32.
***  Proved C2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
     using hypothesis H1.
***  Proved C3:  zlength >= rr_type__linelengthindex__first
     using hypothesis H2.
***  Proved C4:  zlength <= rr_type__linelengthindex__last
     using hypothesis H3.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_4.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  endidx >= integer__base__first
%%%  Simplified H12 on reading formula in, to give:
     %%%  H12:  endidx <= integer__base__last
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  0 >= integer__base__first
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  0 <= integer__base__last
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H20 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  endidx + 1 <= zlength
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  foundtype__2 = rr_type__number -> for_all(i_ : integer, 
          begidx__2 <= i_ and i_ <= endidx__2 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  rr_type__rritemtype__first <= foundtype__2
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H31).
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
***  Proved C1:  endidx__2 < zlength
     using hypothesis H43.
***  Proved C2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
     using hypothesis H2.
***  Proved C3:  zlength >= rr_type__linelengthindex__first
     using hypothesis H3.
***  Proved C4:  zlength <= rr_type__linelengthindex__last
     using hypothesis H4.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_5.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  endidx >= integer__base__first
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  endidx <= 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:  endidx + 1 >= rr_type__linelengthindex__first
     using hypothesis H7.
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= 256 -> character__first <= element(zonefileline, [i___1])
           and element(zonefileline, [i___1]) <= character__last)
<S>  New H4:  zlength <= 256
<S>  New H6:  begidx <= 256
<S>  New H8:  endidx <= 256
<S>  New C2:  endidx <= 255
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C3:  endidx >= - 2147483648
<S>  New C5:  true
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C4:  endidx <= 2147483647
<S>  New C6:  true
***  Proved C2:  endidx <= 255
     using hypotheses H1 & H4.
***  Proved C5:  true
***  Proved C4:  endidx <= 2147483647
     using hypothesis H8.
***  Proved C6:  true
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= 256 -> 0 <= element(zonefileline, [i___1]) and element(
          zonefileline, [i___1]) <= character__last)
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= 256 -> 0 <= element(zonefileline, [i___1]) and element(
          zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H3:  zlength >= 1
<S>  New H5:  begidx >= 1
<S>  New H7:  endidx >= 1
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C3:  endidx >= - 2147483648
     using hypothesis H7.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_6.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  endidx >= integer__base__first
%%%  Simplified H12 on reading formula in, to give:
     %%%  H12:  endidx <= integer__base__last
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  0 >= integer__base__first
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  0 <= integer__base__last
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  endidx + 1 <= zlength
***  Proved C1:  endidx + 1 >= rr_type__linelengthindex__first
     using hypothesis H9.
***  Proved C2:  endidx + 1 <= rr_type__linelengthindex__last
     using hypothesis H10.
***  Proved C3:  zlength >= rr_type__linelengthindex__first
     using hypothesis H3.
***  Proved C4:  zlength <= rr_type__linelengthindex__last
     using hypothesis H4.
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H11:  endidx >= - 2147483648
<S>  New H13:  true
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H12:  endidx <= 2147483647
<S>  New H14:  true
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H3:  zlength >= 1
<S>  New H5:  begidx >= 1
<S>  New H7:  endidx >= 1
<S>  New H9:  endidx >= 0
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H4:  zlength <= 256
<S>  New H6:  begidx <= 256
<S>  New H8:  endidx <= 256
<S>  New H10:  endidx <= 255
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C5:  endidx + 1 <= zlength
     via its standard form, which is:
     Std.Fm C5:  - endidx + zlength > 0
     using hypothesis H1.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_7.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  endidx >= integer__base__first
%%%  Simplified H12 on reading formula in, to give:
     %%%  H12:  endidx <= integer__base__last
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  0 >= integer__base__first
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  0 <= integer__base__last
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H20 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  endidx + 1 <= zlength
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  foundtype__2 = rr_type__number -> for_all(i_ : integer, 
          begidx__2 <= i_ and i_ <= endidx__2 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  rr_type__rritemtype__first <= foundtype__2
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  rr_type__rritemtype__first <= foundtype__2
***  Proved C1:  rr_type__rritemtype__first <= foundtype__2
     using hypothesis H30.
***  Proved C2:  foundtype__2 <= rr_type__rritemtype__last
     using hypothesis H31.
***  Proved C3:  endidx__2 >= rr_type__linelengthindex__first
     using hypothesis H28.
***  Proved C4:  endidx__2 <= rr_type__linelengthindex__last
     using hypothesis H29.
***  Proved C5:  begidx__2 >= rr_type__linelengthindex__first
     using hypothesis H26.
***  Proved C6:  begidx__2 <= rr_type__linelengthindex__last
     using hypothesis H27.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_8.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H4).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H3).
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  rr_type__rritemtype__first <= foundtype__1
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H33 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).
***  Proved C1:  endidx__1 + 1 >= rr_type__linelengthindex__first
     using hypothesis H17.
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= 256 -> character__first <= element(zonefileline, [i___1])
           and element(zonefileline, [i___1]) <= character__last)
<S>  New H3:  zlength <= 256
<S>  New H5:  true
<S>  New H16:  begidx__1 <= 256
<S>  New H18:  endidx__1 <= 256
<S>  New C2:  endidx__1 <= 255
***  Proved C2:  endidx__1 <= 255
     using hypotheses H3 & H34.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_9.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  endidx >= integer__base__first
%%%  Simplified H12 on reading formula in, to give:
     %%%  H12:  endidx <= integer__base__last
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  0 >= integer__base__first
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  0 <= integer__base__last
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H20 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  endidx + 1 <= zlength
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  foundtype__2 = rr_type__number -> for_all(i_ : integer, 
          begidx__2 <= i_ and i_ <= endidx__2 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  rr_type__rritemtype__first <= foundtype__2
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H29).
***  Proved C1:  endidx__2 + 1 >= rr_type__linelengthindex__first
     using hypothesis H28.
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= 256 -> character__first <= element(zonefileline, [i___1])
           and element(zonefileline, [i___1]) <= character__last)
<S>  New H4:  zlength <= 256
<S>  New H6:  begidx <= 256
<S>  New H8:  endidx <= 256
<S>  New H10:  endidx <= 255
<S>  New H27:  begidx__2 <= 256
<S>  New H29:  endidx__2 <= 256
<S>  New C2:  endidx__2 <= 255
***  Proved C2:  endidx__2 <= 255
     using hypotheses H4 & H45.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_10.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H4).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H3).
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  rr_type__rritemtype__first <= foundtype__1
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H33 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).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H38).
***  Proved C1:  endidx__1 + 1 >= rr_type__linelengthindex__first
     using hypothesis H37.
***  Proved C2:  endidx__1 + 1 <= rr_type__linelengthindex__last
     using hypothesis H38.
***  Proved C3:  zlength >= rr_type__linelengthindex__first
     using hypothesis H2.
***  Proved C4:  zlength <= rr_type__linelengthindex__last
     using hypothesis H3.
>>>  Restructured hypothesis H31 into:
     >>>  H31:  foundtype__1 = rr_type__recordindicator or zlength <= endidx__1
>>>  Restructured hypothesis H34 into:
     >>>  H34:  endidx__1 < zlength
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(23).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__first by:
          rr_type__domainnameortimespec.
<S>  New H19:  rr_type__domainnameortimespec <= foundtype__1
-S-  Applied substitution rule parsedomainn_rules(24).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__last by:
          rr_type__other.
<S>  New H20:  foundtype__1 <= rr_type__other
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H2:  zlength >= 1
<S>  New H4:  true
<S>  New H15:  begidx__1 >= 1
<S>  New H17:  endidx__1 >= 1
<S>  New H37:  endidx__1 >= 0
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H3:  zlength <= 256
<S>  New H5:  true
<S>  New H16:  begidx__1 <= 256
<S>  New H18:  endidx__1 <= 256
<S>  New H38:  endidx__1 <= 255
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C5:  endidx__1 + 1 <= zlength
     via its standard form, which is:
     Std.Fm C5:  - endidx__1 + zlength > 0
     using hypothesis H34.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_11.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  endidx >= integer__base__first
%%%  Simplified H12 on reading formula in, to give:
     %%%  H12:  endidx <= integer__base__last
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  0 >= integer__base__first
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  0 <= integer__base__last
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H20 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  endidx + 1 <= zlength
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  foundtype__2 = rr_type__number -> for_all(i_ : integer, 
          begidx__2 <= i_ and i_ <= endidx__2 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  rr_type__rritemtype__first <= foundtype__2
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H29).
---  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).
***  Proved C1:  endidx__2 + 1 >= rr_type__linelengthindex__first
     using hypothesis H48.
***  Proved C2:  endidx__2 + 1 <= rr_type__linelengthindex__last
     using hypothesis H49.
***  Proved C3:  zlength >= rr_type__linelengthindex__first
     using hypothesis H3.
***  Proved C4:  zlength <= rr_type__linelengthindex__last
     using hypothesis H4.
>>>  Restructured hypothesis H42 into:
     >>>  H42:  foundtype__2 = rr_type__recordindicator or zlength <= endidx__2
>>>  Restructured hypothesis H45 into:
     >>>  H45:  endidx__2 < zlength
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H11:  endidx >= - 2147483648
<S>  New H13:  true
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H12:  endidx <= 2147483647
<S>  New H14:  true
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(23).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__first by:
          rr_type__domainnameortimespec.
<S>  New H30:  rr_type__domainnameortimespec <= foundtype__2
-S-  Applied substitution rule parsedomainn_rules(24).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__last by:
          rr_type__other.
<S>  New H31:  foundtype__2 <= rr_type__other
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H3:  zlength >= 1
<S>  New H5:  begidx >= 1
<S>  New H7:  endidx >= 1
<S>  New H9:  endidx >= 0
<S>  New H26:  begidx__2 >= 1
<S>  New H28:  endidx__2 >= 1
<S>  New H48:  endidx__2 >= 0
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H4:  zlength <= 256
<S>  New H6:  begidx <= 256
<S>  New H8:  endidx <= 256
<S>  New H10:  endidx <= 255
<S>  New H27:  begidx__2 <= 256
<S>  New H29:  endidx__2 <= 256
<S>  New H49:  endidx__2 <= 255
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C5:  endidx__2 + 1 <= zlength
     via its standard form, which is:
     Std.Fm C5:  - endidx__2 + zlength > 0
     using hypothesis H45.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_12.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H4).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H3).
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  rr_type__rritemtype__first <= foundtype__1
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H33 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).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H44 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified H49 on reading formula in, to give:
     %%%  H49:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H54 on reading formula in, to give:
     %%%  H54:  rr_type__rritemtype__first <= foundtype__3
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  rr_type__rritemtype__first <= foundtype__3
***  Proved C1:  rr_type__rritemtype__first <= foundtype__3
     using hypothesis H54.
***  Proved C2:  foundtype__3 <= rr_type__rritemtype__last
     using hypothesis H55.
***  Proved C3:  endidx__3 >= rr_type__linelengthindex__first
     using hypothesis H52.
***  Proved C4:  endidx__3 <= rr_type__linelengthindex__last
     using hypothesis H53.
***  Proved C5:  begidx__3 >= rr_type__linelengthindex__first
     using hypothesis H50.
***  Proved C6:  begidx__3 <= rr_type__linelengthindex__last
     using hypothesis H51.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_13.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  endidx >= integer__base__first
%%%  Simplified H12 on reading formula in, to give:
     %%%  H12:  endidx <= integer__base__last
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  0 >= integer__base__first
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  0 <= integer__base__last
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H20 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  endidx + 1 <= zlength
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  foundtype__2 = rr_type__number -> for_all(i_ : integer, 
          begidx__2 <= i_ and i_ <= endidx__2 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  rr_type__rritemtype__first <= foundtype__2
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H29).
---  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).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H55 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H60 on reading formula in, to give:
     %%%  H60:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H65 on reading formula in, to give:
     %%%  H65:  rr_type__rritemtype__first <= foundtype__3
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  rr_type__rritemtype__first <= foundtype__3
***  Proved C1:  rr_type__rritemtype__first <= foundtype__3
     using hypothesis H65.
***  Proved C2:  foundtype__3 <= rr_type__rritemtype__last
     using hypothesis H66.
***  Proved C3:  endidx__3 >= rr_type__linelengthindex__first
     using hypothesis H63.
***  Proved C4:  endidx__3 <= rr_type__linelengthindex__last
     using hypothesis H64.
***  Proved C5:  begidx__3 >= rr_type__linelengthindex__first
     using hypothesis H61.
***  Proved C6:  begidx__3 <= rr_type__linelengthindex__last
     using hypothesis H62.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_14.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H4).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H3).
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  rr_type__rritemtype__first <= foundtype__1
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H33 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).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H44 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified H49 on reading formula in, to give:
     %%%  H49:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H54 on reading formula in, to give:
     %%%  H54:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H54).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H55).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H53).
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> character__first <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
<S>  New H2:  zlength >= 1
<S>  New H4:  true
<S>  New H15:  begidx__1 >= 1
<S>  New H17:  endidx__1 >= 1
<S>  New H37:  endidx__1 >= 0
<S>  New H50:  begidx__3 >= 1
<S>  New H52:  endidx__3 >= 1
<S>  New C1:  endidx__3 - begidx__3 >= 0
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H3:  zlength <= 256
<S>  New H5:  true
<S>  New H16:  begidx__1 <= 256
<S>  New H18:  endidx__1 <= 256
<S>  New H38:  endidx__1 <= 255
<S>  New H51:  begidx__3 <= 256
<S>  New H53:  endidx__3 <= 256
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 
          character__first <= element(zonefileline, [i___1]) and element(
          zonefileline, [i___1]) <= character__last)
<S>  New C2:  endidx__3 - begidx__3 <= 255
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C3:  endidx__3 - begidx__3 >= - 2147483648
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C4:  endidx__3 - begidx__3 <= 2147483647
***  Proved C1:  endidx__3 - begidx__3 >= 0
     using hypothesis H46.
***  Proved C2:  endidx__3 - begidx__3 <= 255
     using hypotheses H50 & H53.
***  Proved C3:  endidx__3 - begidx__3 >= - 2147483648
     using hypothesis H46.
***  Proved C4:  endidx__3 - begidx__3 <= 2147483647
     using hypotheses H50 & H53.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_15.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  endidx >= integer__base__first
%%%  Simplified H12 on reading formula in, to give:
     %%%  H12:  endidx <= integer__base__last
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  0 >= integer__base__first
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  0 <= integer__base__last
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H20 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  endidx + 1 <= zlength
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  foundtype__2 = rr_type__number -> for_all(i_ : integer, 
          begidx__2 <= i_ and i_ <= endidx__2 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  rr_type__rritemtype__first <= foundtype__2
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H29).
---  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).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H55 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H60 on reading formula in, to give:
     %%%  H60:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H65 on reading formula in, to give:
     %%%  H65:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H64).
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> character__first <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
<S>  New H3:  zlength >= 1
<S>  New H5:  begidx >= 1
<S>  New H7:  endidx >= 1
<S>  New H9:  endidx >= 0
<S>  New H26:  begidx__2 >= 1
<S>  New H28:  endidx__2 >= 1
<S>  New H48:  endidx__2 >= 0
<S>  New H61:  begidx__3 >= 1
<S>  New H63:  endidx__3 >= 1
<S>  New C1:  endidx__3 - begidx__3 >= 0
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H4:  zlength <= 256
<S>  New H6:  begidx <= 256
<S>  New H8:  endidx <= 256
<S>  New H10:  endidx <= 255
<S>  New H27:  begidx__2 <= 256
<S>  New H29:  endidx__2 <= 256
<S>  New H49:  endidx__2 <= 255
<S>  New H62:  begidx__3 <= 256
<S>  New H64:  endidx__3 <= 256
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 
          character__first <= element(zonefileline, [i___1]) and element(
          zonefileline, [i___1]) <= character__last)
<S>  New C2:  endidx__3 - begidx__3 <= 255
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H11:  endidx >= - 2147483648
<S>  New H13:  true
<S>  New C3:  endidx__3 - begidx__3 >= - 2147483648
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H12:  endidx <= 2147483647
<S>  New H14:  true
<S>  New C4:  endidx__3 - begidx__3 <= 2147483647
***  Proved C1:  endidx__3 - begidx__3 >= 0
     using hypothesis H57.
***  Proved C2:  endidx__3 - begidx__3 <= 255
     using hypotheses H61 & H64.
***  Proved C3:  endidx__3 - begidx__3 >= - 2147483648
     using hypothesis H57.
***  Proved C4:  endidx__3 - begidx__3 <= 2147483647
     using hypotheses H61 & H64.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_16.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H4).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H3).
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  rr_type__rritemtype__first <= foundtype__1
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H33 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).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H44 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified H49 on reading formula in, to give:
     %%%  H49:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H54 on reading formula in, to give:
     %%%  H54:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H54).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H55).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H54).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H55).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H67).
%%%  Simplified H75 on reading formula in, to give:
     %%%  H75:  true
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H79 has been replaced by "true".  (It is already present, as 
          H53).
-S-  Applied substitution rule parsedomainn_rules(13).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New C1:  endidx__3 >= 0
<S>  New C3:  begidx__3 >= 0
-S-  Applied substitution rule parsedomainn_rules(14).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New C2:  endidx__3 <= 2147483647
<S>  New C4:  begidx__3 <= 2147483647
>>>  Restructured hypothesis H31 into:
     >>>  H31:  foundtype__1 = rr_type__recordindicator or zlength <= endidx__1
>>>  Restructured hypothesis H34 into:
     >>>  H34:  endidx__1 < zlength
-S-  Applied substitution rule parsedomainn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H74:  endidx__3 - begidx__3 > 127
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H68:  endidx__3 - begidx__3 >= - 2147483648
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H69:  endidx__3 - begidx__3 <= 2147483647
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(23).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__first by:
          rr_type__domainnameortimespec.
<S>  New H19:  rr_type__domainnameortimespec <= foundtype__1
<S>  New H54:  rr_type__domainnameortimespec <= foundtype__3
-S-  Applied substitution rule parsedomainn_rules(24).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__last by:
          rr_type__other.
<S>  New H20:  foundtype__1 <= rr_type__other
<S>  New H55:  foundtype__3 <= rr_type__other
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H2:  zlength >= 1
<S>  New H4:  true
<S>  New H15:  begidx__1 >= 1
<S>  New H17:  endidx__1 >= 1
<S>  New H37:  endidx__1 >= 0
<S>  New H50:  begidx__3 >= 1
<S>  New H52:  endidx__3 >= 1
<S>  New H66:  endidx__3 - begidx__3 >= 0
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H3:  zlength <= 256
<S>  New H5:  true
<S>  New H16:  begidx__1 <= 256
<S>  New H18:  endidx__1 <= 256
<S>  New H38:  endidx__1 <= 255
<S>  New H51:  begidx__3 <= 256
<S>  New H53:  endidx__3 <= 256
<S>  New H67:  endidx__3 - begidx__3 <= 255
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C1:  endidx__3 >= 0
     using hypothesis H52.
***  Proved C3:  begidx__3 >= 0
     using hypothesis H50.
***  Proved C2:  endidx__3 <= 2147483647
     using hypothesis H53.
***  Proved C4:  begidx__3 <= 2147483647
     using hypothesis H51.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_17.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  endidx >= integer__base__first
%%%  Simplified H12 on reading formula in, to give:
     %%%  H12:  endidx <= integer__base__last
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  0 >= integer__base__first
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  0 <= integer__base__last
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H20 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  endidx + 1 <= zlength
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  foundtype__2 = rr_type__number -> for_all(i_ : integer, 
          begidx__2 <= i_ and i_ <= endidx__2 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  rr_type__rritemtype__first <= foundtype__2
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H29).
---  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).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H55 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H60 on reading formula in, to give:
     %%%  H60:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H65 on reading formula in, to give:
     %%%  H65:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H81 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H82 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H83 has been replaced by "true".  (It is already present, as 
          H77).
---  Hypothesis H84 has been replaced by "true".  (It is already present, as 
          H78).
%%%  Simplified H86 on reading formula in, to give:
     %%%  H86:  true
---  Hypothesis H87 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H88 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H89 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H90 has been replaced by "true".  (It is already present, as 
          H64).
-S-  Applied substitution rule parsedomainn_rules(13).
     This was achieved by replacing all occurrences of natural__first by:
          0.
<S>  New C1:  endidx__3 >= 0
<S>  New C3:  begidx__3 >= 0
-S-  Applied substitution rule parsedomainn_rules(14).
     This was achieved by replacing all occurrences of natural__last by:
          2147483647.
<S>  New C2:  endidx__3 <= 2147483647
<S>  New C4:  begidx__3 <= 2147483647
>>>  Restructured hypothesis H42 into:
     >>>  H42:  foundtype__2 = rr_type__recordindicator or zlength <= endidx__2
>>>  Restructured hypothesis H45 into:
     >>>  H45:  endidx__2 < zlength
-S-  Applied substitution rule parsedomainn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H85:  endidx__3 - begidx__3 > 127
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H11:  endidx >= - 2147483648
<S>  New H13:  true
<S>  New H79:  endidx__3 - begidx__3 >= - 2147483648
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H12:  endidx <= 2147483647
<S>  New H14:  true
<S>  New H80:  endidx__3 - begidx__3 <= 2147483647
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(23).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__first by:
          rr_type__domainnameortimespec.
<S>  New H30:  rr_type__domainnameortimespec <= foundtype__2
<S>  New H65:  rr_type__domainnameortimespec <= foundtype__3
-S-  Applied substitution rule parsedomainn_rules(24).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__last by:
          rr_type__other.
<S>  New H31:  foundtype__2 <= rr_type__other
<S>  New H66:  foundtype__3 <= rr_type__other
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H3:  zlength >= 1
<S>  New H5:  begidx >= 1
<S>  New H7:  endidx >= 1
<S>  New H9:  endidx >= 0
<S>  New H26:  begidx__2 >= 1
<S>  New H28:  endidx__2 >= 1
<S>  New H48:  endidx__2 >= 0
<S>  New H61:  begidx__3 >= 1
<S>  New H63:  endidx__3 >= 1
<S>  New H77:  endidx__3 - begidx__3 >= 0
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H4:  zlength <= 256
<S>  New H6:  begidx <= 256
<S>  New H8:  endidx <= 256
<S>  New H10:  endidx <= 255
<S>  New H27:  begidx__2 <= 256
<S>  New H29:  endidx__2 <= 256
<S>  New H49:  endidx__2 <= 255
<S>  New H62:  begidx__3 <= 256
<S>  New H64:  endidx__3 <= 256
<S>  New H78:  endidx__3 - begidx__3 <= 255
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C1:  endidx__3 >= 0
     using hypothesis H63.
***  Proved C3:  begidx__3 >= 0
     using hypothesis H61.
***  Proved C2:  endidx__3 <= 2147483647
     using hypothesis H64.
***  Proved C4:  begidx__3 <= 2147483647
     using hypothesis H62.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_18.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H4).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H3).
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  rr_type__rritemtype__first <= foundtype__1
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H33 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).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H44 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified H49 on reading formula in, to give:
     %%%  H49:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H54 on reading formula in, to give:
     %%%  H54:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H54).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H55).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H54).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H55).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H67).
%%%  Simplified H74 on reading formula in, to give:
     %%%  H74:  not endidx__3 - begidx__3 + 1 > rr_type__maxdomainnamelength
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H53).
-S-  Applied substitution rule parsedomainn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C1:  endidx__3 >= - 2147483648
<S>  New C3:  begidx__3 >= - 2147483648
-S-  Applied substitution rule parsedomainn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C2:  endidx__3 <= 2147483647
<S>  New C4:  begidx__3 <= 2147483647
>>>  Restructured hypothesis H31 into:
     >>>  H31:  foundtype__1 = rr_type__recordindicator or zlength <= endidx__1
>>>  Restructured hypothesis H34 into:
     >>>  H34:  endidx__1 < zlength
>>>  Restructured hypothesis H74 into:
     >>>  H74:  endidx__3 - begidx__3 + 1 <= rr_type__maxdomainnamelength
-S-  Applied substitution rule parsedomainn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H74:  endidx__3 - begidx__3 <= 127
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H68:  endidx__3 - begidx__3 >= - 2147483648
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H69:  endidx__3 - begidx__3 <= 2147483647
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(23).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__first by:
          rr_type__domainnameortimespec.
<S>  New H19:  rr_type__domainnameortimespec <= foundtype__1
<S>  New H54:  rr_type__domainnameortimespec <= foundtype__3
-S-  Applied substitution rule parsedomainn_rules(24).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__last by:
          rr_type__other.
<S>  New H20:  foundtype__1 <= rr_type__other
<S>  New H55:  foundtype__3 <= rr_type__other
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H2:  zlength >= 1
<S>  New H4:  true
<S>  New H15:  begidx__1 >= 1
<S>  New H17:  endidx__1 >= 1
<S>  New H37:  endidx__1 >= 0
<S>  New H50:  begidx__3 >= 1
<S>  New H52:  endidx__3 >= 1
<S>  New H66:  endidx__3 - begidx__3 >= 0
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H3:  zlength <= 256
<S>  New H5:  true
<S>  New H16:  begidx__1 <= 256
<S>  New H18:  endidx__1 <= 256
<S>  New H38:  endidx__1 <= 255
<S>  New H51:  begidx__3 <= 256
<S>  New H53:  endidx__3 <= 256
<S>  New H67:  endidx__3 - begidx__3 <= 255
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C1:  endidx__3 >= - 2147483648
     using hypothesis H52.
***  Proved C3:  begidx__3 >= - 2147483648
     using hypothesis H50.
***  Proved C2:  endidx__3 <= 2147483647
     using hypothesis H53.
***  Proved C4:  begidx__3 <= 2147483647
     using hypothesis H51.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_19.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  endidx >= integer__base__first
%%%  Simplified H12 on reading formula in, to give:
     %%%  H12:  endidx <= integer__base__last
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  0 >= integer__base__first
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  0 <= integer__base__last
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H20 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  endidx + 1 <= zlength
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  foundtype__2 = rr_type__number -> for_all(i_ : integer, 
          begidx__2 <= i_ and i_ <= endidx__2 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  rr_type__rritemtype__first <= foundtype__2
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H29).
---  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).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H55 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H60 on reading formula in, to give:
     %%%  H60:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H65 on reading formula in, to give:
     %%%  H65:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H81 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H82 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H83 has been replaced by "true".  (It is already present, as 
          H77).
---  Hypothesis H84 has been replaced by "true".  (It is already present, as 
          H78).
%%%  Simplified H85 on reading formula in, to give:
     %%%  H85:  not endidx__3 - begidx__3 + 1 > rr_type__maxdomainnamelength
---  Hypothesis H86 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H87 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H88 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H89 has been replaced by "true".  (It is already present, as 
          H64).
-S-  Applied substitution rule parsedomainn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C1:  endidx__3 >= - 2147483648
<S>  New C3:  begidx__3 >= - 2147483648
-S-  Applied substitution rule parsedomainn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C2:  endidx__3 <= 2147483647
<S>  New C4:  begidx__3 <= 2147483647
>>>  Restructured hypothesis H42 into:
     >>>  H42:  foundtype__2 = rr_type__recordindicator or zlength <= endidx__2
>>>  Restructured hypothesis H45 into:
     >>>  H45:  endidx__2 < zlength
>>>  Restructured hypothesis H85 into:
     >>>  H85:  endidx__3 - begidx__3 + 1 <= rr_type__maxdomainnamelength
-S-  Applied substitution rule parsedomainn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H85:  endidx__3 - begidx__3 <= 127
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H11:  endidx >= - 2147483648
<S>  New H13:  true
<S>  New H79:  endidx__3 - begidx__3 >= - 2147483648
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H12:  endidx <= 2147483647
<S>  New H14:  true
<S>  New H80:  endidx__3 - begidx__3 <= 2147483647
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(23).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__first by:
          rr_type__domainnameortimespec.
<S>  New H30:  rr_type__domainnameortimespec <= foundtype__2
<S>  New H65:  rr_type__domainnameortimespec <= foundtype__3
-S-  Applied substitution rule parsedomainn_rules(24).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__last by:
          rr_type__other.
<S>  New H31:  foundtype__2 <= rr_type__other
<S>  New H66:  foundtype__3 <= rr_type__other
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H3:  zlength >= 1
<S>  New H5:  begidx >= 1
<S>  New H7:  endidx >= 1
<S>  New H9:  endidx >= 0
<S>  New H26:  begidx__2 >= 1
<S>  New H28:  endidx__2 >= 1
<S>  New H48:  endidx__2 >= 0
<S>  New H61:  begidx__3 >= 1
<S>  New H63:  endidx__3 >= 1
<S>  New H77:  endidx__3 - begidx__3 >= 0
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H4:  zlength <= 256
<S>  New H6:  begidx <= 256
<S>  New H8:  endidx <= 256
<S>  New H10:  endidx <= 255
<S>  New H27:  begidx__2 <= 256
<S>  New H29:  endidx__2 <= 256
<S>  New H49:  endidx__2 <= 255
<S>  New H62:  begidx__3 <= 256
<S>  New H64:  endidx__3 <= 256
<S>  New H78:  endidx__3 - begidx__3 <= 255
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C1:  endidx__3 >= - 2147483648
     using hypothesis H63.
***  Proved C3:  begidx__3 >= - 2147483648
     using hypothesis H61.
***  Proved C2:  endidx__3 <= 2147483647
     using hypothesis H64.
***  Proved C4:  begidx__3 <= 2147483647
     using hypothesis H62.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_20.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H4).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H3).
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  rr_type__rritemtype__first <= foundtype__1
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H33 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).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H44 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified H49 on reading formula in, to give:
     %%%  H49:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H54 on reading formula in, to give:
     %%%  H54:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H54).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H55).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H54).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H55).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H67).
%%%  Simplified H74 on reading formula in, to give:
     %%%  H74:  not endidx__3 - begidx__3 + 1 > rr_type__maxdomainnamelength
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H53).
***  Proved C1:  begidx__3 <= endidx__3 -> endidx__3 >= integer__first and 
          endidx__3 <= integer__last
     using hypotheses H79 & H80.
***  Proved C2:  begidx__3 <= endidx__3 -> begidx__3 >= integer__first and 
          begidx__3 <= integer__last
     using hypotheses H81 & H82.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_21.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  endidx >= integer__base__first
%%%  Simplified H12 on reading formula in, to give:
     %%%  H12:  endidx <= integer__base__last
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  0 >= integer__base__first
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  0 <= integer__base__last
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H20 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  endidx + 1 <= zlength
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  foundtype__2 = rr_type__number -> for_all(i_ : integer, 
          begidx__2 <= i_ and i_ <= endidx__2 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  rr_type__rritemtype__first <= foundtype__2
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H29).
---  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).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H55 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H60 on reading formula in, to give:
     %%%  H60:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H65 on reading formula in, to give:
     %%%  H65:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H81 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H82 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H83 has been replaced by "true".  (It is already present, as 
          H77).
---  Hypothesis H84 has been replaced by "true".  (It is already present, as 
          H78).
%%%  Simplified H85 on reading formula in, to give:
     %%%  H85:  not endidx__3 - begidx__3 + 1 > rr_type__maxdomainnamelength
---  Hypothesis H86 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H87 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H88 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H89 has been replaced by "true".  (It is already present, as 
          H64).
***  Proved C1:  begidx__3 <= endidx__3 -> endidx__3 >= integer__first and 
          endidx__3 <= integer__last
     using hypotheses H90 & H91.
***  Proved C2:  begidx__3 <= endidx__3 -> begidx__3 >= integer__first and 
          begidx__3 <= integer__last
     using hypotheses H92 & H93.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_22.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H4).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H3).
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  rr_type__rritemtype__first <= foundtype__1
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H33 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).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H44 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified H49 on reading formula in, to give:
     %%%  H49:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H54 on reading formula in, to give:
     %%%  H54:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H54).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H55).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H54).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H55).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H67).
%%%  Simplified H74 on reading formula in, to give:
     %%%  H74:  not endidx__3 - begidx__3 + 1 > rr_type__maxdomainnamelength
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H85 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H86 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H87 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H88 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H89 has been replaced by "true".  (It is already present, as 
          H46).
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  true
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  true
***  Proved C2:  endidx__3 - begidx__3 + 1 <= rr_type__maxdomainnamelength
     using hypothesis H74.
***  Proved C3:  true
***  Proved C4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
     using hypothesis H1.
***  Proved C5:  zlength >= rr_type__linelengthindex__first
     using hypothesis H2.
***  Proved C6:  zlength <= rr_type__linelengthindex__last
     using hypothesis H3.
***  Proved C7:  begidx__3 >= integer__first
     using hypothesis H81.
***  Proved C8:  begidx__3 <= integer__last
     using hypothesis H82.
***  Proved C9:  true
***  Proved C10:  begidx__3 <= endidx__3
     using hypothesis H46.
***  Proved C11:  endidx__3 >= rr_type__linelengthindex__first
     using hypothesis H52.
***  Proved C12:  endidx__3 <= rr_type__linelengthindex__last
     using hypothesis H53.
>>>  Restructured hypothesis H31 into:
     >>>  H31:  foundtype__1 = rr_type__recordindicator or zlength <= endidx__1
>>>  Restructured hypothesis H34 into:
     >>>  H34:  endidx__1 < zlength
>>>  Restructured hypothesis H74 into:
     >>>  H74:  endidx__3 - begidx__3 + 1 <= rr_type__maxdomainnamelength
+++  Using "A->B, A |- B" on hypotheses H83 & H46 yields a new hypothesis:
     +++  H90:  endidx__3 >= integer__first and endidx__3 <= integer__last
+++  Using "A->B, A |- B" on hypotheses H84 & H46 yields a new hypothesis:
     +++  H91:  begidx__3 >= integer__first and begidx__3 <= integer__last
-S-  Applied substitution rule parsedomainn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H74:  endidx__3 - begidx__3 <= 127
-S-  Applied substitution rule parsedomainn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H79:  endidx__3 >= - 2147483648
<S>  New H81:  begidx__3 >= - 2147483648
<S>  New H83:  begidx__3 <= endidx__3 -> endidx__3 >= - 2147483648 and 
          endidx__3 <= integer__last
<S>  New H84:  begidx__3 <= endidx__3 -> begidx__3 >= - 2147483648 and 
          begidx__3 <= integer__last
<S>  New H90:  endidx__3 >= - 2147483648 and endidx__3 <= integer__last
<S>  New H91:  begidx__3 >= - 2147483648 and begidx__3 <= integer__last
-S-  Applied substitution rule parsedomainn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H80:  endidx__3 <= 2147483647
<S>  New H82:  begidx__3 <= 2147483647
<S>  New H83:  begidx__3 <= endidx__3 -> endidx__3 >= - 2147483648 and 
          endidx__3 <= 2147483647
<S>  New H84:  begidx__3 <= endidx__3 -> begidx__3 >= - 2147483648 and 
          begidx__3 <= 2147483647
<S>  New H90:  endidx__3 >= - 2147483648 and endidx__3 <= 2147483647
<S>  New H91:  begidx__3 >= - 2147483648 and begidx__3 <= 2147483647
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H68:  endidx__3 - begidx__3 >= - 2147483648
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H69:  endidx__3 - begidx__3 <= 2147483647
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(23).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__first by:
          rr_type__domainnameortimespec.
<S>  New H19:  rr_type__domainnameortimespec <= foundtype__1
<S>  New H54:  rr_type__domainnameortimespec <= foundtype__3
-S-  Applied substitution rule parsedomainn_rules(24).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__last by:
          rr_type__other.
<S>  New H20:  foundtype__1 <= rr_type__other
<S>  New H55:  foundtype__3 <= rr_type__other
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H2:  zlength >= 1
<S>  New H4:  true
<S>  New H15:  begidx__1 >= 1
<S>  New H17:  endidx__1 >= 1
<S>  New H37:  endidx__1 >= 0
<S>  New H50:  begidx__3 >= 1
<S>  New H52:  endidx__3 >= 1
<S>  New H66:  endidx__3 - begidx__3 >= 0
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H3:  zlength <= 256
<S>  New H5:  true
<S>  New H16:  begidx__1 <= 256
<S>  New H18:  endidx__1 <= 256
<S>  New H38:  endidx__1 <= 255
<S>  New H51:  begidx__3 <= 256
<S>  New H53:  endidx__3 <= 256
<S>  New H67:  endidx__3 - begidx__3 <= 255
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C1:  begidx__3 >= 1
     using hypothesis H50.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_23.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  endidx >= integer__base__first
%%%  Simplified H12 on reading formula in, to give:
     %%%  H12:  endidx <= integer__base__last
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  0 >= integer__base__first
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  0 <= integer__base__last
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H20 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  endidx + 1 <= zlength
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  foundtype__2 = rr_type__number -> for_all(i_ : integer, 
          begidx__2 <= i_ and i_ <= endidx__2 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  rr_type__rritemtype__first <= foundtype__2
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H29).
---  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).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H55 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H60 on reading formula in, to give:
     %%%  H60:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H65 on reading formula in, to give:
     %%%  H65:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H81 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H82 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H83 has been replaced by "true".  (It is already present, as 
          H77).
---  Hypothesis H84 has been replaced by "true".  (It is already present, as 
          H78).
%%%  Simplified H85 on reading formula in, to give:
     %%%  H85:  not endidx__3 - begidx__3 + 1 > rr_type__maxdomainnamelength
---  Hypothesis H86 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H87 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H88 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H89 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H96 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H97 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H98 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H99 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H100 has been replaced by "true".  (It is already present, as 
          H57).
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  true
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  true
***  Proved C2:  endidx__3 - begidx__3 + 1 <= rr_type__maxdomainnamelength
     using hypothesis H85.
***  Proved C3:  true
***  Proved C4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
     using hypothesis H2.
***  Proved C5:  zlength >= rr_type__linelengthindex__first
     using hypothesis H3.
***  Proved C6:  zlength <= rr_type__linelengthindex__last
     using hypothesis H4.
***  Proved C7:  begidx__3 >= integer__first
     using hypothesis H92.
***  Proved C8:  begidx__3 <= integer__last
     using hypothesis H93.
***  Proved C9:  true
***  Proved C10:  begidx__3 <= endidx__3
     using hypothesis H57.
***  Proved C11:  endidx__3 >= rr_type__linelengthindex__first
     using hypothesis H63.
***  Proved C12:  endidx__3 <= rr_type__linelengthindex__last
     using hypothesis H64.
>>>  Restructured hypothesis H42 into:
     >>>  H42:  foundtype__2 = rr_type__recordindicator or zlength <= endidx__2
>>>  Restructured hypothesis H45 into:
     >>>  H45:  endidx__2 < zlength
>>>  Restructured hypothesis H85 into:
     >>>  H85:  endidx__3 - begidx__3 + 1 <= rr_type__maxdomainnamelength
+++  Using "A->B, A |- B" on hypotheses H94 & H57 yields a new hypothesis:
     +++  H101:  endidx__3 >= integer__first and endidx__3 <= integer__last
+++  Using "A->B, A |- B" on hypotheses H95 & H57 yields a new hypothesis:
     +++  H102:  begidx__3 >= integer__first and begidx__3 <= integer__last
-S-  Applied substitution rule parsedomainn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H85:  endidx__3 - begidx__3 <= 127
-S-  Applied substitution rule parsedomainn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H90:  endidx__3 >= - 2147483648
<S>  New H92:  begidx__3 >= - 2147483648
<S>  New H94:  begidx__3 <= endidx__3 -> endidx__3 >= - 2147483648 and 
          endidx__3 <= integer__last
<S>  New H95:  begidx__3 <= endidx__3 -> begidx__3 >= - 2147483648 and 
          begidx__3 <= integer__last
<S>  New H101:  endidx__3 >= - 2147483648 and endidx__3 <= integer__last
<S>  New H102:  begidx__3 >= - 2147483648 and begidx__3 <= integer__last
-S-  Applied substitution rule parsedomainn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H91:  endidx__3 <= 2147483647
<S>  New H93:  begidx__3 <= 2147483647
<S>  New H94:  begidx__3 <= endidx__3 -> endidx__3 >= - 2147483648 and 
          endidx__3 <= 2147483647
<S>  New H95:  begidx__3 <= endidx__3 -> begidx__3 >= - 2147483648 and 
          begidx__3 <= 2147483647
<S>  New H101:  endidx__3 >= - 2147483648 and endidx__3 <= 2147483647
<S>  New H102:  begidx__3 >= - 2147483648 and begidx__3 <= 2147483647
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H11:  endidx >= - 2147483648
<S>  New H13:  true
<S>  New H79:  endidx__3 - begidx__3 >= - 2147483648
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H12:  endidx <= 2147483647
<S>  New H14:  true
<S>  New H80:  endidx__3 - begidx__3 <= 2147483647
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(23).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__first by:
          rr_type__domainnameortimespec.
<S>  New H30:  rr_type__domainnameortimespec <= foundtype__2
<S>  New H65:  rr_type__domainnameortimespec <= foundtype__3
-S-  Applied substitution rule parsedomainn_rules(24).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__last by:
          rr_type__other.
<S>  New H31:  foundtype__2 <= rr_type__other
<S>  New H66:  foundtype__3 <= rr_type__other
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H3:  zlength >= 1
<S>  New H5:  begidx >= 1
<S>  New H7:  endidx >= 1
<S>  New H9:  endidx >= 0
<S>  New H26:  begidx__2 >= 1
<S>  New H28:  endidx__2 >= 1
<S>  New H48:  endidx__2 >= 0
<S>  New H61:  begidx__3 >= 1
<S>  New H63:  endidx__3 >= 1
<S>  New H77:  endidx__3 - begidx__3 >= 0
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H4:  zlength <= 256
<S>  New H6:  begidx <= 256
<S>  New H8:  endidx <= 256
<S>  New H10:  endidx <= 255
<S>  New H27:  begidx__2 <= 256
<S>  New H29:  endidx__2 <= 256
<S>  New H49:  endidx__2 <= 255
<S>  New H62:  begidx__3 <= 256
<S>  New H64:  endidx__3 <= 256
<S>  New H78:  endidx__3 - begidx__3 <= 255
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C1:  begidx__3 >= 1
     using hypothesis H61.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_24.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
***  Proved C1:  begidx >= 1
     using hypothesis H1.
***  Proved C2:  endidx - begidx + 1 <= rr_type__maxdomainnamelength
     using hypothesis H2.
***  Proved C3:  endidx = endidx__entry__loop__2
     using hypothesis H3.
***  Proved C4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
     using hypothesis H4.
***  Proved C5:  zlength >= rr_type__linelengthindex__first
     using hypothesis H5.
***  Proved C6:  zlength <= rr_type__linelengthindex__last
     using hypothesis H6.
***  Proved C7:  loop__2__i + 1 >= integer__first
     using hypothesis H7.
***  Proved C9:  loop__2__i + 1 >= begidx
     using hypothesis H9.
***  Proved C11:  endidx__entry__loop__2 >= rr_type__linelengthindex__first
     using hypothesis H11.
***  Proved C12:  endidx__entry__loop__2 <= rr_type__linelengthindex__last
     using hypothesis H12.
-S-  Applied substitution rule parsedomainn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H8:  loop__2__i <= 2147483647
<S>  New C8:  loop__2__i <= 2147483646
>>>  Restructured hypothesis H23 into:
     >>>  H23:  loop__2__i <> endidx__entry__loop__2
-S-  Applied substitution rule parsedomainn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H2:  endidx - begidx <= 127
-S-  Applied substitution rule parsedomainn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H7:  loop__2__i >= - 2147483648
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H19:  loop__2__i + 1 - begidx >= - 2147483648
<S>  New H21:  loop__2__i >= - 2147483649
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H20:  loop__2__i + 1 - begidx <= 2147483647
<S>  New H22:  loop__2__i <= 2147483646
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
<S>  New H13:  element(zonefileline, [loop__2__i]) >= 0
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H14:  element(zonefileline, [loop__2__i]) <= 255
<S>  New H4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H5:  zlength >= 1
<S>  New H11:  endidx__entry__loop__2 >= 1
<S>  New H15:  loop__2__i >= 1
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H6:  zlength <= 256
<S>  New H12:  endidx__entry__loop__2 <= 256
<S>  New H16:  loop__2__i <= 256
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
-S-  Applied substitution rule parsedomainn_rules(69).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__first by:
          1.
<S>  New H17:  loop__2__i + 1 - begidx >= 1
-S-  Applied substitution rule parsedomainn_rules(70).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__last by:
          128.
<S>  New H18:  loop__2__i + 1 - begidx <= 128
%%%  Hypotheses H10 & H23 together imply that
          loop__2__i < endidx__entry__loop__2.
     H10 & H23 have therefore been deleted and a new H24 added to this effect.
***  Proved C10:  loop__2__i + 1 <= endidx__entry__loop__2
     via its standard form, which is:
     Std.Fm C10:  endidx__entry__loop__2 - loop__2__i > 0
     using hypothesis H24.
***  Proved C8:  loop__2__i <= 2147483646
     using hypothesis H22.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_25.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
***  Proved C4:  loop__2__i <= rr_type__linelengthindex__last
     using hypotheses H10 & H12.
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
<S>  New C1:  element(zonefileline, [loop__2__i]) >= 0
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
<S>  New C2:  element(zonefileline, [loop__2__i]) <= 255
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H5:  zlength >= 1
<S>  New H11:  endidx__entry__loop__2 >= 1
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
<S>  New C3:  loop__2__i >= 1
-S-  Applied substitution rule parsedomainn_rules(69).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__first by:
          1.
<S>  New C5:  loop__2__i + 1 - begidx >= 1
-S-  Applied substitution rule parsedomainn_rules(70).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__last by:
          128.
<S>  New C6:  loop__2__i + 1 - begidx <= 128
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C7:  loop__2__i + 1 - begidx >= - 2147483648
<S>  New C9:  loop__2__i >= - 2147483649
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C8:  loop__2__i + 1 - begidx <= 2147483647
<S>  New C10:  loop__2__i <= 2147483646
***  Proved C1:  element(zonefileline, [loop__2__i]) >= 0
     using hypotheses H1, H4, H9, H10 & H12.
***  Proved C2:  element(zonefileline, [loop__2__i]) <= 255
     using hypotheses H1, H4, H9, H10 & H12.
***  Proved C3:  loop__2__i >= 1
     using hypotheses H1 & H9.
***  Proved C7:  loop__2__i + 1 - begidx >= - 2147483648
     using hypothesis H9.
***  Proved C9:  loop__2__i >= - 2147483649
     using hypotheses H1 & H9.
-S-  Applied substitution rule parsedomainn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H2:  endidx - begidx <= 127
-S-  Applied substitution rule parsedomainn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H7:  loop__2__i >= - 2147483648
-S-  Applied substitution rule parsedomainn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H8:  loop__2__i <= 2147483647
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
<S>  New H6:  zlength <= 256
<S>  New H12:  endidx__entry__loop__2 <= 256
***  Proved C5:  loop__2__i + 1 - begidx >= 1
     via its standard form, which is:
     Std.Fm C5:  - begidx + loop__2__i > - 1
     using hypothesis H9.
***  Proved C8:  loop__2__i + 1 - begidx <= 2147483647
     using hypotheses H1 & H8.
***  Proved C10:  loop__2__i <= 2147483646
     using hypotheses H10 & H12.
---  Eliminated hypothesis H7 (redundant, given H1 & H9).
---  Eliminated hypothesis H8 (redundant, given H10 & H12).
-S-  Eliminated hypothesis H3.
     This was achieved by replacing all occurrences of endidx by:
          endidx__entry__loop__2.
<S>  New H2:  endidx__entry__loop__2 - begidx <= 127
***  Proved C6:  loop__2__i + 1 - begidx <= 128
     via its standard form, which is:
     Std.Fm C6:  begidx - loop__2__i > - 128
     using hypotheses H2, H3 & H10.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_26.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H4).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H3).
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  rr_type__rritemtype__first <= foundtype__1
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H33 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).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H44 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified H49 on reading formula in, to give:
     %%%  H49:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H54 on reading formula in, to give:
     %%%  H54:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H54).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H55).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H54).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H55).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H67).
%%%  Simplified H74 on reading formula in, to give:
     %%%  H74:  not endidx__3 - begidx__3 + 1 > rr_type__maxdomainnamelength
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H85 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H86 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H87 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H88 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H90 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H91 has been replaced by "true".  (It is already present, as 
          H53).
***  Proved C3:  endidx__3 + 1 >= integer__first
     using hypothesis H79.
-S-  Applied substitution rule parsedomainn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H74:  not endidx__3 - begidx__3 > 127
<S>  New C1:  128 >= integer__first
<S>  New C2:  128 <= integer__last
-S-  Applied substitution rule parsedomainn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H79:  endidx__3 >= - 2147483648
<S>  New H81:  begidx__3 >= - 2147483648
<S>  New H83:  begidx__3 <= endidx__3 -> endidx__3 >= - 2147483648 and 
          endidx__3 <= integer__last
<S>  New H84:  begidx__3 <= endidx__3 -> begidx__3 >= - 2147483648 and 
          begidx__3 <= integer__last
<S>  New C1:  true
-S-  Applied substitution rule parsedomainn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H80:  endidx__3 <= 2147483647
<S>  New H82:  begidx__3 <= 2147483647
<S>  New H83:  begidx__3 <= endidx__3 -> endidx__3 >= - 2147483648 and 
          endidx__3 <= 2147483647
<S>  New H84:  begidx__3 <= endidx__3 -> begidx__3 >= - 2147483648 and 
          begidx__3 <= 2147483647
<S>  New C4:  endidx__3 <= 2147483646
<S>  New C2:  true
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H68:  endidx__3 - begidx__3 >= - 2147483648
<S>  New C5:  endidx__3 >= - 2147483649
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H69:  endidx__3 - begidx__3 <= 2147483647
<S>  New C6:  endidx__3 <= 2147483646
***  Proved C1:  true
***  Proved C4:  endidx__3 <= 2147483646
     using hypotheses H82 & H89.
***  Proved C2:  true
***  Proved C5:  endidx__3 >= - 2147483649
     using hypothesis H79.
***  Proved C6:  endidx__3 <= 2147483646
     using hypotheses H82 & H89.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_27.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  endidx >= integer__base__first
%%%  Simplified H12 on reading formula in, to give:
     %%%  H12:  endidx <= integer__base__last
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  0 >= integer__base__first
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  0 <= integer__base__last
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H20 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  endidx + 1 <= zlength
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  foundtype__2 = rr_type__number -> for_all(i_ : integer, 
          begidx__2 <= i_ and i_ <= endidx__2 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  rr_type__rritemtype__first <= foundtype__2
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H29).
---  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).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H55 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H60 on reading formula in, to give:
     %%%  H60:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H65 on reading formula in, to give:
     %%%  H65:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H81 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H82 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H83 has been replaced by "true".  (It is already present, as 
          H77).
---  Hypothesis H84 has been replaced by "true".  (It is already present, as 
          H78).
%%%  Simplified H85 on reading formula in, to give:
     %%%  H85:  not endidx__3 - begidx__3 + 1 > rr_type__maxdomainnamelength
---  Hypothesis H86 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H87 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H88 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H89 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H96 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H97 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H98 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H99 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H101 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H102 has been replaced by "true".  (It is already present, as 
          H64).
***  Proved C3:  endidx__3 + 1 >= integer__first
     using hypothesis H90.
-S-  Applied substitution rule parsedomainn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H85:  not endidx__3 - begidx__3 > 127
<S>  New C1:  128 >= integer__first
<S>  New C2:  128 <= integer__last
-S-  Applied substitution rule parsedomainn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H90:  endidx__3 >= - 2147483648
<S>  New H92:  begidx__3 >= - 2147483648
<S>  New H94:  begidx__3 <= endidx__3 -> endidx__3 >= - 2147483648 and 
          endidx__3 <= integer__last
<S>  New H95:  begidx__3 <= endidx__3 -> begidx__3 >= - 2147483648 and 
          begidx__3 <= integer__last
<S>  New C1:  true
-S-  Applied substitution rule parsedomainn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H91:  endidx__3 <= 2147483647
<S>  New H93:  begidx__3 <= 2147483647
<S>  New H94:  begidx__3 <= endidx__3 -> endidx__3 >= - 2147483648 and 
          endidx__3 <= 2147483647
<S>  New H95:  begidx__3 <= endidx__3 -> begidx__3 >= - 2147483648 and 
          begidx__3 <= 2147483647
<S>  New C4:  endidx__3 <= 2147483646
<S>  New C2:  true
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H11:  endidx >= - 2147483648
<S>  New H13:  true
<S>  New H79:  endidx__3 - begidx__3 >= - 2147483648
<S>  New C5:  endidx__3 >= - 2147483649
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H12:  endidx <= 2147483647
<S>  New H14:  true
<S>  New H80:  endidx__3 - begidx__3 <= 2147483647
<S>  New C6:  endidx__3 <= 2147483646
***  Proved C1:  true
***  Proved C4:  endidx__3 <= 2147483646
     using hypotheses H93 & H100.
***  Proved C2:  true
***  Proved C5:  endidx__3 >= - 2147483649
     using hypothesis H90.
***  Proved C6:  endidx__3 <= 2147483646
     using hypotheses H93 & H100.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_28.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
***  Proved C3:  endidx + 1 >= integer__first
     using hypotheses H3, H7 & H10.
***  Proved C5:  endidx + 1 >= integer__base__first
     using hypotheses H3, H10 & H21.
***  Proved C6:  endidx + 1 <= integer__base__last
     using hypotheses H3, H22 & H23.
-S-  Applied substitution rule parsedomainn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H2:  endidx - begidx <= 127
<S>  New C1:  128 >= integer__first
<S>  New C2:  128 <= integer__last
-S-  Applied substitution rule parsedomainn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H7:  loop__2__i >= - 2147483648
<S>  New C1:  true
-S-  Applied substitution rule parsedomainn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H8:  loop__2__i <= 2147483647
<S>  New C4:  endidx <= 2147483646
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H19:  loop__2__i + 1 - begidx >= - 2147483648
<S>  New H21:  loop__2__i >= - 2147483649
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H20:  loop__2__i + 1 - begidx <= 2147483647
<S>  New H22:  loop__2__i <= 2147483646
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
<S>  New H13:  element(zonefileline, [loop__2__i]) >= 0
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H14:  element(zonefileline, [loop__2__i]) <= 255
<S>  New H4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H5:  zlength >= 1
<S>  New H11:  endidx__entry__loop__2 >= 1
<S>  New H15:  loop__2__i >= 1
<S>  New H24:  endidx >= 1
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H6:  zlength <= 256
<S>  New H12:  endidx__entry__loop__2 <= 256
<S>  New H16:  loop__2__i <= 256
<S>  New H25:  endidx <= 256
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
-S-  Applied substitution rule parsedomainn_rules(69).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__first by:
          1.
<S>  New H17:  loop__2__i + 1 - begidx >= 1
-S-  Applied substitution rule parsedomainn_rules(70).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__last by:
          128.
<S>  New H18:  loop__2__i + 1 - begidx <= 128
***  Proved C4:  endidx <= 2147483646
     using hypothesis H25.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_29.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H4).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H3).
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  rr_type__rritemtype__first <= foundtype__1
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H33 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).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H44 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified H49 on reading formula in, to give:
     %%%  H49:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H54 on reading formula in, to give:
     %%%  H54:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H54).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H55).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H54).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H55).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H67).
%%%  Simplified H74 on reading formula in, to give:
     %%%  H74:  not endidx__3 - begidx__3 + 1 > rr_type__maxdomainnamelength
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H85 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H86 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H87 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H88 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H90 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H91 has been replaced by "true".  (It is already present, as 
          H53).
***  Proved C1:  endidx__3 + 1 <= rr_type__maxdomainnamelength -> 
          rr_type__maxdomainnamelength >= integer__first and 
          rr_type__maxdomainnamelength <= integer__last
     using hypotheses H92 & H93.
***  Proved C2:  endidx__3 + 1 <= rr_type__maxdomainnamelength -> endidx__3 + 1 
          >= integer__first and endidx__3 + 1 <= integer__last
     using hypotheses H94 & H95.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_30.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  endidx >= integer__base__first
%%%  Simplified H12 on reading formula in, to give:
     %%%  H12:  endidx <= integer__base__last
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  0 >= integer__base__first
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  0 <= integer__base__last
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H20 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  endidx + 1 <= zlength
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  foundtype__2 = rr_type__number -> for_all(i_ : integer, 
          begidx__2 <= i_ and i_ <= endidx__2 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  rr_type__rritemtype__first <= foundtype__2
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H29).
---  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).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H55 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H60 on reading formula in, to give:
     %%%  H60:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H65 on reading formula in, to give:
     %%%  H65:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H81 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H82 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H83 has been replaced by "true".  (It is already present, as 
          H77).
---  Hypothesis H84 has been replaced by "true".  (It is already present, as 
          H78).
%%%  Simplified H85 on reading formula in, to give:
     %%%  H85:  not endidx__3 - begidx__3 + 1 > rr_type__maxdomainnamelength
---  Hypothesis H86 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H87 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H88 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H89 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H96 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H97 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H98 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H99 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H101 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H102 has been replaced by "true".  (It is already present, as 
          H64).
***  Proved C1:  endidx__3 + 1 <= rr_type__maxdomainnamelength -> 
          rr_type__maxdomainnamelength >= integer__first and 
          rr_type__maxdomainnamelength <= integer__last
     using hypotheses H103 & H104.
***  Proved C2:  endidx__3 + 1 <= rr_type__maxdomainnamelength -> endidx__3 + 1 
          >= integer__first and endidx__3 + 1 <= integer__last
     using hypotheses H105 & H106.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_31.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
***  Proved C1:  endidx + 1 <= rr_type__maxdomainnamelength -> 
          rr_type__maxdomainnamelength >= integer__first and 
          rr_type__maxdomainnamelength <= integer__last
     using hypotheses H26 & H27.
***  Proved C2:  endidx + 1 <= rr_type__maxdomainnamelength -> endidx + 1 >= 
          integer__first and endidx + 1 <= integer__last
     using hypotheses H28 & H29.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_32.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H4).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H3).
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H19 on reading formula in, to give:
     %%%  H19:  rr_type__rritemtype__first <= foundtype__1
---  Hypothesis H21 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H22 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H33 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).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H37).
---  Hypothesis H42 has been replaced by "true".  (It is already present, as 
          H38).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H44 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified H49 on reading formula in, to give:
     %%%  H49:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H54 on reading formula in, to give:
     %%%  H54:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H56 has been replaced by "true".  (It is already present, as 
          H54).
---  Hypothesis H57 has been replaced by "true".  (It is already present, as 
          H55).
---  Hypothesis H58 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H59 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H60 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H61 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H62 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H63 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H64 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H65 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H54).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H55).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H67).
%%%  Simplified H74 on reading formula in, to give:
     %%%  H74:  not endidx__3 - begidx__3 + 1 > rr_type__maxdomainnamelength
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H77 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H78 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H85 has been replaced by "true".  (It is already present, as 
          H50).
---  Hypothesis H86 has been replaced by "true".  (It is already present, as 
          H51).
---  Hypothesis H87 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H88 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H90 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H91 has been replaced by "true".  (It is already present, as 
          H53).
---  Hypothesis H100 has been replaced by "true".  (It is already present, as 
          H52).
---  Hypothesis H101 has been replaced by "true".  (It is already present, as 
          H53).
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  true
***  Proved C2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
     using hypothesis H1.
***  Proved C3:  zlength >= rr_type__linelengthindex__first
     using hypothesis H2.
***  Proved C4:  zlength <= rr_type__linelengthindex__last
     using hypothesis H3.
***  Proved C5:  endidx__3 + 1 >= integer__first
     using hypothesis H94.
***  Proved C6:  endidx__3 + 1 <= integer__last
     using hypothesis H95.
***  Proved C7:  true
***  Proved C8:  endidx__3 + 1 <= rr_type__maxdomainnamelength
     using hypothesis H102.
>>>  Restructured hypothesis H31 into:
     >>>  H31:  foundtype__1 = rr_type__recordindicator or zlength <= endidx__1
>>>  Restructured hypothesis H34 into:
     >>>  H34:  endidx__1 < zlength
>>>  Restructured hypothesis H74 into:
     >>>  H74:  endidx__3 - begidx__3 + 1 <= rr_type__maxdomainnamelength
>>>  Restructured hypothesis H89 into:
     >>>  H89:  endidx__3 < begidx__3
+++  Using "A->B, A |- B" on hypotheses H83 & H46 yields a new hypothesis:
     +++  H103:  endidx__3 >= integer__first and endidx__3 <= integer__last
+++  Using "A->B, A |- B" on hypotheses H84 & H46 yields a new hypothesis:
     +++  H104:  begidx__3 >= integer__first and begidx__3 <= integer__last
+++  Using "A->B, A |- B" on hypotheses H98 & H102 yields a new hypothesis:
     +++  H105:  rr_type__maxdomainnamelength >= integer__first and 
          rr_type__maxdomainnamelength <= integer__last
+++  Using "A->B, A |- B" on hypotheses H99 & H102 yields a new hypothesis:
     +++  H106:  endidx__3 + 1 >= integer__first and endidx__3 + 1 <= 
          integer__last
-S-  Applied substitution rule parsedomainn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H74:  endidx__3 - begidx__3 <= 127
<S>  New H92:  128 >= integer__first
<S>  New H93:  128 <= integer__last
<S>  New H98:  endidx__3 <= 127 -> 128 >= integer__first and 128 <= 
          integer__last
<S>  New H99:  endidx__3 <= 127 -> endidx__3 + 1 >= integer__first and 
          endidx__3 + 1 <= integer__last
<S>  New H102:  endidx__3 <= 127
<S>  New H105:  128 >= integer__first and 128 <= integer__last
-S-  Applied substitution rule parsedomainn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H79:  endidx__3 >= - 2147483648
<S>  New H81:  begidx__3 >= - 2147483648
<S>  New H83:  begidx__3 <= endidx__3 -> endidx__3 >= - 2147483648 and 
          endidx__3 <= integer__last
<S>  New H84:  begidx__3 <= endidx__3 -> begidx__3 >= - 2147483648 and 
          begidx__3 <= integer__last
<S>  New H94:  endidx__3 >= - 2147483649
<S>  New H103:  endidx__3 >= - 2147483648 and endidx__3 <= integer__last
<S>  New H104:  begidx__3 >= - 2147483648 and begidx__3 <= integer__last
<S>  New H106:  endidx__3 >= - 2147483649 and endidx__3 + 1 <= integer__last
<S>  New H92:  true
<S>  New H98:  endidx__3 <= 127 -> 128 <= integer__last
<S>  New H99:  endidx__3 <= 127 -> endidx__3 >= - 2147483649 and endidx__3 + 1 
          <= integer__last
<S>  New H105:  128 <= integer__last
-S-  Applied substitution rule parsedomainn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H80:  endidx__3 <= 2147483647
<S>  New H82:  begidx__3 <= 2147483647
<S>  New H95:  endidx__3 <= 2147483646
<S>  New H93:  true
<S>  New H83:  begidx__3 <= endidx__3 -> endidx__3 >= - 2147483648 and 
          endidx__3 <= 2147483647
<S>  New H84:  begidx__3 <= endidx__3 -> begidx__3 >= - 2147483648 and 
          begidx__3 <= 2147483647
<S>  New H103:  endidx__3 >= - 2147483648 and endidx__3 <= 2147483647
<S>  New H104:  begidx__3 >= - 2147483648 and begidx__3 <= 2147483647
<S>  New H106:  endidx__3 >= - 2147483649 and endidx__3 <= 2147483646
<S>  New H98:  true
<S>  New H99:  endidx__3 <= 127 -> endidx__3 >= - 2147483649 and endidx__3 <= 
          2147483646
<S>  New H105:  true
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H68:  endidx__3 - begidx__3 >= - 2147483648
<S>  New H96:  endidx__3 >= - 2147483649
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H69:  endidx__3 - begidx__3 <= 2147483647
<S>  New H97:  endidx__3 <= 2147483646
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(23).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__first by:
          rr_type__domainnameortimespec.
<S>  New H19:  rr_type__domainnameortimespec <= foundtype__1
<S>  New H54:  rr_type__domainnameortimespec <= foundtype__3
-S-  Applied substitution rule parsedomainn_rules(24).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__last by:
          rr_type__other.
<S>  New H20:  foundtype__1 <= rr_type__other
<S>  New H55:  foundtype__3 <= rr_type__other
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H2:  zlength >= 1
<S>  New H4:  true
<S>  New H15:  begidx__1 >= 1
<S>  New H17:  endidx__1 >= 1
<S>  New H37:  endidx__1 >= 0
<S>  New H50:  begidx__3 >= 1
<S>  New H52:  endidx__3 >= 1
<S>  New H66:  endidx__3 - begidx__3 >= 0
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H3:  zlength <= 256
<S>  New H5:  true
<S>  New H16:  begidx__1 <= 256
<S>  New H18:  endidx__1 <= 256
<S>  New H38:  endidx__1 <= 255
<S>  New H51:  begidx__3 <= 256
<S>  New H53:  endidx__3 <= 256
<S>  New H67:  endidx__3 - begidx__3 <= 255
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C1:  endidx__3 >= 1
     using hypothesis H52.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_33.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified H9 on reading formula in, to give:
     %%%  H9:  endidx + 1 >= rr_type__linelengthindex__first
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  endidx + 1 <= rr_type__linelengthindex__last
%%%  Simplified H11 on reading formula in, to give:
     %%%  H11:  endidx >= integer__base__first
%%%  Simplified H12 on reading formula in, to give:
     %%%  H12:  endidx <= integer__base__last
%%%  Simplified H13 on reading formula in, to give:
     %%%  H13:  0 >= integer__base__first
%%%  Simplified H14 on reading formula in, to give:
     %%%  H14:  0 <= integer__base__last
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H20 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  endidx + 1 <= zlength
%%%  Simplified H25 on reading formula in, to give:
     %%%  H25:  foundtype__2 = rr_type__number -> for_all(i_ : integer, 
          begidx__2 <= i_ and i_ <= endidx__2 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  rr_type__rritemtype__first <= foundtype__2
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H27).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H40 has been replaced by "true".  (It is already present, as 
          H30).
---  Hypothesis H41 has been replaced by "true".  (It is already present, as 
          H31).
---  Hypothesis H43 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H44 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H29).
---  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).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H48).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H49).
---  Hypothesis H54 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H55 has been replaced by "true".  (It is already present, as H4)
          .
%%%  Simplified H60 on reading formula in, to give:
     %%%  H60:  foundtype__3 = rr_type__number -> for_all(i_ : integer, 
          begidx__3 <= i_ and i_ <= endidx__3 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H65 on reading formula in, to give:
     %%%  H65:  rr_type__rritemtype__first <= foundtype__3
---  Hypothesis H67 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H68 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H69 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H70 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H71 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H72 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H73 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H74 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H75 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H76 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H81 has been replaced by "true".  (It is already present, as 
          H65).
---  Hypothesis H82 has been replaced by "true".  (It is already present, as 
          H66).
---  Hypothesis H83 has been replaced by "true".  (It is already present, as 
          H77).
---  Hypothesis H84 has been replaced by "true".  (It is already present, as 
          H78).
%%%  Simplified H85 on reading formula in, to give:
     %%%  H85:  not endidx__3 - begidx__3 + 1 > rr_type__maxdomainnamelength
---  Hypothesis H86 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H87 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H88 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H89 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H96 has been replaced by "true".  (It is already present, as 
          H61).
---  Hypothesis H97 has been replaced by "true".  (It is already present, as 
          H62).
---  Hypothesis H98 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H99 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H101 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H102 has been replaced by "true".  (It is already present, as 
          H64).
---  Hypothesis H111 has been replaced by "true".  (It is already present, as 
          H63).
---  Hypothesis H112 has been replaced by "true".  (It is already present, as 
          H64).
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  true
***  Proved C2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
     using hypothesis H2.
***  Proved C3:  zlength >= rr_type__linelengthindex__first
     using hypothesis H3.
***  Proved C4:  zlength <= rr_type__linelengthindex__last
     using hypothesis H4.
***  Proved C5:  endidx__3 + 1 >= integer__first
     using hypothesis H105.
***  Proved C6:  endidx__3 + 1 <= integer__last
     using hypothesis H106.
***  Proved C7:  true
***  Proved C8:  endidx__3 + 1 <= rr_type__maxdomainnamelength
     using hypothesis H113.
>>>  Restructured hypothesis H42 into:
     >>>  H42:  foundtype__2 = rr_type__recordindicator or zlength <= endidx__2
>>>  Restructured hypothesis H45 into:
     >>>  H45:  endidx__2 < zlength
>>>  Restructured hypothesis H85 into:
     >>>  H85:  endidx__3 - begidx__3 + 1 <= rr_type__maxdomainnamelength
>>>  Restructured hypothesis H100 into:
     >>>  H100:  endidx__3 < begidx__3
+++  Using "A->B, A |- B" on hypotheses H94 & H57 yields a new hypothesis:
     +++  H114:  endidx__3 >= integer__first and endidx__3 <= integer__last
+++  Using "A->B, A |- B" on hypotheses H95 & H57 yields a new hypothesis:
     +++  H115:  begidx__3 >= integer__first and begidx__3 <= integer__last
+++  Using "A->B, A |- B" on hypotheses H109 & H113 yields a new hypothesis:
     +++  H116:  rr_type__maxdomainnamelength >= integer__first and 
          rr_type__maxdomainnamelength <= integer__last
+++  Using "A->B, A |- B" on hypotheses H110 & H113 yields a new hypothesis:
     +++  H117:  endidx__3 + 1 >= integer__first and endidx__3 + 1 <= 
          integer__last
-S-  Applied substitution rule parsedomainn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H85:  endidx__3 - begidx__3 <= 127
<S>  New H103:  128 >= integer__first
<S>  New H104:  128 <= integer__last
<S>  New H109:  endidx__3 <= 127 -> 128 >= integer__first and 128 <= 
          integer__last
<S>  New H110:  endidx__3 <= 127 -> endidx__3 + 1 >= integer__first and 
          endidx__3 + 1 <= integer__last
<S>  New H113:  endidx__3 <= 127
<S>  New H116:  128 >= integer__first and 128 <= integer__last
-S-  Applied substitution rule parsedomainn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H90:  endidx__3 >= - 2147483648
<S>  New H92:  begidx__3 >= - 2147483648
<S>  New H94:  begidx__3 <= endidx__3 -> endidx__3 >= - 2147483648 and 
          endidx__3 <= integer__last
<S>  New H95:  begidx__3 <= endidx__3 -> begidx__3 >= - 2147483648 and 
          begidx__3 <= integer__last
<S>  New H105:  endidx__3 >= - 2147483649
<S>  New H114:  endidx__3 >= - 2147483648 and endidx__3 <= integer__last
<S>  New H115:  begidx__3 >= - 2147483648 and begidx__3 <= integer__last
<S>  New H117:  endidx__3 >= - 2147483649 and endidx__3 + 1 <= integer__last
<S>  New H103:  true
<S>  New H109:  endidx__3 <= 127 -> 128 <= integer__last
<S>  New H110:  endidx__3 <= 127 -> endidx__3 >= - 2147483649 and endidx__3 + 1 
          <= integer__last
<S>  New H116:  128 <= integer__last
-S-  Applied substitution rule parsedomainn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H91:  endidx__3 <= 2147483647
<S>  New H93:  begidx__3 <= 2147483647
<S>  New H106:  endidx__3 <= 2147483646
<S>  New H104:  true
<S>  New H94:  begidx__3 <= endidx__3 -> endidx__3 >= - 2147483648 and 
          endidx__3 <= 2147483647
<S>  New H95:  begidx__3 <= endidx__3 -> begidx__3 >= - 2147483648 and 
          begidx__3 <= 2147483647
<S>  New H114:  endidx__3 >= - 2147483648 and endidx__3 <= 2147483647
<S>  New H115:  begidx__3 >= - 2147483648 and begidx__3 <= 2147483647
<S>  New H117:  endidx__3 >= - 2147483649 and endidx__3 <= 2147483646
<S>  New H109:  true
<S>  New H110:  endidx__3 <= 127 -> endidx__3 >= - 2147483649 and endidx__3 <= 
          2147483646
<S>  New H116:  true
-S-  Applied substitution rule parsedomainn_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H11:  endidx >= - 2147483648
<S>  New H13:  true
<S>  New H79:  endidx__3 - begidx__3 >= - 2147483648
<S>  New H107:  endidx__3 >= - 2147483649
-S-  Applied substitution rule parsedomainn_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H12:  endidx <= 2147483647
<S>  New H14:  true
<S>  New H80:  endidx__3 - begidx__3 <= 2147483647
<S>  New H108:  endidx__3 <= 2147483646
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(23).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__first by:
          rr_type__domainnameortimespec.
<S>  New H30:  rr_type__domainnameortimespec <= foundtype__2
<S>  New H65:  rr_type__domainnameortimespec <= foundtype__3
-S-  Applied substitution rule parsedomainn_rules(24).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__last by:
          rr_type__other.
<S>  New H31:  foundtype__2 <= rr_type__other
<S>  New H66:  foundtype__3 <= rr_type__other
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H3:  zlength >= 1
<S>  New H5:  begidx >= 1
<S>  New H7:  endidx >= 1
<S>  New H9:  endidx >= 0
<S>  New H26:  begidx__2 >= 1
<S>  New H28:  endidx__2 >= 1
<S>  New H48:  endidx__2 >= 0
<S>  New H61:  begidx__3 >= 1
<S>  New H63:  endidx__3 >= 1
<S>  New H77:  endidx__3 - begidx__3 >= 0
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H4:  zlength <= 256
<S>  New H6:  begidx <= 256
<S>  New H8:  endidx <= 256
<S>  New H10:  endidx <= 255
<S>  New H27:  begidx__2 <= 256
<S>  New H29:  endidx__2 <= 256
<S>  New H49:  endidx__2 <= 255
<S>  New H62:  begidx__3 <= 256
<S>  New H64:  endidx__3 <= 256
<S>  New H78:  endidx__3 - begidx__3 <= 255
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C1:  endidx__3 >= 1
     using hypothesis H63.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_34.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H25).
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified C7 on reading formula in, to give:
     %%%  C7:  true
***  Proved C1:  endidx >= 1
     using hypotheses H1, H3, H9 & H10.
***  Proved C2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
     using hypothesis H4.
***  Proved C3:  zlength >= rr_type__linelengthindex__first
     using hypothesis H5.
***  Proved C4:  zlength <= rr_type__linelengthindex__last
     using hypothesis H6.
***  Proved C5:  endidx + 1 >= integer__first
     using hypothesis H28.
***  Proved C6:  endidx + 1 <= integer__last
     using hypothesis H29.
***  Proved C7:  true
***  Proved C8:  endidx + 1 <= rr_type__maxdomainnamelength
     using hypothesis H36.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_35.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
***  Proved C1:  endidx >= 1
     using hypothesis H1.
***  Proved C2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
     using hypothesis H2.
***  Proved C3:  zlength >= rr_type__linelengthindex__first
     using hypothesis H3.
***  Proved C4:  zlength <= rr_type__linelengthindex__last
     using hypothesis H4.
***  Proved C5:  loop__3__i + 1 >= integer__first
     using hypothesis H5.
***  Proved C7:  loop__3__i + 1 >= endidx + 1
     using hypothesis H7.
-S-  Applied substitution rule parsedomainn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H6:  loop__3__i <= 2147483647
<S>  New C6:  loop__3__i <= 2147483646
-S-  Applied substitution rule parsedomainn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H8:  loop__3__i <= 128
<S>  New H13:  not loop__3__i = 128
<S>  New C8:  loop__3__i <= 127
***  Proved C6:  loop__3__i <= 2147483646
     using hypotheses H8 & H13.
***  Proved C8:  loop__3__i <= 127
     using hypotheses H8 & H13.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsedomainname_36.  @@@@@@@@@@
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
-S-  Applied substitution rule parsedomainn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
<S>  New C1:  true
-S-  Applied substitution rule parsedomainn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H2:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
<S>  New C2:  true
-S-  Applied substitution rule parsedomainn_rules(69).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__first by:
          1.
<S>  New C3:  loop__3__i >= 1
-S-  Applied substitution rule parsedomainn_rules(70).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__last by:
          128.
<S>  New C4:  loop__3__i <= 128
***  Proved C1:  true
***  Proved C2:  true
***  Proved C3:  loop__3__i >= 1
     using hypotheses H1 & H7.
-S-  Applied substitution rule parsedomainn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H8:  loop__3__i <= 128
-S-  Applied substitution rule parsedomainn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H5:  loop__3__i >= - 2147483648
-S-  Applied substitution rule parsedomainn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H6:  loop__3__i <= 2147483647
-S-  Applied substitution rule parsedomainn_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
<S>  New H3:  zlength >= 1
-S-  Applied substitution rule parsedomainn_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H4:  zlength <= 256
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C4:  loop__3__i <= 128
     using hypothesis H8.
***  PROVED VC.


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


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


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


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


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


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


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


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

