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

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



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

function Rr_Type.ConvertDomainNameToWire






@@@@@@@@@@  VC: function_convertdomainnametowire_1.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  domainnamelength(domainnameversion) = 1 and (element(
          domainnameversion, [1]) = 32 or element(domainnameversion, [2]) = 32) 
          or (domainnamelength(domainnameversion) = maxdomainnamelength or 
          element(domainnameversion, [domainnamelength(domainnameversion) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          domainnameversion) -> element(domainnameversion, [q_]) <> 32))
***  Proved C1:  domainnamelength(domainnameversion) >= 
          domainnamestringtypeindex__first
     using hypothesis H2.
***  Proved C2:  domainnamelength(domainnameversion) <= 
          domainnamestringtypeindex__last
     using hypothesis H3.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_2.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  domainnamelength(domainnameversion) = 1 and (element(
          domainnameversion, [1]) = 32 or element(domainnameversion, [2]) = 32) 
          or (domainnamelength(domainnameversion) = maxdomainnamelength or 
          element(domainnameversion, [domainnamelength(domainnameversion) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          domainnameversion) -> element(domainnameversion, [q_]) <> 32))
---  Hypothesis H5 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H3).
-S-  Applied substitution rule convertdomai_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C1:  domainnamelength(domainnameversion) >= - 2147483647
<S>  New C5:  domainnamestringtypeindex__first >= - 2147483648
-S-  Applied substitution rule convertdomai_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C2:  domainnamelength(domainnameversion) <= 2147483648
<S>  New C6:  domainnamestringtypeindex__first <= 2147483647
-S-  Applied substitution rule convertdomai_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C3:  domainnamelength(domainnameversion) >= - 2147483647
-S-  Applied substitution rule convertdomai_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C4:  domainnamelength(domainnameversion) <= 2147483648
-S-  Applied substitution rule convertdomai_rules(25).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> character__first <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= character__last)
<S>  New H2:  domainnamelength(domainnameversion) >= 1
<S>  New C5:  true
<S>  New C6:  true
***  Proved C1:  domainnamelength(domainnameversion) >= - 2147483647
     using hypothesis H2.
***  Proved C3:  domainnamelength(domainnameversion) >= - 2147483647
     using hypothesis H2.
***  Proved C5:  true
***  Proved C6:  true
-S-  Applied substitution rule convertdomai_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H4:  domainnamelength(domainnameversion) = 1 and (element(
          domainnameversion, [1]) = 32 or element(domainnameversion, [2]) = 32) 
          or (domainnamelength(domainnameversion) = 128 or element(
          domainnameversion, [domainnamelength(domainnameversion) + 1]) = 32 
          and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          domainnameversion) -> element(domainnameversion, [q_]) <> 32))
-S-  Applied substitution rule convertdomai_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(domainnameversion, [
          i___1]) and element(domainnameversion, [i___1]) <= character__last)
-S-  Applied substitution rule convertdomai_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(domainnameversion, [
          i___1]) and element(domainnameversion, [i___1]) <= 255)
-S-  Applied substitution rule convertdomai_rules(26).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H3:  domainnamelength(domainnameversion) <= 128
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(domainnameversion, [i___1]) and element(domainnameversion, [
          i___1]) <= 255)
***  Proved C2:  domainnamelength(domainnameversion) <= 2147483648
     using hypothesis H3.
***  Proved C4:  domainnamelength(domainnameversion) <= 2147483648
     using hypothesis H3.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_3.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  domainnamelength(domainnameversion) = 1 and (element(
          domainnameversion, [1]) = 32 or element(domainnameversion, [2]) = 32) 
          or (domainnamelength(domainnameversion) = maxdomainnamelength or 
          element(domainnameversion, [domainnamelength(domainnameversion) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          domainnameversion) -> element(domainnameversion, [q_]) <> 32))
---  Hypothesis H5 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H3).
***  Proved C1:  domainnamestringtypeindex__first <= domainnamelength(
          domainnameversion) - 1 -> domainnamelength(domainnameversion) - 1 >= 
          integer__first and domainnamelength(domainnameversion) - 1 <= 
          integer__last
     using hypotheses H9 & H10.
***  Proved C2:  domainnamestringtypeindex__first <= domainnamelength(
          domainnameversion) - 1 -> domainnamestringtypeindex__first >= 
          integer__first and domainnamestringtypeindex__first <= integer__last
     using hypotheses H13 & H14.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_4.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  domainnamelength(domainnameversion) = 1 and (element(
          domainnameversion, [1]) = 32 or element(domainnameversion, [2]) = 32) 
          or (domainnamelength(domainnameversion) = maxdomainnamelength or 
          element(domainnameversion, [domainnamelength(domainnameversion) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          domainnameversion) -> element(domainnameversion, [q_]) <> 32))
---  Hypothesis H5 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
%%%  Simplified C6 on reading formula in, to give:
     %%%  C6:  true
***  Proved C3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
     using hypothesis H1.
***  Proved C4:  domainnamestringtypeindex__first >= integer__first
     using hypothesis H13.
***  Proved C5:  domainnamestringtypeindex__first <= integer__last
     using hypothesis H14.
***  Proved C6:  true
***  Proved C7:  domainnamestringtypeindex__first <= domainnamelength(
          domainnameversion) - 1
     using hypothesis H19.
***  Proved C8:  domainnamelength(domainnameversion) >= 
          domainnamestringtypeindex__first
     using hypothesis H2.
***  Proved C9:  domainnamelength(domainnameversion) <= 
          domainnamestringtypeindex__last
     using hypothesis H3.
-S-  Applied substitution rule convertdomai_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H4:  domainnamelength(domainnameversion) = 1 and (element(
          domainnameversion, [1]) = 32 or element(domainnameversion, [2]) = 32) 
          or (domainnamelength(domainnameversion) = 128 or element(
          domainnameversion, [domainnamelength(domainnameversion) + 1]) = 32 
          and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          domainnameversion) -> element(domainnameversion, [q_]) <> 32))
<S>  New C2:  domainnamelength(domainnameversion) <= 128
+++  Using "A->B, A |- B" on hypotheses H15 & H19 yields a new hypothesis:
     +++  H20:  domainnamelength(domainnameversion) - 1 >= integer__first and 
          domainnamelength(domainnameversion) - 1 <= integer__last
+++  Using "A->B, A |- B" on hypotheses H16 & H19 yields a new hypothesis:
     +++  H21:  domainnamestringtypeindex__first >= integer__first and 
          domainnamestringtypeindex__first <= integer__last
-S-  Applied substitution rule convertdomai_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H9:  domainnamelength(domainnameversion) >= - 2147483647
<S>  New H13:  domainnamestringtypeindex__first >= - 2147483648
<S>  New H15:  domainnamestringtypeindex__first <= domainnamelength(
          domainnameversion) - 1 -> domainnamelength(domainnameversion) >= - 
          2147483647 and domainnamelength(domainnameversion) - 1 <= 
          integer__last
<S>  New H16:  domainnamestringtypeindex__first <= domainnamelength(
          domainnameversion) - 1 -> domainnamestringtypeindex__first >= - 
          2147483648 and domainnamestringtypeindex__first <= integer__last
<S>  New H20:  domainnamelength(domainnameversion) >= - 2147483647 and 
          domainnamelength(domainnameversion) - 1 <= integer__last
<S>  New H21:  domainnamestringtypeindex__first >= - 2147483648 and 
          domainnamestringtypeindex__first <= integer__last
-S-  Applied substitution rule convertdomai_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H10:  domainnamelength(domainnameversion) <= 2147483648
<S>  New H14:  domainnamestringtypeindex__first <= 2147483647
<S>  New H15:  domainnamestringtypeindex__first <= domainnamelength(
          domainnameversion) - 1 -> domainnamelength(domainnameversion) >= - 
          2147483647 and domainnamelength(domainnameversion) <= 2147483648
<S>  New H16:  domainnamestringtypeindex__first <= domainnamelength(
          domainnameversion) - 1 -> domainnamestringtypeindex__first >= - 
          2147483648 and domainnamestringtypeindex__first <= 2147483647
<S>  New H20:  domainnamelength(domainnameversion) >= - 2147483647 and 
          domainnamelength(domainnameversion) <= 2147483648
<S>  New H21:  domainnamestringtypeindex__first >= - 2147483648 and 
          domainnamestringtypeindex__first <= 2147483647
-S-  Applied substitution rule convertdomai_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H11:  domainnamelength(domainnameversion) >= - 2147483647
-S-  Applied substitution rule convertdomai_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H12:  domainnamelength(domainnameversion) <= 2147483648
-S-  Applied substitution rule convertdomai_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= character__last)
-S-  Applied substitution rule convertdomai_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= 255)
-S-  Applied substitution rule convertdomai_rules(25).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H2:  domainnamelength(domainnameversion) >= 1
<S>  New H19:  2 <= domainnamelength(domainnameversion)
<S>  New H13:  true
<S>  New H14:  true
<S>  New H15:  2 <= domainnamelength(domainnameversion) -> domainnamelength(
          domainnameversion) >= - 2147483647 and domainnamelength(
          domainnameversion) <= 2147483648
<S>  New H16:  true
<S>  New H21:  true
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(domainnameversion, [
          i___1]) and element(domainnameversion, [i___1]) <= 255)
-S-  Applied substitution rule convertdomai_rules(26).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H3:  domainnamelength(domainnameversion) <= 128
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(domainnameversion, [i___1]) and element(domainnameversion, [
          i___1]) <= 255)
***  Proved C1:  domainnamelength(domainnameversion) >= 1
     using hypothesis H2.
***  Proved C2:  domainnamelength(domainnameversion) <= 128
     using hypothesis H3.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_5.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H22).
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
***  Proved C1:  lengthofdomainname >= 1
     using hypothesis H1.
***  Proved C2:  lengthofdomainname <= maxdomainnamelength
     using hypothesis H2.
***  Proved C3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
     using hypothesis H3.
***  Proved C4:  loop__1__i + 1 >= integer__first
     using hypothesis H4.
***  Proved C6:  loop__1__i + 1 >= domainnamestringtypeindex__first
     using hypothesis H6.
***  Proved C8:  lengthofdomainname__entry__loop__1 >= 
          domainnamestringtypeindex__first
     using hypothesis H8.
***  Proved C9:  lengthofdomainname__entry__loop__1 <= 
          domainnamestringtypeindex__last
     using hypothesis H9.
-S-  Applied substitution rule convertdomai_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H5:  loop__1__i <= 2147483647
<S>  New C5:  loop__1__i <= 2147483646
>>>  Restructured hypothesis H25 into:
     >>>  H25:  loop__1__i <> lengthofdomainname__entry__loop__1 - 1
-S-  Applied substitution rule convertdomai_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H2:  lengthofdomainname <= 128
-S-  Applied substitution rule convertdomai_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H4:  loop__1__i >= - 2147483648
-S-  Applied substitution rule convertdomai_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H15:  loop__1__i >= - 2147483649
-S-  Applied substitution rule convertdomai_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H16:  loop__1__i <= 2147483646
-S-  Applied substitution rule convertdomai_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= character__last)
<S>  New H21:  findperiod(domainnameversion, loop__1__i + 1) >= 0
-S-  Applied substitution rule convertdomai_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H22:  findperiod(domainnameversion, loop__1__i + 1) <= 255
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= 255)
-S-  Applied substitution rule convertdomai_rules(20).
     This was achieved by replacing all occurrences of linelengthindex__first 
          by:
          1.
<S>  New H13:  loop__1__i >= 0
-S-  Applied substitution rule convertdomai_rules(21).
     This was achieved by replacing all occurrences of linelengthindex__last by:
          256.
<S>  New H14:  loop__1__i <= 255
-S-  Applied substitution rule convertdomai_rules(25).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H6:  loop__1__i >= 1
<S>  New H8:  lengthofdomainname__entry__loop__1 >= 1
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(domainnameversion, [
          i___1]) and element(domainnameversion, [i___1]) <= 255)
-S-  Applied substitution rule convertdomai_rules(26).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H9:  lengthofdomainname__entry__loop__1 <= 128
<S>  New H11:  loop__1__i <= 128
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(domainnameversion, [i___1]) and element(domainnameversion, [
          i___1]) <= 255)
-S-  Applied substitution rule convertdomai_rules(30).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__first by:
          1.
<S>  New H17:  loop__1__i >= 0
-S-  Applied substitution rule convertdomai_rules(31).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__last by:
          129.
<S>  New H18:  loop__1__i <= 128
%%%  Hypotheses H7 & H25 together imply that
          loop__1__i < lengthofdomainname__entry__loop__1 - 1.
     H7 & H25 have therefore been deleted and a new H26 added to this effect.
***  Proved C7:  loop__1__i + 1 <= lengthofdomainname__entry__loop__1 - 1
     via its standard form, which is:
     Std.Fm C7:  lengthofdomainname__entry__loop__1 - loop__1__i > 1
     using hypothesis H26.
***  Proved C5:  loop__1__i <= 2147483646
     using hypothesis H16.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_6.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H11).
%%%  Simplified C3 on reading formula in, to give:
     %%%  C3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
***  Proved C1:  lengthofdomainname >= 1
     using hypothesis H1.
***  Proved C2:  lengthofdomainname <= maxdomainnamelength
     using hypothesis H2.
***  Proved C3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
     using hypothesis H3.
***  Proved C4:  loop__1__i + 1 >= integer__first
     using hypothesis H4.
***  Proved C6:  loop__1__i + 1 >= domainnamestringtypeindex__first
     using hypothesis H6.
***  Proved C8:  lengthofdomainname__entry__loop__1 >= 
          domainnamestringtypeindex__first
     using hypothesis H8.
***  Proved C9:  lengthofdomainname__entry__loop__1 <= 
          domainnamestringtypeindex__last
     using hypothesis H9.
-S-  Applied substitution rule convertdomai_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H5:  loop__1__i <= 2147483647
<S>  New C5:  loop__1__i <= 2147483646
>>>  Restructured hypothesis H12 into:
     >>>  H12:  element(domainnameversion, [loop__1__i]) <> 46
>>>  Restructured hypothesis H21 into:
     >>>  H21:  loop__1__i <> lengthofdomainname__entry__loop__1 - 1
-S-  Applied substitution rule convertdomai_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H2:  lengthofdomainname <= 128
-S-  Applied substitution rule convertdomai_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H4:  loop__1__i >= - 2147483648
-S-  Applied substitution rule convertdomai_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H19:  loop__1__i >= - 2147483649
-S-  Applied substitution rule convertdomai_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H20:  loop__1__i <= 2147483646
-S-  Applied substitution rule convertdomai_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= character__last)
<S>  New H13:  element(domainnameversion, [loop__1__i]) >= 0
-S-  Applied substitution rule convertdomai_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H14:  element(domainnameversion, [loop__1__i]) <= 255
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= 255)
-S-  Applied substitution rule convertdomai_rules(25).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H6:  loop__1__i >= 1
<S>  New H8:  lengthofdomainname__entry__loop__1 >= 1
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(domainnameversion, [
          i___1]) and element(domainnameversion, [i___1]) <= 255)
-S-  Applied substitution rule convertdomai_rules(26).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H9:  lengthofdomainname__entry__loop__1 <= 128
<S>  New H11:  loop__1__i <= 128
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(domainnameversion, [i___1]) and element(domainnameversion, [
          i___1]) <= 255)
-S-  Applied substitution rule convertdomai_rules(30).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__first by:
          1.
<S>  New H17:  loop__1__i >= 0
-S-  Applied substitution rule convertdomai_rules(31).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__last by:
          129.
<S>  New H18:  loop__1__i <= 128
%%%  Hypotheses H7 & H21 together imply that
          loop__1__i < lengthofdomainname__entry__loop__1 - 1.
     H7 & H21 have therefore been deleted and a new H22 added to this effect.
***  Proved C7:  loop__1__i + 1 <= lengthofdomainname__entry__loop__1 - 1
     via its standard form, which is:
     Std.Fm C7:  lengthofdomainname__entry__loop__1 - loop__1__i > 1
     using hypothesis H22.
***  Proved C5:  loop__1__i <= 2147483646
     using hypothesis H20.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_7.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
***  Proved C1:  loop__1__i >= domainnamestringtypeindex__first
     using hypothesis H6.
***  Proved C2:  loop__1__i <= domainnamestringtypeindex__last
     using hypotheses H7 & H9.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_8.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H6)
          .
-S-  Applied substitution rule convertdomai_rules(20).
     This was achieved by replacing all occurrences of linelengthindex__first 
          by:
          1.
<S>  New C1:  loop__1__i >= 0
-S-  Applied substitution rule convertdomai_rules(21).
     This was achieved by replacing all occurrences of linelengthindex__last by:
          256.
<S>  New C2:  loop__1__i <= 255
-S-  Applied substitution rule convertdomai_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C3:  loop__1__i >= - 2147483649
<S>  New C7:  loop__1__i >= - 2147483649
-S-  Applied substitution rule convertdomai_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C4:  loop__1__i <= 2147483646
<S>  New C8:  loop__1__i <= 2147483646
-S-  Applied substitution rule convertdomai_rules(30).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__first by:
          1.
<S>  New C5:  loop__1__i >= 0
-S-  Applied substitution rule convertdomai_rules(31).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__last by:
          129.
<S>  New C6:  loop__1__i <= 128
-S-  Applied substitution rule convertdomai_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H2:  lengthofdomainname <= 128
-S-  Applied substitution rule convertdomai_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H4:  loop__1__i >= - 2147483648
-S-  Applied substitution rule convertdomai_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H5:  loop__1__i <= 2147483647
-S-  Applied substitution rule convertdomai_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= character__last)
-S-  Applied substitution rule convertdomai_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= 255)
-S-  Applied substitution rule convertdomai_rules(25).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H6:  loop__1__i >= 1
<S>  New H8:  lengthofdomainname__entry__loop__1 >= 1
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(domainnameversion, [
          i___1]) and element(domainnameversion, [i___1]) <= 255)
-S-  Applied substitution rule convertdomai_rules(26).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H9:  lengthofdomainname__entry__loop__1 <= 128
<S>  New H11:  loop__1__i <= 128
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(domainnameversion, [i___1]) and element(domainnameversion, [
          i___1]) <= 255)
***  Proved C1:  loop__1__i >= 0
     using hypothesis H6.
***  Proved C2:  loop__1__i <= 255
     using hypothesis H11.
***  Proved C3:  loop__1__i >= - 2147483649
     using hypothesis H4.
***  Proved C7:  loop__1__i >= - 2147483649
     using hypothesis H4.
***  Proved C4:  loop__1__i <= 2147483646
     using hypothesis H11.
***  Proved C8:  loop__1__i <= 2147483646
     using hypothesis H11.
***  Proved C5:  loop__1__i >= 0
     using hypothesis H6.
***  Proved C6:  loop__1__i <= 128
     using hypothesis H11.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_9.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H16).
***  Proved C1:  findperiod(domainnameversion, loop__1__i + 1) >= 
          character__first
     using hypothesis H21.
***  Proved C2:  findperiod(domainnameversion, loop__1__i + 1) <= 
          character__last
     using hypothesis H22.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_10.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H6)
          .
***  Proved C1:  element(domainnameversion, [loop__1__i]) >= character__first
     using hypotheses H3, H6 & H11.
***  Proved C2:  element(domainnameversion, [loop__1__i]) <= character__last
     using hypotheses H3, H6 & H11.
***  Proved C3:  loop__1__i >= domainnamestringtypeindex__first
     using hypothesis H6.
***  Proved C4:  loop__1__i <= domainnamestringtypeindex__last
     using hypothesis H11.
-S-  Applied substitution rule convertdomai_rules(30).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__first by:
          1.
<S>  New C5:  loop__1__i >= 0
-S-  Applied substitution rule convertdomai_rules(31).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__last by:
          129.
<S>  New C6:  loop__1__i <= 128
-S-  Applied substitution rule convertdomai_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C7:  loop__1__i >= - 2147483649
-S-  Applied substitution rule convertdomai_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C8:  loop__1__i <= 2147483646
>>>  Restructured hypothesis H12 into:
     >>>  H12:  element(domainnameversion, [loop__1__i]) <> 46
-S-  Applied substitution rule convertdomai_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H2:  lengthofdomainname <= 128
-S-  Applied substitution rule convertdomai_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H4:  loop__1__i >= - 2147483648
-S-  Applied substitution rule convertdomai_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H5:  loop__1__i <= 2147483647
-S-  Applied substitution rule convertdomai_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= character__last)
-S-  Applied substitution rule convertdomai_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= 255)
-S-  Applied substitution rule convertdomai_rules(25).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H6:  loop__1__i >= 1
<S>  New H8:  lengthofdomainname__entry__loop__1 >= 1
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(domainnameversion, [
          i___1]) and element(domainnameversion, [i___1]) <= 255)
-S-  Applied substitution rule convertdomai_rules(26).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H9:  lengthofdomainname__entry__loop__1 <= 128
<S>  New H11:  loop__1__i <= 128
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(domainnameversion, [i___1]) and element(domainnameversion, [
          i___1]) <= 255)
***  Proved C5:  loop__1__i >= 0
     using hypothesis H6.
***  Proved C6:  loop__1__i <= 128
     using hypothesis H11.
***  Proved C7:  loop__1__i >= - 2147483649
     using hypothesis H4.
***  Proved C8:  loop__1__i <= 2147483646
     using hypothesis H11.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_11.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  domainnamelength(domainnameversion) = 1 and (element(
          domainnameversion, [1]) = 32 or element(domainnameversion, [2]) = 32) 
          or (domainnamelength(domainnameversion) = maxdomainnamelength or 
          element(domainnameversion, [domainnamelength(domainnameversion) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          domainnameversion) -> element(domainnameversion, [q_]) <> 32))
---  Hypothesis H5 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H3)
          .
-S-  Applied substitution rule convertdomai_rules(25).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> character__first <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= character__last)
<S>  New H2:  domainnamelength(domainnameversion) >= 1
<S>  New H13:  1 >= integer__first
<S>  New H14:  1 <= integer__last
<S>  New H15:  2 <= domainnamelength(domainnameversion) -> domainnamelength(
          domainnameversion) - 1 >= integer__first and domainnamelength(
          domainnameversion) - 1 <= integer__last
<S>  New H16:  2 <= domainnamelength(domainnameversion) -> 1 >= integer__first 
          and 1 <= integer__last
<S>  New H19:  not 2 <= domainnamelength(domainnameversion)
<S>  New C1:  1 >= linelengthindex__first
<S>  New C2:  1 <= linelengthindex__last
<S>  New C3:  1 >= wirestringtypeindex__first
<S>  New C4:  1 <= wirestringtypeindex__last
-S-  Applied substitution rule convertdomai_rules(20).
     This was achieved by replacing all occurrences of linelengthindex__first 
          by:
          1.
<S>  New C1:  true
-S-  Applied substitution rule convertdomai_rules(21).
     This was achieved by replacing all occurrences of linelengthindex__last by:
          256.
<S>  New C2:  true
-S-  Applied substitution rule convertdomai_rules(30).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__first by:
          1.
<S>  New C3:  true
-S-  Applied substitution rule convertdomai_rules(31).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__last by:
          129.
<S>  New C4:  true
***  Proved C1:  true
***  Proved C2:  true
***  Proved C3:  true
***  Proved C4:  true
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_12.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H22).
***  Proved C2:  domainnamestringtypeindex__first <= linelengthindex__last
     using hypotheses H6 & H14.
***  Proved C4:  domainnamestringtypeindex__first <= wirestringtypeindex__last
     using hypotheses H6 & H18.
-S-  Applied substitution rule convertdomai_rules(25).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> character__first <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= character__last)
<S>  New H6:  loop__1__i >= 1
<S>  New H8:  lengthofdomainname__entry__loop__1 >= 1
<S>  New C1:  1 >= linelengthindex__first
<S>  New C3:  1 >= wirestringtypeindex__first
-S-  Applied substitution rule convertdomai_rules(20).
     This was achieved by replacing all occurrences of linelengthindex__first 
          by:
          1.
<S>  New H13:  loop__1__i >= 0
<S>  New C1:  true
-S-  Applied substitution rule convertdomai_rules(30).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__first by:
          1.
<S>  New H17:  loop__1__i >= 0
<S>  New C3:  true
***  Proved C1:  true
***  Proved C3:  true
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_13.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H11).
***  Proved C4:  domainnamestringtypeindex__first <= wirestringtypeindex__last
     using hypotheses H6 & H18.
-S-  Applied substitution rule convertdomai_rules(25).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> character__first <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= character__last)
<S>  New H6:  loop__1__i >= 1
<S>  New H8:  lengthofdomainname__entry__loop__1 >= 1
<S>  New C1:  1 >= linelengthindex__first
<S>  New C2:  1 <= linelengthindex__last
<S>  New C3:  1 >= wirestringtypeindex__first
-S-  Applied substitution rule convertdomai_rules(20).
     This was achieved by replacing all occurrences of linelengthindex__first 
          by:
          1.
<S>  New C1:  true
-S-  Applied substitution rule convertdomai_rules(21).
     This was achieved by replacing all occurrences of linelengthindex__last by:
          256.
<S>  New C2:  true
-S-  Applied substitution rule convertdomai_rules(30).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__first by:
          1.
<S>  New H17:  loop__1__i >= 0
<S>  New C3:  true
***  Proved C1:  true
***  Proved C2:  true
***  Proved C3:  true
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_14.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  domainnamelength(domainnameversion) = 1 and (element(
          domainnameversion, [1]) = 32 or element(domainnameversion, [2]) = 32) 
          or (domainnamelength(domainnameversion) = maxdomainnamelength or 
          element(domainnameversion, [domainnamelength(domainnameversion) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          domainnameversion) -> element(domainnameversion, [q_]) <> 32))
---  Hypothesis H5 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H3)
          .
***  Proved C1:  findperiod(domainnameversion, domainnamestringtypeindex__first)
           >= character__first
     using hypothesis H24.
***  Proved C2:  findperiod(domainnameversion, domainnamestringtypeindex__first)
           <= character__last
     using hypothesis H25.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_15.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H22).
***  Proved C1:  findperiod(domainnameversion, domainnamestringtypeindex__first)
           >= character__first
     using hypothesis H30.
***  Proved C2:  findperiod(domainnameversion, domainnamestringtypeindex__first)
           <= character__last
     using hypothesis H31.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_16.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H11).
***  Proved C1:  findperiod(domainnameversion, domainnamestringtypeindex__first)
           >= character__first
     using hypothesis H26.
***  Proved C2:  findperiod(domainnameversion, domainnamestringtypeindex__first)
           <= character__last
     using hypothesis H27.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_17.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  domainnamelength(domainnameversion) = 1 and (element(
          domainnameversion, [1]) = 32 or element(domainnameversion, [2]) = 32) 
          or (domainnamelength(domainnameversion) = maxdomainnamelength or 
          element(domainnameversion, [domainnamelength(domainnameversion) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          domainnameversion) -> element(domainnameversion, [q_]) <> 32))
---  Hypothesis H5 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H25).
***  Proved C5:  domainnamelength(domainnameversion) + 1 >= 
          wirestringtypeindex__first
     using hypotheses H2 & H22.
***  Proved C7:  domainnamelength(domainnameversion) + 1 >= integer__base__first
     using hypothesis H11.
-S-  Applied substitution rule convertdomai_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= character__last)
<S>  New H24:  findperiod(domainnameversion, domainnamestringtypeindex__first) 
          >= 0
<S>  New C1:  true
<S>  New C3:  true
-S-  Applied substitution rule convertdomai_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H25:  findperiod(domainnameversion, domainnamestringtypeindex__first) 
          <= 255
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= 255)
<S>  New C2:  true
<S>  New C4:  true
-S-  Applied substitution rule convertdomai_rules(31).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__last by:
          129.
<S>  New H23:  domainnamestringtypeindex__first <= 129
<S>  New C6:  domainnamelength(domainnameversion) <= 128
-S-  Applied substitution rule convertdomai_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H12:  domainnamelength(domainnameversion) <= 2147483648
<S>  New C8:  domainnamelength(domainnameversion) <= 2147483646
***  Proved C1:  true
***  Proved C3:  true
***  Proved C2:  true
***  Proved C4:  true
>>>  Restructured hypothesis H19 into:
     >>>  H19:  domainnamelength(domainnameversion) - 1 < 
          domainnamestringtypeindex__first
-S-  Applied substitution rule convertdomai_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H4:  domainnamelength(domainnameversion) = 1 and (element(
          domainnameversion, [1]) = 32 or element(domainnameversion, [2]) = 32) 
          or (domainnamelength(domainnameversion) = 128 or element(
          domainnameversion, [domainnamelength(domainnameversion) + 1]) = 32 
          and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          domainnameversion) -> element(domainnameversion, [q_]) <> 32))
-S-  Applied substitution rule convertdomai_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H9:  domainnamelength(domainnameversion) >= - 2147483647
<S>  New H13:  domainnamestringtypeindex__first >= - 2147483648
<S>  New H15:  domainnamestringtypeindex__first <= domainnamelength(
          domainnameversion) - 1 -> domainnamelength(domainnameversion) >= - 
          2147483647 and domainnamelength(domainnameversion) - 1 <= 
          integer__last
<S>  New H16:  domainnamestringtypeindex__first <= domainnamelength(
          domainnameversion) - 1 -> domainnamestringtypeindex__first >= - 
          2147483648 and domainnamestringtypeindex__first <= integer__last
-S-  Applied substitution rule convertdomai_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H10:  domainnamelength(domainnameversion) <= 2147483648
<S>  New H14:  domainnamestringtypeindex__first <= 2147483647
<S>  New H15:  domainnamestringtypeindex__first <= domainnamelength(
          domainnameversion) - 1 -> domainnamelength(domainnameversion) >= - 
          2147483647 and domainnamelength(domainnameversion) <= 2147483648
<S>  New H16:  domainnamestringtypeindex__first <= domainnamelength(
          domainnameversion) - 1 -> domainnamestringtypeindex__first >= - 
          2147483648 and domainnamestringtypeindex__first <= 2147483647
-S-  Applied substitution rule convertdomai_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H11:  domainnamelength(domainnameversion) >= - 2147483647
-S-  Applied substitution rule convertdomai_rules(20).
     This was achieved by replacing all occurrences of linelengthindex__first 
          by:
          1.
<S>  New H20:  domainnamestringtypeindex__first >= 1
-S-  Applied substitution rule convertdomai_rules(21).
     This was achieved by replacing all occurrences of linelengthindex__last by:
          256.
<S>  New H21:  domainnamestringtypeindex__first <= 256
-S-  Applied substitution rule convertdomai_rules(25).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(domainnameversion, [
          i___1]) and element(domainnameversion, [i___1]) <= 255)
<S>  New H2:  domainnamelength(domainnameversion) >= 1
<S>  New H19:  domainnamelength(domainnameversion) < 2
<S>  New H22:  1 >= wirestringtypeindex__first
<S>  New H23:  true
<S>  New H24:  findperiod(domainnameversion, 1) >= 0
<S>  New H25:  findperiod(domainnameversion, 1) <= 255
<S>  New H13:  true
<S>  New H14:  true
<S>  New H15:  2 <= domainnamelength(domainnameversion) -> domainnamelength(
          domainnameversion) >= - 2147483647 and domainnamelength(
          domainnameversion) <= 2147483648
<S>  New H16:  true
<S>  New H20:  true
<S>  New H21:  true
-S-  Applied substitution rule convertdomai_rules(26).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H3:  domainnamelength(domainnameversion) <= 128
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(domainnameversion, [i___1]) and element(domainnameversion, [
          i___1]) <= 255)
-S-  Applied substitution rule convertdomai_rules(30).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__first by:
          1.
<S>  New H22:  true
***  Proved C6:  domainnamelength(domainnameversion) <= 128
     using hypothesis H3.
***  Proved C8:  domainnamelength(domainnameversion) <= 2147483646
     using hypothesis H19.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_18.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis 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).
-S-  Applied substitution rule convertdomai_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= character__last)
<S>  New H21:  findperiod(domainnameversion, loop__1__i + 1) >= 0
<S>  New H30:  findperiod(domainnameversion, domainnamestringtypeindex__first) 
          >= 0
<S>  New C1:  true
<S>  New C3:  true
-S-  Applied substitution rule convertdomai_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H22:  findperiod(domainnameversion, loop__1__i + 1) <= 255
<S>  New H31:  findperiod(domainnameversion, domainnamestringtypeindex__first) 
          <= 255
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= 255)
<S>  New C2:  true
<S>  New C4:  true
-S-  Applied substitution rule convertdomai_rules(30).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__first by:
          1.
<S>  New H17:  loop__1__i >= 0
<S>  New H28:  domainnamestringtypeindex__first >= 1
<S>  New C5:  lengthofdomainname >= 0
-S-  Applied substitution rule convertdomai_rules(31).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__last by:
          129.
<S>  New H18:  loop__1__i <= 128
<S>  New H29:  domainnamestringtypeindex__first <= 129
<S>  New C6:  lengthofdomainname <= 128
-S-  Applied substitution rule convertdomai_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H15:  loop__1__i >= - 2147483649
<S>  New C7:  lengthofdomainname >= - 2147483649
-S-  Applied substitution rule convertdomai_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H16:  loop__1__i <= 2147483646
<S>  New C8:  lengthofdomainname <= 2147483646
***  Proved C1:  true
***  Proved C3:  true
***  Proved C2:  true
***  Proved C4:  true
***  Proved C5:  lengthofdomainname >= 0
     using hypothesis H1.
***  Proved C7:  lengthofdomainname >= - 2147483649
     using hypothesis H1.
-S-  Applied substitution rule convertdomai_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H2:  lengthofdomainname <= 128
-S-  Applied substitution rule convertdomai_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H4:  loop__1__i >= - 2147483648
-S-  Applied substitution rule convertdomai_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H5:  loop__1__i <= 2147483647
-S-  Applied substitution rule convertdomai_rules(20).
     This was achieved by replacing all occurrences of linelengthindex__first 
          by:
          1.
<S>  New H13:  loop__1__i >= 0
<S>  New H26:  domainnamestringtypeindex__first >= 1
-S-  Applied substitution rule convertdomai_rules(21).
     This was achieved by replacing all occurrences of linelengthindex__last by:
          256.
<S>  New H14:  loop__1__i <= 255
<S>  New H27:  domainnamestringtypeindex__first <= 256
-S-  Applied substitution rule convertdomai_rules(25).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(domainnameversion, [
          i___1]) and element(domainnameversion, [i___1]) <= 255)
<S>  New H6:  loop__1__i >= 1
<S>  New H8:  lengthofdomainname__entry__loop__1 >= 1
<S>  New H28:  true
<S>  New H29:  true
<S>  New H30:  findperiod(domainnameversion, 1) >= 0
<S>  New H31:  findperiod(domainnameversion, 1) <= 255
<S>  New H26:  true
<S>  New H27:  true
-S-  Applied substitution rule convertdomai_rules(26).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H9:  lengthofdomainname__entry__loop__1 <= 128
<S>  New H11:  loop__1__i <= 128
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(domainnameversion, [i___1]) and element(domainnameversion, [
          i___1]) <= 255)
***  Proved C6:  lengthofdomainname <= 128
     using hypothesis H2.
***  Proved C8:  lengthofdomainname <= 2147483646
     using hypothesis H2.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_19.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H11).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H27).
-S-  Applied substitution rule convertdomai_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= character__last)
<S>  New H13:  element(domainnameversion, [loop__1__i]) >= 0
<S>  New H26:  findperiod(domainnameversion, domainnamestringtypeindex__first) 
          >= 0
<S>  New C1:  true
<S>  New C3:  true
-S-  Applied substitution rule convertdomai_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H14:  element(domainnameversion, [loop__1__i]) <= 255
<S>  New H27:  findperiod(domainnameversion, domainnamestringtypeindex__first) 
          <= 255
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= 255)
<S>  New C2:  true
<S>  New C4:  true
-S-  Applied substitution rule convertdomai_rules(30).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__first by:
          1.
<S>  New H17:  loop__1__i >= 0
<S>  New H24:  domainnamestringtypeindex__first >= 1
<S>  New C5:  lengthofdomainname >= 0
-S-  Applied substitution rule convertdomai_rules(31).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__last by:
          129.
<S>  New H18:  loop__1__i <= 128
<S>  New H25:  domainnamestringtypeindex__first <= 129
<S>  New C6:  lengthofdomainname <= 128
-S-  Applied substitution rule convertdomai_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H19:  loop__1__i >= - 2147483649
<S>  New C7:  lengthofdomainname >= - 2147483649
-S-  Applied substitution rule convertdomai_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H20:  loop__1__i <= 2147483646
<S>  New C8:  lengthofdomainname <= 2147483646
***  Proved C1:  true
***  Proved C3:  true
***  Proved C2:  true
***  Proved C4:  true
***  Proved C5:  lengthofdomainname >= 0
     using hypothesis H1.
***  Proved C7:  lengthofdomainname >= - 2147483649
     using hypothesis H1.
>>>  Restructured hypothesis H12 into:
     >>>  H12:  element(domainnameversion, [loop__1__i]) <> 46
-S-  Applied substitution rule convertdomai_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H2:  lengthofdomainname <= 128
-S-  Applied substitution rule convertdomai_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H4:  loop__1__i >= - 2147483648
-S-  Applied substitution rule convertdomai_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H5:  loop__1__i <= 2147483647
-S-  Applied substitution rule convertdomai_rules(20).
     This was achieved by replacing all occurrences of linelengthindex__first 
          by:
          1.
<S>  New H22:  domainnamestringtypeindex__first >= 1
-S-  Applied substitution rule convertdomai_rules(21).
     This was achieved by replacing all occurrences of linelengthindex__last by:
          256.
<S>  New H23:  domainnamestringtypeindex__first <= 256
-S-  Applied substitution rule convertdomai_rules(25).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(domainnameversion, [
          i___1]) and element(domainnameversion, [i___1]) <= 255)
<S>  New H6:  loop__1__i >= 1
<S>  New H8:  lengthofdomainname__entry__loop__1 >= 1
<S>  New H24:  true
<S>  New H25:  true
<S>  New H26:  findperiod(domainnameversion, 1) >= 0
<S>  New H27:  findperiod(domainnameversion, 1) <= 255
<S>  New H22:  true
<S>  New H23:  true
-S-  Applied substitution rule convertdomai_rules(26).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H9:  lengthofdomainname__entry__loop__1 <= 128
<S>  New H11:  loop__1__i <= 128
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(domainnameversion, [i___1]) and element(domainnameversion, [
          i___1]) <= 255)
***  Proved C6:  lengthofdomainname <= 128
     using hypothesis H2.
***  Proved C8:  lengthofdomainname <= 2147483646
     using hypothesis H2.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_20.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  domainnamelength(domainnameversion) = 1 and (element(
          domainnameversion, [1]) = 32 or element(domainnameversion, [2]) = 32) 
          or (domainnamelength(domainnameversion) = maxdomainnamelength or 
          element(domainnameversion, [domainnamelength(domainnameversion) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          domainnameversion) -> element(domainnameversion, [q_]) <> 32))
---  Hypothesis H5 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H24).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H25).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H28).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H29).
%%%  Simplified H36 on reading formula in, to give:
     %%%  H36:  for_all(i___1 : integer, wirestringtypeindex__first <= i___1 
          and i___1 <= wirestringtypeindex__last -> character__first <= element(
          update(update(blankwire, [domainnamestringtypeindex__first], 
          findperiod(domainnameversion, domainnamestringtypeindex__first)), [
          domainnamelength(domainnameversion) + 1], 0), [i___1]) and element(
          update(update(blankwire, [domainnamestringtypeindex__first], 
          findperiod(domainnameversion, domainnamestringtypeindex__first)), [
          domainnamelength(domainnameversion) + 1], 0), [i___1]) <= 
          character__last)
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  for_all(i_ : integer, domainnamestringtypeindex__first <= i_ and 
          i_ <= domainnamestringtypeindex__last -> 0 <= element(update(update(
          blankwire, [domainnamestringtypeindex__first], findperiod(
          domainnameversion, domainnamestringtypeindex__first)), [
          domainnamelength(domainnameversion) + 1], 0), [i_]) and element(
          update(update(blankwire, [domainnamestringtypeindex__first], 
          findperiod(domainnameversion, domainnamestringtypeindex__first)), [
          domainnamelength(domainnameversion) + 1], 0), [i_]) <= 255)
>>>  Restructured hypothesis H19 into:
     >>>  H19:  domainnamelength(domainnameversion) - 1 < 
          domainnamestringtypeindex__first
-S-  Applied substitution rule convertdomai_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H4:  domainnamelength(domainnameversion) = 1 and (element(
          domainnameversion, [1]) = 32 or element(domainnameversion, [2]) = 32) 
          or (domainnamelength(domainnameversion) = 128 or element(
          domainnameversion, [domainnamelength(domainnameversion) + 1]) = 32 
          and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          domainnameversion) -> element(domainnameversion, [q_]) <> 32))
-S-  Applied substitution rule convertdomai_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H9:  domainnamelength(domainnameversion) >= - 2147483647
<S>  New H13:  domainnamestringtypeindex__first >= - 2147483648
<S>  New H15:  domainnamestringtypeindex__first <= domainnamelength(
          domainnameversion) - 1 -> domainnamelength(domainnameversion) >= - 
          2147483647 and domainnamelength(domainnameversion) - 1 <= 
          integer__last
<S>  New H16:  domainnamestringtypeindex__first <= domainnamelength(
          domainnameversion) - 1 -> domainnamestringtypeindex__first >= - 
          2147483648 and domainnamestringtypeindex__first <= integer__last
-S-  Applied substitution rule convertdomai_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H10:  domainnamelength(domainnameversion) <= 2147483648
<S>  New H14:  domainnamestringtypeindex__first <= 2147483647
<S>  New H15:  domainnamestringtypeindex__first <= domainnamelength(
          domainnameversion) - 1 -> domainnamelength(domainnameversion) >= - 
          2147483647 and domainnamelength(domainnameversion) <= 2147483648
<S>  New H16:  domainnamestringtypeindex__first <= domainnamelength(
          domainnameversion) - 1 -> domainnamestringtypeindex__first >= - 
          2147483648 and domainnamestringtypeindex__first <= 2147483647
-S-  Applied substitution rule convertdomai_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H11:  domainnamelength(domainnameversion) >= - 2147483647
<S>  New H34:  domainnamelength(domainnameversion) >= - 2147483649
-S-  Applied substitution rule convertdomai_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H12:  domainnamelength(domainnameversion) <= 2147483648
<S>  New H35:  domainnamelength(domainnameversion) <= 2147483646
-S-  Applied substitution rule convertdomai_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= character__last)
<S>  New H24:  findperiod(domainnameversion, domainnamestringtypeindex__first) 
          >= 0
<S>  New H28:  true
<S>  New H36:  for_all(i___1 : integer, wirestringtypeindex__first <= i___1 and 
          i___1 <= wirestringtypeindex__last -> 0 <= element(update(update(
          blankwire, [domainnamestringtypeindex__first], findperiod(
          domainnameversion, domainnamestringtypeindex__first)), [
          domainnamelength(domainnameversion) + 1], 0), [i___1]) and element(
          update(update(blankwire, [domainnamestringtypeindex__first], 
          findperiod(domainnameversion, domainnamestringtypeindex__first)), [
          domainnamelength(domainnameversion) + 1], 0), [i___1]) <= 
          character__last)
-S-  Applied substitution rule convertdomai_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H25:  findperiod(domainnameversion, domainnamestringtypeindex__first) 
          <= 255
<S>  New H29:  true
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= 255)
<S>  New H36:  for_all(i___1 : integer, wirestringtypeindex__first <= i___1 and 
          i___1 <= wirestringtypeindex__last -> 0 <= element(update(update(
          blankwire, [domainnamestringtypeindex__first], findperiod(
          domainnameversion, domainnamestringtypeindex__first)), [
          domainnamelength(domainnameversion) + 1], 0), [i___1]) and element(
          update(update(blankwire, [domainnamestringtypeindex__first], 
          findperiod(domainnameversion, domainnamestringtypeindex__first)), [
          domainnamelength(domainnameversion) + 1], 0), [i___1]) <= 255)
-S-  Applied substitution rule convertdomai_rules(20).
     This was achieved by replacing all occurrences of linelengthindex__first 
          by:
          1.
<S>  New H20:  domainnamestringtypeindex__first >= 1
-S-  Applied substitution rule convertdomai_rules(21).
     This was achieved by replacing all occurrences of linelengthindex__last by:
          256.
<S>  New H21:  domainnamestringtypeindex__first <= 256
-S-  Applied substitution rule convertdomai_rules(25).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H2:  domainnamelength(domainnameversion) >= 1
<S>  New H19:  domainnamelength(domainnameversion) < 2
<S>  New H22:  1 >= wirestringtypeindex__first
<S>  New H23:  1 <= wirestringtypeindex__last
<S>  New H13:  true
<S>  New H14:  true
<S>  New H15:  2 <= domainnamelength(domainnameversion) -> domainnamelength(
          domainnameversion) >= - 2147483647 and domainnamelength(
          domainnameversion) <= 2147483648
<S>  New H16:  true
<S>  New H24:  findperiod(domainnameversion, 1) >= 0
<S>  New H25:  findperiod(domainnameversion, 1) <= 255
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(domainnameversion, [
          i___1]) and element(domainnameversion, [i___1]) <= 255)
<S>  New H36:  for_all(i___1 : integer, wirestringtypeindex__first <= i___1 and 
          i___1 <= wirestringtypeindex__last -> 0 <= element(update(update(
          blankwire, [1], findperiod(domainnameversion, 1)), [domainnamelength(
          domainnameversion) + 1], 0), [i___1]) and element(update(update(
          blankwire, [1], findperiod(domainnameversion, 1)), [domainnamelength(
          domainnameversion) + 1], 0), [i___1]) <= 255)
<S>  New H20:  true
<S>  New H21:  true
<S>  New C1:  for_all(i_ : integer, 1 <= i_ and i_ <= 
          domainnamestringtypeindex__last -> 0 <= element(update(update(
          blankwire, [1], findperiod(domainnameversion, 1)), [domainnamelength(
          domainnameversion) + 1], 0), [i_]) and element(update(update(
          blankwire, [1], findperiod(domainnameversion, 1)), [domainnamelength(
          domainnameversion) + 1], 0), [i_]) <= 255)
-S-  Applied substitution rule convertdomai_rules(26).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H3:  domainnamelength(domainnameversion) <= 128
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(domainnameversion, [i___1]) and element(domainnameversion, [
          i___1]) <= 255)
<S>  New C1:  for_all(i_ : integer, 1 <= i_ and i_ <= 128 -> 0 <= element(
          update(update(blankwire, [1], findperiod(domainnameversion, 1)), [
          domainnamelength(domainnameversion) + 1], 0), [i_]) and element(
          update(update(blankwire, [1], findperiod(domainnameversion, 1)), [
          domainnamelength(domainnameversion) + 1], 0), [i_]) <= 255)
-S-  Applied substitution rule convertdomai_rules(30).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__first by:
          1.
<S>  New H32:  domainnamelength(domainnameversion) >= 0
<S>  New H22:  true
<S>  New H36:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          wirestringtypeindex__last -> 0 <= element(update(update(blankwire, [1]
          , findperiod(domainnameversion, 1)), [domainnamelength(
          domainnameversion) + 1], 0), [i___1]) and element(update(update(
          blankwire, [1], findperiod(domainnameversion, 1)), [domainnamelength(
          domainnameversion) + 1], 0), [i___1]) <= 255)
-S-  Applied substitution rule convertdomai_rules(31).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__last by:
          129.
<S>  New H33:  domainnamelength(domainnameversion) <= 128
<S>  New H23:  true
<S>  New H36:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(update(update(blankwire, [1], findperiod(domainnameversion, 1)
          ), [domainnamelength(domainnameversion) + 1], 0), [i___1]) and 
          element(update(update(blankwire, [1], findperiod(domainnameversion, 1)
          ), [domainnamelength(domainnameversion) + 1], 0), [i___1]) <= 255)
---  Eliminated hypothesis H5 (true-hypothesis).
---  Eliminated hypothesis H6 (true-hypothesis).
---  Eliminated hypothesis H7 (true-hypothesis).
---  Eliminated hypothesis H8 (true-hypothesis).
---  Eliminated hypothesis H17 (true-hypothesis).
---  Eliminated hypothesis H18 (true-hypothesis).
---  Eliminated hypothesis H26 (true-hypothesis).
---  Eliminated hypothesis H27 (true-hypothesis).
---  Eliminated hypothesis H30 (true-hypothesis).
---  Eliminated hypothesis H31 (true-hypothesis).
---  Eliminated hypothesis H28 (true-hypothesis).
---  Eliminated hypothesis H29 (true-hypothesis).
---  Eliminated hypothesis H13 (true-hypothesis).
---  Eliminated hypothesis H14 (true-hypothesis).
---  Eliminated hypothesis H16 (true-hypothesis).
---  Eliminated hypothesis H20 (true-hypothesis).
---  Eliminated hypothesis H21 (true-hypothesis).
---  Eliminated hypothesis H22 (true-hypothesis).
---  Eliminated hypothesis H23 (true-hypothesis).
%%%  Simplified H4 further (given H19), to give:
     %%%  H4:  domainnamelength(domainnameversion) = 1 and (element(
          domainnameversion, [1]) = 32 or element(domainnameversion, [2]) = 32) 
          or element(domainnameversion, [domainnamelength(domainnameversion) + 
          1]) = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          domainnameversion) -> element(domainnameversion, [q_]) <> 32)
---  Eliminated hypothesis H11 (duplicate of H9).
---  Eliminated hypothesis H12 (duplicate of H10).
---  Eliminated hypothesis H33 (duplicate of H3).
---  Eliminated hypothesis H3 (redundant, given H19).
---  Eliminated hypothesis H9 (redundant, given H2).
---  Eliminated hypothesis H10 (redundant, given H19).
---  Eliminated hypothesis H32 (redundant, given H2).
---  Eliminated hypothesis H34 (redundant, given H2).
---  Eliminated hypothesis H35 (redundant, given H19).
     +++  New H37:  integer__size >= 0
     +++  New H38:  character__size >= 0
     +++  New H39:  positive__size >= 0
     +++  New H40:  linelengthindex__size >= 0
     +++  New H41:  domainnamestringtypeindex__size >= 0
     +++  New H42:  wirestringtypeindex__size >= 0
>>>  Attempting to prove quantified formula C1 by "unwrapping" it.
+++  Added new hypotheses (in proving an implication formula).
     +++  New H43:  1 <= int_i__1
     +++  New H44:  int_i__1 <= 128
+++  New subgoal C1:  0 <= element(update(update(blankwire, [1], findperiod(
          domainnameversion, 1)), [domainnamelength(domainnameversion) + 1], 0)
          , [int_i__1]) and element(update(update(blankwire, [1], findperiod(
          domainnameversion, 1)), [domainnamelength(domainnameversion) + 1], 0)
          , [int_i__1]) <= 255
>>>  Conclusion C1 has now been split into two, giving:
     >>>  C1:  0 <= element(update(update(blankwire, [1], findperiod(
          domainnameversion, 1)), [domainnamelength(domainnameversion) + 1], 0)
          , [int_i__1])
     >>>  C2:  element(update(update(blankwire, [1], findperiod(
          domainnameversion, 1)), [domainnamelength(domainnameversion) + 1], 0)
          , [int_i__1]) <= 255
***  Proved subgoal C1
     using hypotheses H36, H43 & H44.
***  Proved subgoal C2
     using hypotheses H36, H43 & H44.
***  Proved C1:  for_all(i_ : integer, 1 <= i_ and i_ <= 128 -> 0 <= element(
          update(update(blankwire, [1], findperiod(domainnameversion, 1)), [
          domainnamelength(domainnameversion) + 1], 0), [i_]) and element(
          update(update(blankwire, [1], findperiod(domainnameversion, 1)), [
          domainnamelength(domainnameversion) + 1], 0), [i_]) <= 255)
     by unwrapping a universally-quantified formula.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_21.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H20 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis 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 H36 has been replaced by "true".  (It is already present, as 
          H34).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H35).
%%%  Simplified H42 on reading formula in, to give:
     %%%  H42:  for_all(i___1 : integer, wirestringtypeindex__first <= i___1 
          and i___1 <= wirestringtypeindex__last -> character__first <= element(
          update(update(update(wireversion, [loop__1__i + 1], findperiod(
          domainnameversion, loop__1__i + 1)), [
          domainnamestringtypeindex__first], findperiod(domainnameversion, 
          domainnamestringtypeindex__first)), [lengthofdomainname + 1], 0), [
          i___1]) and element(update(update(update(wireversion, [loop__1__i + 1]
          , findperiod(domainnameversion, loop__1__i + 1)), [
          domainnamestringtypeindex__first], findperiod(domainnameversion, 
          domainnamestringtypeindex__first)), [lengthofdomainname + 1], 0), [
          i___1]) <= character__last)
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  for_all(i_ : integer, domainnamestringtypeindex__first <= i_ and 
          i_ <= domainnamestringtypeindex__last -> 0 <= element(update(update(
          update(wireversion, [loop__1__i + 1], findperiod(domainnameversion, 
          loop__1__i + 1)), [domainnamestringtypeindex__first], findperiod(
          domainnameversion, domainnamestringtypeindex__first)), [
          lengthofdomainname + 1], 0), [i_]) and element(update(update(update(
          wireversion, [loop__1__i + 1], findperiod(domainnameversion, 
          loop__1__i + 1)), [domainnamestringtypeindex__first], findperiod(
          domainnameversion, domainnamestringtypeindex__first)), [
          lengthofdomainname + 1], 0), [i_]) <= 255)
-S-  Applied substitution rule convertdomai_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H2:  lengthofdomainname <= 128
-S-  Applied substitution rule convertdomai_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H4:  loop__1__i >= - 2147483648
-S-  Applied substitution rule convertdomai_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H5:  loop__1__i <= 2147483647
-S-  Applied substitution rule convertdomai_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H15:  loop__1__i >= - 2147483649
<S>  New H40:  lengthofdomainname >= - 2147483649
-S-  Applied substitution rule convertdomai_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H16:  loop__1__i <= 2147483646
<S>  New H41:  lengthofdomainname <= 2147483646
-S-  Applied substitution rule convertdomai_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= character__last)
<S>  New H21:  findperiod(domainnameversion, loop__1__i + 1) >= 0
<S>  New H30:  findperiod(domainnameversion, domainnamestringtypeindex__first) 
          >= 0
<S>  New H34:  true
<S>  New H42:  for_all(i___1 : integer, wirestringtypeindex__first <= i___1 and 
          i___1 <= wirestringtypeindex__last -> 0 <= element(update(update(
          update(wireversion, [loop__1__i + 1], findperiod(domainnameversion, 
          loop__1__i + 1)), [domainnamestringtypeindex__first], findperiod(
          domainnameversion, domainnamestringtypeindex__first)), [
          lengthofdomainname + 1], 0), [i___1]) and element(update(update(
          update(wireversion, [loop__1__i + 1], findperiod(domainnameversion, 
          loop__1__i + 1)), [domainnamestringtypeindex__first], findperiod(
          domainnameversion, domainnamestringtypeindex__first)), [
          lengthofdomainname + 1], 0), [i___1]) <= character__last)
-S-  Applied substitution rule convertdomai_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H22:  findperiod(domainnameversion, loop__1__i + 1) <= 255
<S>  New H31:  findperiod(domainnameversion, domainnamestringtypeindex__first) 
          <= 255
<S>  New H35:  true
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= 255)
<S>  New H42:  for_all(i___1 : integer, wirestringtypeindex__first <= i___1 and 
          i___1 <= wirestringtypeindex__last -> 0 <= element(update(update(
          update(wireversion, [loop__1__i + 1], findperiod(domainnameversion, 
          loop__1__i + 1)), [domainnamestringtypeindex__first], findperiod(
          domainnameversion, domainnamestringtypeindex__first)), [
          lengthofdomainname + 1], 0), [i___1]) and element(update(update(
          update(wireversion, [loop__1__i + 1], findperiod(domainnameversion, 
          loop__1__i + 1)), [domainnamestringtypeindex__first], findperiod(
          domainnameversion, domainnamestringtypeindex__first)), [
          lengthofdomainname + 1], 0), [i___1]) <= 255)
-S-  Applied substitution rule convertdomai_rules(20).
     This was achieved by replacing all occurrences of linelengthindex__first 
          by:
          1.
<S>  New H13:  loop__1__i >= 0
<S>  New H26:  domainnamestringtypeindex__first >= 1
-S-  Applied substitution rule convertdomai_rules(21).
     This was achieved by replacing all occurrences of linelengthindex__last by:
          256.
<S>  New H14:  loop__1__i <= 255
<S>  New H27:  domainnamestringtypeindex__first <= 256
-S-  Applied substitution rule convertdomai_rules(25).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H6:  loop__1__i >= 1
<S>  New H8:  lengthofdomainname__entry__loop__1 >= 1
<S>  New H28:  1 >= wirestringtypeindex__first
<S>  New H29:  1 <= wirestringtypeindex__last
<S>  New H30:  findperiod(domainnameversion, 1) >= 0
<S>  New H31:  findperiod(domainnameversion, 1) <= 255
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(domainnameversion, [
          i___1]) and element(domainnameversion, [i___1]) <= 255)
<S>  New H42:  for_all(i___1 : integer, wirestringtypeindex__first <= i___1 and 
          i___1 <= wirestringtypeindex__last -> 0 <= element(update(update(
          update(wireversion, [loop__1__i + 1], findperiod(domainnameversion, 
          loop__1__i + 1)), [1], findperiod(domainnameversion, 1)), [
          lengthofdomainname + 1], 0), [i___1]) and element(update(update(
          update(wireversion, [loop__1__i + 1], findperiod(domainnameversion, 
          loop__1__i + 1)), [1], findperiod(domainnameversion, 1)), [
          lengthofdomainname + 1], 0), [i___1]) <= 255)
<S>  New H26:  true
<S>  New H27:  true
<S>  New C1:  for_all(i_ : integer, 1 <= i_ and i_ <= 
          domainnamestringtypeindex__last -> 0 <= element(update(update(update(
          wireversion, [loop__1__i + 1], findperiod(domainnameversion, 
          loop__1__i + 1)), [1], findperiod(domainnameversion, 1)), [
          lengthofdomainname + 1], 0), [i_]) and element(update(update(update(
          wireversion, [loop__1__i + 1], findperiod(domainnameversion, 
          loop__1__i + 1)), [1], findperiod(domainnameversion, 1)), [
          lengthofdomainname + 1], 0), [i_]) <= 255)
-S-  Applied substitution rule convertdomai_rules(26).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H9:  lengthofdomainname__entry__loop__1 <= 128
<S>  New H11:  loop__1__i <= 128
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(domainnameversion, [i___1]) and element(domainnameversion, [
          i___1]) <= 255)
<S>  New C1:  for_all(i_ : integer, 1 <= i_ and i_ <= 128 -> 0 <= element(
          update(update(update(wireversion, [loop__1__i + 1], findperiod(
          domainnameversion, loop__1__i + 1)), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [i_]) and 
          element(update(update(update(wireversion, [loop__1__i + 1], 
          findperiod(domainnameversion, loop__1__i + 1)), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [i_]) <= 255)
-S-  Applied substitution rule convertdomai_rules(30).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__first by:
          1.
<S>  New H17:  loop__1__i >= 0
<S>  New H38:  lengthofdomainname >= 0
<S>  New H28:  true
<S>  New H42:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          wirestringtypeindex__last -> 0 <= element(update(update(update(
          wireversion, [loop__1__i + 1], findperiod(domainnameversion, 
          loop__1__i + 1)), [1], findperiod(domainnameversion, 1)), [
          lengthofdomainname + 1], 0), [i___1]) and element(update(update(
          update(wireversion, [loop__1__i + 1], findperiod(domainnameversion, 
          loop__1__i + 1)), [1], findperiod(domainnameversion, 1)), [
          lengthofdomainname + 1], 0), [i___1]) <= 255)
-S-  Applied substitution rule convertdomai_rules(31).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__last by:
          129.
<S>  New H18:  loop__1__i <= 128
<S>  New H39:  lengthofdomainname <= 128
<S>  New H29:  true
<S>  New H42:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(update(update(update(wireversion, [loop__1__i + 1], 
          findperiod(domainnameversion, loop__1__i + 1)), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [i___1]) and 
          element(update(update(update(wireversion, [loop__1__i + 1], 
          findperiod(domainnameversion, loop__1__i + 1)), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [i___1]) <= 255)
---  Eliminated hypothesis H10 (true-hypothesis).
---  Eliminated hypothesis H19 (true-hypothesis).
---  Eliminated hypothesis H20 (true-hypothesis).
---  Eliminated hypothesis H23 (true-hypothesis).
---  Eliminated hypothesis H24 (true-hypothesis).
---  Eliminated hypothesis H32 (true-hypothesis).
---  Eliminated hypothesis H33 (true-hypothesis).
---  Eliminated hypothesis H36 (true-hypothesis).
---  Eliminated hypothesis H37 (true-hypothesis).
---  Eliminated hypothesis H34 (true-hypothesis).
---  Eliminated hypothesis H35 (true-hypothesis).
---  Eliminated hypothesis H26 (true-hypothesis).
---  Eliminated hypothesis H27 (true-hypothesis).
---  Eliminated hypothesis H28 (true-hypothesis).
---  Eliminated hypothesis H29 (true-hypothesis).
---  Eliminated hypothesis H39 (duplicate of H2).
---  Eliminated hypothesis H17 (duplicate of H13).
---  Eliminated hypothesis H18 (duplicate of H11).
---  Eliminated hypothesis H4 (redundant, given H6).
---  Eliminated hypothesis H5 (redundant, given H11).
---  Eliminated hypothesis H7 (redundant, given H25).
---  Eliminated hypothesis H13 (redundant, given H6).
---  Eliminated hypothesis H14 (redundant, given H11).
---  Eliminated hypothesis H15 (redundant, given H6).
---  Eliminated hypothesis H16 (redundant, given H11).
---  Eliminated hypothesis H38 (redundant, given H1).
---  Eliminated hypothesis H40 (redundant, given H1).
---  Eliminated hypothesis H41 (redundant, given H2).
-S-  Eliminated hypothesis H25.
     This was achieved by replacing all occurrences of loop__1__i by:
          lengthofdomainname__entry__loop__1 - 1.
<S>  New H12:  element(domainnameversion, [lengthofdomainname__entry__loop__1 - 
          1]) = 46
<S>  New H21:  findperiod(domainnameversion, lengthofdomainname__entry__loop__1)
           >= 0
<S>  New H22:  findperiod(domainnameversion, lengthofdomainname__entry__loop__1)
           <= 255
<S>  New H6:  lengthofdomainname__entry__loop__1 >= 2
<S>  New H11:  lengthofdomainname__entry__loop__1 <= 129
<S>  New H42:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], findperiod(domainnameversion, 
          lengthofdomainname__entry__loop__1)), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [i___1]) and 
          element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], findperiod(domainnameversion, 
          lengthofdomainname__entry__loop__1)), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [i___1]) <= 255)
<S>  New C1:  for_all(i_ : integer, 1 <= i_ and i_ <= 128 -> 0 <= element(
          update(update(update(wireversion, [lengthofdomainname__entry__loop__1]
          , findperiod(domainnameversion, lengthofdomainname__entry__loop__1)), 
          [1], findperiod(domainnameversion, 1)), [lengthofdomainname + 1], 0), 
          [i_]) and element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], findperiod(domainnameversion, 
          lengthofdomainname__entry__loop__1)), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [i_]) <= 255)
     +++  New H43:  integer__size >= 0
     +++  New H44:  character__size >= 0
     +++  New H45:  positive__size >= 0
     +++  New H46:  linelengthindex__size >= 0
     +++  New H47:  domainnamestringtypeindex__size >= 0
     +++  New H48:  wirestringtypeindex__size >= 0
>>>  Attempting to prove quantified formula C1 by "unwrapping" it.
+++  Added new hypotheses (in proving an implication formula).
     +++  New H49:  1 <= int_i__2
     +++  New H50:  int_i__2 <= 128
+++  New subgoal C1:  0 <= element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], findperiod(domainnameversion, 
          lengthofdomainname__entry__loop__1)), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [int_i__2]) and 
          element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], findperiod(domainnameversion, 
          lengthofdomainname__entry__loop__1)), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [int_i__2]) <= 
          255
>>>  Conclusion C1 has now been split into two, giving:
     >>>  C1:  0 <= element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], findperiod(domainnameversion, 
          lengthofdomainname__entry__loop__1)), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [int_i__2])
     >>>  C2:  element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], findperiod(domainnameversion, 
          lengthofdomainname__entry__loop__1)), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [int_i__2]) <= 
          255
***  Proved subgoal C1
     using hypotheses H42, H49 & H50.
***  Proved subgoal C2
     using hypotheses H42, H49 & H50.
***  Proved C1:  for_all(i_ : integer, 1 <= i_ and i_ <= 128 -> 0 <= element(
          update(update(update(wireversion, [lengthofdomainname__entry__loop__1]
          , findperiod(domainnameversion, lengthofdomainname__entry__loop__1)), 
          [1], findperiod(domainnameversion, 1)), [lengthofdomainname + 1], 0), 
          [i_]) and element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], findperiod(domainnameversion, 
          lengthofdomainname__entry__loop__1)), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [i_]) <= 255)
     by unwrapping a universally-quantified formula.
***  PROVED VC.


@@@@@@@@@@  VC: function_convertdomainnametowire_22.  @@@@@@@@@@
%%%  Simplified H3 on reading formula in, to give:
     %%%  H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(domainnameversion, [i___1]) and element(
          domainnameversion, [i___1]) <= character__last)
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H15 has been replaced by "true".  (It is already present, as H6)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H11).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H26).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H27).
---  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).
%%%  Simplified H38 on reading formula in, to give:
     %%%  H38:  for_all(i___1 : integer, wirestringtypeindex__first <= i___1 
          and i___1 <= wirestringtypeindex__last -> character__first <= element(
          update(update(update(wireversion, [loop__1__i + 1], element(
          domainnameversion, [loop__1__i])), [domainnamestringtypeindex__first]
          , findperiod(domainnameversion, domainnamestringtypeindex__first)), [
          lengthofdomainname + 1], 0), [i___1]) and element(update(update(
          update(wireversion, [loop__1__i + 1], element(domainnameversion, [
          loop__1__i])), [domainnamestringtypeindex__first], findperiod(
          domainnameversion, domainnamestringtypeindex__first)), [
          lengthofdomainname + 1], 0), [i___1]) <= character__last)
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  for_all(i_ : integer, domainnamestringtypeindex__first <= i_ and 
          i_ <= domainnamestringtypeindex__last -> 0 <= element(update(update(
          update(wireversion, [loop__1__i + 1], element(domainnameversion, [
          loop__1__i])), [domainnamestringtypeindex__first], findperiod(
          domainnameversion, domainnamestringtypeindex__first)), [
          lengthofdomainname + 1], 0), [i_]) and element(update(update(update(
          wireversion, [loop__1__i + 1], element(domainnameversion, [loop__1__i]
          )), [domainnamestringtypeindex__first], findperiod(domainnameversion, 
          domainnamestringtypeindex__first)), [lengthofdomainname + 1], 0), [i_]
          ) <= 255)
>>>  Restructured hypothesis H12 into:
     >>>  H12:  element(domainnameversion, [loop__1__i]) <> 46
-S-  Applied substitution rule convertdomai_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H2:  lengthofdomainname <= 128
-S-  Applied substitution rule convertdomai_rules(5).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H4:  loop__1__i >= - 2147483648
-S-  Applied substitution rule convertdomai_rules(6).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H5:  loop__1__i <= 2147483647
-S-  Applied substitution rule convertdomai_rules(7).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H19:  loop__1__i >= - 2147483649
<S>  New H36:  lengthofdomainname >= - 2147483649
-S-  Applied substitution rule convertdomai_rules(8).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H20:  loop__1__i <= 2147483646
<S>  New H37:  lengthofdomainname <= 2147483646
-S-  Applied substitution rule convertdomai_rules(10).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= character__last)
<S>  New H13:  element(domainnameversion, [loop__1__i]) >= 0
<S>  New H26:  findperiod(domainnameversion, domainnamestringtypeindex__first) 
          >= 0
<S>  New H30:  true
<S>  New H38:  for_all(i___1 : integer, wirestringtypeindex__first <= i___1 and 
          i___1 <= wirestringtypeindex__last -> 0 <= element(update(update(
          update(wireversion, [loop__1__i + 1], element(domainnameversion, [
          loop__1__i])), [domainnamestringtypeindex__first], findperiod(
          domainnameversion, domainnamestringtypeindex__first)), [
          lengthofdomainname + 1], 0), [i___1]) and element(update(update(
          update(wireversion, [loop__1__i + 1], element(domainnameversion, [
          loop__1__i])), [domainnamestringtypeindex__first], findperiod(
          domainnameversion, domainnamestringtypeindex__first)), [
          lengthofdomainname + 1], 0), [i___1]) <= character__last)
-S-  Applied substitution rule convertdomai_rules(11).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H14:  element(domainnameversion, [loop__1__i]) <= 255
<S>  New H27:  findperiod(domainnameversion, domainnamestringtypeindex__first) 
          <= 255
<S>  New H31:  true
<S>  New H3:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          domainnameversion, [i___1]) and element(domainnameversion, [i___1]) 
          <= 255)
<S>  New H38:  for_all(i___1 : integer, wirestringtypeindex__first <= i___1 and 
          i___1 <= wirestringtypeindex__last -> 0 <= element(update(update(
          update(wireversion, [loop__1__i + 1], element(domainnameversion, [
          loop__1__i])), [domainnamestringtypeindex__first], findperiod(
          domainnameversion, domainnamestringtypeindex__first)), [
          lengthofdomainname + 1], 0), [i___1]) and element(update(update(
          update(wireversion, [loop__1__i + 1], element(domainnameversion, [
          loop__1__i])), [domainnamestringtypeindex__first], findperiod(
          domainnameversion, domainnamestringtypeindex__first)), [
          lengthofdomainname + 1], 0), [i___1]) <= 255)
-S-  Applied substitution rule convertdomai_rules(20).
     This was achieved by replacing all occurrences of linelengthindex__first 
          by:
          1.
<S>  New H22:  domainnamestringtypeindex__first >= 1
-S-  Applied substitution rule convertdomai_rules(21).
     This was achieved by replacing all occurrences of linelengthindex__last by:
          256.
<S>  New H23:  domainnamestringtypeindex__first <= 256
-S-  Applied substitution rule convertdomai_rules(25).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H6:  loop__1__i >= 1
<S>  New H8:  lengthofdomainname__entry__loop__1 >= 1
<S>  New H24:  1 >= wirestringtypeindex__first
<S>  New H25:  1 <= wirestringtypeindex__last
<S>  New H26:  findperiod(domainnameversion, 1) >= 0
<S>  New H27:  findperiod(domainnameversion, 1) <= 255
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(domainnameversion, [
          i___1]) and element(domainnameversion, [i___1]) <= 255)
<S>  New H38:  for_all(i___1 : integer, wirestringtypeindex__first <= i___1 and 
          i___1 <= wirestringtypeindex__last -> 0 <= element(update(update(
          update(wireversion, [loop__1__i + 1], element(domainnameversion, [
          loop__1__i])), [1], findperiod(domainnameversion, 1)), [
          lengthofdomainname + 1], 0), [i___1]) and element(update(update(
          update(wireversion, [loop__1__i + 1], element(domainnameversion, [
          loop__1__i])), [1], findperiod(domainnameversion, 1)), [
          lengthofdomainname + 1], 0), [i___1]) <= 255)
<S>  New H22:  true
<S>  New H23:  true
<S>  New C1:  for_all(i_ : integer, 1 <= i_ and i_ <= 
          domainnamestringtypeindex__last -> 0 <= element(update(update(update(
          wireversion, [loop__1__i + 1], element(domainnameversion, [loop__1__i]
          )), [1], findperiod(domainnameversion, 1)), [lengthofdomainname + 1], 
          0), [i_]) and element(update(update(update(wireversion, [loop__1__i + 
          1], element(domainnameversion, [loop__1__i])), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [i_]) <= 255)
-S-  Applied substitution rule convertdomai_rules(26).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H9:  lengthofdomainname__entry__loop__1 <= 128
<S>  New H11:  loop__1__i <= 128
<S>  New H3:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(domainnameversion, [i___1]) and element(domainnameversion, [
          i___1]) <= 255)
<S>  New C1:  for_all(i_ : integer, 1 <= i_ and i_ <= 128 -> 0 <= element(
          update(update(update(wireversion, [loop__1__i + 1], element(
          domainnameversion, [loop__1__i])), [1], findperiod(domainnameversion, 
          1)), [lengthofdomainname + 1], 0), [i_]) and element(update(update(
          update(wireversion, [loop__1__i + 1], element(domainnameversion, [
          loop__1__i])), [1], findperiod(domainnameversion, 1)), [
          lengthofdomainname + 1], 0), [i_]) <= 255)
-S-  Applied substitution rule convertdomai_rules(30).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__first by:
          1.
<S>  New H17:  loop__1__i >= 0
<S>  New H34:  lengthofdomainname >= 0
<S>  New H24:  true
<S>  New H38:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          wirestringtypeindex__last -> 0 <= element(update(update(update(
          wireversion, [loop__1__i + 1], element(domainnameversion, [loop__1__i]
          )), [1], findperiod(domainnameversion, 1)), [lengthofdomainname + 1], 
          0), [i___1]) and element(update(update(update(wireversion, [
          loop__1__i + 1], element(domainnameversion, [loop__1__i])), [1], 
          findperiod(domainnameversion, 1)), [lengthofdomainname + 1], 0), [
          i___1]) <= 255)
-S-  Applied substitution rule convertdomai_rules(31).
     This was achieved by replacing all occurrences of 
          wirestringtypeindex__last by:
          129.
<S>  New H18:  loop__1__i <= 128
<S>  New H35:  lengthofdomainname <= 128
<S>  New H25:  true
<S>  New H38:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(update(update(update(wireversion, [loop__1__i + 1], element(
          domainnameversion, [loop__1__i])), [1], findperiod(domainnameversion, 
          1)), [lengthofdomainname + 1], 0), [i___1]) and element(update(update(
          update(wireversion, [loop__1__i + 1], element(domainnameversion, [
          loop__1__i])), [1], findperiod(domainnameversion, 1)), [
          lengthofdomainname + 1], 0), [i___1]) <= 255)
---  Eliminated hypothesis H10 (true-hypothesis).
---  Eliminated hypothesis H15 (true-hypothesis).
---  Eliminated hypothesis H16 (true-hypothesis).
---  Eliminated hypothesis H28 (true-hypothesis).
---  Eliminated hypothesis H29 (true-hypothesis).
---  Eliminated hypothesis H32 (true-hypothesis).
---  Eliminated hypothesis H33 (true-hypothesis).
---  Eliminated hypothesis H30 (true-hypothesis).
---  Eliminated hypothesis H31 (true-hypothesis).
---  Eliminated hypothesis H22 (true-hypothesis).
---  Eliminated hypothesis H23 (true-hypothesis).
---  Eliminated hypothesis H24 (true-hypothesis).
---  Eliminated hypothesis H25 (true-hypothesis).
---  Eliminated hypothesis H35 (duplicate of H2).
---  Eliminated hypothesis H18 (duplicate of H11).
---  Eliminated hypothesis H4 (redundant, given H6).
---  Eliminated hypothesis H5 (redundant, given H11).
---  Eliminated hypothesis H7 (redundant, given H21).
---  Eliminated hypothesis H17 (redundant, given H6).
---  Eliminated hypothesis H19 (redundant, given H6).
---  Eliminated hypothesis H20 (redundant, given H11).
---  Eliminated hypothesis H34 (redundant, given H1).
---  Eliminated hypothesis H36 (redundant, given H1).
---  Eliminated hypothesis H37 (redundant, given H2).
-S-  Eliminated hypothesis H21.
     This was achieved by replacing all occurrences of loop__1__i by:
          lengthofdomainname__entry__loop__1 - 1.
<S>  New H12:  element(domainnameversion, [lengthofdomainname__entry__loop__1 - 
          1]) <> 46
<S>  New H13:  element(domainnameversion, [lengthofdomainname__entry__loop__1 - 
          1]) >= 0
<S>  New H14:  element(domainnameversion, [lengthofdomainname__entry__loop__1 - 
          1]) <= 255
<S>  New H6:  lengthofdomainname__entry__loop__1 >= 2
<S>  New H11:  lengthofdomainname__entry__loop__1 <= 129
<S>  New H38:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], element(domainnameversion, [
          lengthofdomainname__entry__loop__1 - 1])), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [i___1]) and 
          element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], element(domainnameversion, [
          lengthofdomainname__entry__loop__1 - 1])), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [i___1]) <= 255)
<S>  New C1:  for_all(i_ : integer, 1 <= i_ and i_ <= 128 -> 0 <= element(
          update(update(update(wireversion, [lengthofdomainname__entry__loop__1]
          , element(domainnameversion, [lengthofdomainname__entry__loop__1 - 1])
          ), [1], findperiod(domainnameversion, 1)), [lengthofdomainname + 1], 
          0), [i_]) and element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], element(domainnameversion, [
          lengthofdomainname__entry__loop__1 - 1])), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [i_]) <= 255)
     +++  New H39:  integer__size >= 0
     +++  New H40:  character__size >= 0
     +++  New H41:  positive__size >= 0
     +++  New H42:  linelengthindex__size >= 0
     +++  New H43:  domainnamestringtypeindex__size >= 0
     +++  New H44:  wirestringtypeindex__size >= 0
>>>  Attempting to prove quantified formula C1 by "unwrapping" it.
+++  Added new hypotheses (in proving an implication formula).
     +++  New H45:  1 <= int_i__3
     +++  New H46:  int_i__3 <= 128
+++  New subgoal C1:  0 <= element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], element(domainnameversion, [
          lengthofdomainname__entry__loop__1 - 1])), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [int_i__3]) and 
          element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], element(domainnameversion, [
          lengthofdomainname__entry__loop__1 - 1])), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [int_i__3]) <= 
          255
>>>  Conclusion C1 has now been split into two, giving:
     >>>  C1:  0 <= element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], element(domainnameversion, [
          lengthofdomainname__entry__loop__1 - 1])), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [int_i__3])
     >>>  C2:  element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], element(domainnameversion, [
          lengthofdomainname__entry__loop__1 - 1])), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [int_i__3]) <= 
          255
***  Proved subgoal C1
     using hypotheses H38, H45 & H46.
***  Proved subgoal C2
     using hypotheses H38, H45 & H46.
***  Proved C1:  for_all(i_ : integer, 1 <= i_ and i_ <= 128 -> 0 <= element(
          update(update(update(wireversion, [lengthofdomainname__entry__loop__1]
          , element(domainnameversion, [lengthofdomainname__entry__loop__1 - 1])
          ), [1], findperiod(domainnameversion, 1)), [lengthofdomainname + 1], 
          0), [i_]) and element(update(update(update(wireversion, [
          lengthofdomainname__entry__loop__1], element(domainnameversion, [
          lengthofdomainname__entry__loop__1 - 1])), [1], findperiod(
          domainnameversion, 1)), [lengthofdomainname + 1], 0), [i_]) <= 255)
     by unwrapping a universally-quantified formula.
***  PROVED VC.

