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

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



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

procedure Rr_Type.AppendDomainNames






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


@@@@@@@@@@  VC: procedure_appenddomainnames_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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
***  Proved C1:  domainnamelength(right) >= domainnamestringtypeindex__first
     using hypothesis H8.
***  Proved C2:  domainnamelength(right) <= domainnamestringtypeindex__last
     using hypothesis H9.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
-S-  Applied substitution rule appenddomain_rules(6).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C1:  domainnamelength(left) + 1 + domainnamelength(right) >= - 
          2147483648
<S>  New C3:  domainnamelength(left) >= - 2147483649
-S-  Applied substitution rule appenddomain_rules(7).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C2:  domainnamelength(left) + 1 + domainnamelength(right) <= 2147483647
<S>  New C4:  domainnamelength(left) <= 2147483646
-S-  Applied substitution rule appenddomain_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 128 or element(
          left, [domainnamelength(left) + 1]) = 32 and for_all(q_ : integer, 1 
          <= q_ and q_ <= domainnamelength(left) -> element(left, [q_]) <> 32))
<S>  New H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 128 or 
          element(right, [domainnamelength(right) + 1]) = 32 and for_all(q_ : 
          integer, 1 <= q_ and q_ <= domainnamelength(right) -> element(right, [
          q_]) <> 32))
-S-  Applied substitution rule appenddomain_rules(9).
     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(
          left, [i___1]) and element(left, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= character__last)
-S-  Applied substitution rule appenddomain_rules(10).
     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(
          left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(19).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H3:  domainnamelength(left) >= 1
<S>  New H8:  domainnamelength(right) >= 1
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(left, [i___1]) and 
          element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(right, [i___1]) and 
          element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(20).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H4:  domainnamelength(left) <= 128
<S>  New H9:  domainnamelength(right) <= 128
<S>  New H15:  domainnamelength(left) = 128
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(right, [i___1]) and element(right, [i___1]) <= 255)
***  Proved C1:  domainnamelength(left) + 1 + domainnamelength(right) >= - 
          2147483648
     using hypotheses H3 & H8.
***  Proved C3:  domainnamelength(left) >= - 2147483649
     using hypothesis H3.
***  Proved C2:  domainnamelength(left) + 1 + domainnamelength(right) <= 
          2147483647
     using hypotheses H4 & H9.
***  Proved C4:  domainnamelength(left) <= 2147483646
     using hypothesis H4.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
-S-  Applied substitution rule appenddomain_rules(6).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C1:  domainnamelength(left) + 1 + domainnamelength(right) >= - 
          2147483648
<S>  New C3:  domainnamelength(left) >= - 2147483649
-S-  Applied substitution rule appenddomain_rules(7).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C2:  domainnamelength(left) + 1 + domainnamelength(right) <= 2147483647
<S>  New C4:  domainnamelength(left) <= 2147483646
>>>  Restructured hypothesis H15 into:
     >>>  H15:  domainnamelength(left) <> domainnamestringtypeindex__last
-S-  Applied substitution rule appenddomain_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 128 or element(
          left, [domainnamelength(left) + 1]) = 32 and for_all(q_ : integer, 1 
          <= q_ and q_ <= domainnamelength(left) -> element(left, [q_]) <> 32))
<S>  New H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 128 or 
          element(right, [domainnamelength(right) + 1]) = 32 and for_all(q_ : 
          integer, 1 <= q_ and q_ <= domainnamelength(right) -> element(right, [
          q_]) <> 32))
-S-  Applied substitution rule appenddomain_rules(9).
     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(
          left, [i___1]) and element(left, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= character__last)
-S-  Applied substitution rule appenddomain_rules(10).
     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(
          left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(19).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H3:  domainnamelength(left) >= 1
<S>  New H8:  domainnamelength(right) >= 1
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(left, [i___1]) and 
          element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(right, [i___1]) and 
          element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(20).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H4:  domainnamelength(left) <= 128
<S>  New H9:  domainnamelength(right) <= 128
<S>  New H15:  domainnamelength(left) <> 128
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(right, [i___1]) and element(right, [i___1]) <= 255)
%%%  Hypotheses H4 & H15 together imply that
          domainnamelength(left) < 128.
     H4 & H15 have therefore been deleted and a new H20 added to this effect.
***  Proved C1:  domainnamelength(left) + 1 + domainnamelength(right) >= - 
          2147483648
     using hypotheses H3 & H8.
***  Proved C3:  domainnamelength(left) >= - 2147483649
     using hypothesis H3.
***  Proved C2:  domainnamelength(left) + 1 + domainnamelength(right) <= 
          2147483647
     using hypotheses H9 & H20.
***  Proved C4:  domainnamelength(left) <= 2147483646
     using hypothesis H20.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_5.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
***  Proved C1:  domainnamelength(left) >= domainnamestringtypeindex__first
     using hypothesis H3.
***  Proved C2:  domainnamelength(left) <= domainnamestringtypeindex__last
     using hypothesis H4.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_6.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
***  Proved C1:  domainnamelength(left) >= domainnamestringtypeindex__first
     using hypothesis H3.
***  Proved C2:  domainnamelength(left) <= domainnamestringtypeindex__last
     using hypothesis H4.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_7.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
***  Proved C1:  domainnamelength(left) >= domainnamestringtypeindex__first
     using hypothesis H3.
***  Proved C2:  domainnamelength(left) <= domainnamestringtypeindex__last
     using hypothesis H4.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_8.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
***  Proved C1:  domainnamelength(left) >= domainnamestringtypeindex__first
     using hypothesis H3.
***  Proved C2:  domainnamelength(left) <= domainnamestringtypeindex__last
     using hypothesis H4.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_9.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
***  Proved C3:  domainnamelength(left) + 1 >= domainnamestringtypeindex__first
     using hypothesis H3.
***  Proved C5:  domainnamelength(left) + 1 >= integer__base__first
     using hypothesis H22.
***  Proved C6:  domainnamelength(left) + 1 <= integer__base__last
     using hypothesis H23.
-S-  Applied substitution rule appenddomain_rules(9).
     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(
          left, [i___1]) and element(left, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= character__last)
<S>  New C1:  true
-S-  Applied substitution rule appenddomain_rules(10).
     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(
          left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= 255)
<S>  New C2:  true
-S-  Applied substitution rule appenddomain_rules(20).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H4:  domainnamelength(left) <= 128
<S>  New H9:  domainnamelength(right) <= 128
<S>  New H15:  domainnamelength(left) = 128
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= 128 -> 0 <= element(left, [i___1]) and element(
          left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= 128 -> 0 <= element(right, [i___1]) and element(
          right, [i___1]) <= 255)
<S>  New C4:  domainnamelength(left) <= 127
***  Proved C1:  true
***  Proved C2:  true
>>>  Restructured hypothesis H30 into:
     >>>  H30:  element(left, [domainnamelength(left)]) <> origin_char or 
          domainnamelength(left) <> 1
-S-  Applied substitution rule appenddomain_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 128 or element(
          left, [domainnamelength(left) + 1]) = 32 and for_all(q_ : integer, 1 
          <= q_ and q_ <= domainnamelength(left) -> element(left, [q_]) <> 32))
<S>  New H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 128 or 
          element(right, [domainnamelength(right) + 1]) = 32 and for_all(q_ : 
          integer, 1 <= q_ and q_ <= domainnamelength(right) -> element(right, [
          q_]) <> 32))
<S>  New H24:  domainnamelength(left) + 1 + domainnamelength(right) > 128
-S-  Applied substitution rule appenddomain_rules(2).
     This was achieved by replacing all occurrences of origin_char by:
          64.
<S>  New H30:  element(left, [domainnamelength(left)]) <> 64 or 
          domainnamelength(left) <> 1
-S-  Applied substitution rule appenddomain_rules(6).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H20:  domainnamelength(left) + 1 + domainnamelength(right) >= - 
          2147483648
<S>  New H22:  domainnamelength(left) >= - 2147483649
-S-  Applied substitution rule appenddomain_rules(7).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H21:  domainnamelength(left) + 1 + domainnamelength(right) <= 
          2147483647
<S>  New H23:  domainnamelength(left) <= 2147483646
-S-  Applied substitution rule appenddomain_rules(19).
     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 <= 128 -> 0 <= 
          element(left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(right, [i___1]) and element(right, [i___1]) <= 255)
<S>  New H3:  domainnamelength(left) >= 1
<S>  New H8:  domainnamelength(right) >= 1
###  Established a contradiction [false-hypothesis] using hypothesis H25.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_10.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
***  Proved C3:  domainnamelength(left) + 1 >= domainnamestringtypeindex__first
     using hypothesis H3.
***  Proved C5:  domainnamelength(left) + 1 >= integer__base__first
     using hypothesis H22.
***  Proved C6:  domainnamelength(left) + 1 <= integer__base__last
     using hypothesis H23.
-S-  Applied substitution rule appenddomain_rules(9).
     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(
          left, [i___1]) and element(left, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= character__last)
<S>  New C1:  true
-S-  Applied substitution rule appenddomain_rules(10).
     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(
          left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= 255)
<S>  New C2:  true
-S-  Applied substitution rule appenddomain_rules(20).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H4:  domainnamelength(left) <= 128
<S>  New H9:  domainnamelength(right) <= 128
<S>  New H15:  not domainnamelength(left) = 128
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= 128 -> 0 <= element(left, [i___1]) and element(
          left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= 128 -> 0 <= element(right, [i___1]) and element(
          right, [i___1]) <= 255)
<S>  New C4:  domainnamelength(left) <= 127
***  Proved C1:  true
***  Proved C2:  true
***  Proved C4:  domainnamelength(left) <= 127
     using hypotheses H4 & H15.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
***  Proved C3:  domainnamelength(left) + 1 >= domainnamestringtypeindex__first
     using hypothesis H3.
***  Proved C5:  domainnamelength(left) + 1 >= integer__base__first
     using hypothesis H22.
***  Proved C6:  domainnamelength(left) + 1 <= integer__base__last
     using hypothesis H23.
-S-  Applied substitution rule appenddomain_rules(9).
     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(
          left, [i___1]) and element(left, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= character__last)
<S>  New C1:  true
-S-  Applied substitution rule appenddomain_rules(10).
     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(
          left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= 255)
<S>  New C2:  true
-S-  Applied substitution rule appenddomain_rules(20).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H4:  domainnamelength(left) <= 128
<S>  New H9:  domainnamelength(right) <= 128
<S>  New H15:  domainnamelength(left) = 128
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= 128 -> 0 <= element(left, [i___1]) and element(
          left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= 128 -> 0 <= element(right, [i___1]) and element(
          right, [i___1]) <= 255)
<S>  New C4:  domainnamelength(left) <= 127
***  Proved C1:  true
***  Proved C2:  true
>>>  Restructured hypothesis H24 into:
     >>>  H24:  domainnamelength(left) + 1 + domainnamelength(right) <= 
          maxdomainnamelength
>>>  Restructured hypothesis H30 into:
     >>>  H30:  element(left, [domainnamelength(left)]) <> origin_char or 
          domainnamelength(left) <> 1
-S-  Applied substitution rule appenddomain_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 128 or element(
          left, [domainnamelength(left) + 1]) = 32 and for_all(q_ : integer, 1 
          <= q_ and q_ <= domainnamelength(left) -> element(left, [q_]) <> 32))
<S>  New H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 128 or 
          element(right, [domainnamelength(right) + 1]) = 32 and for_all(q_ : 
          integer, 1 <= q_ and q_ <= domainnamelength(right) -> element(right, [
          q_]) <> 32))
<S>  New H24:  domainnamelength(left) + 1 + domainnamelength(right) <= 128
-S-  Applied substitution rule appenddomain_rules(2).
     This was achieved by replacing all occurrences of origin_char by:
          64.
<S>  New H30:  element(left, [domainnamelength(left)]) <> 64 or 
          domainnamelength(left) <> 1
-S-  Applied substitution rule appenddomain_rules(6).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H20:  domainnamelength(left) + 1 + domainnamelength(right) >= - 
          2147483648
<S>  New H22:  domainnamelength(left) >= - 2147483649
-S-  Applied substitution rule appenddomain_rules(7).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H21:  domainnamelength(left) + 1 + domainnamelength(right) <= 
          2147483647
<S>  New H23:  domainnamelength(left) <= 2147483646
-S-  Applied substitution rule appenddomain_rules(19).
     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 <= 128 -> 0 <= 
          element(left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(right, [i___1]) and element(right, [i___1]) <= 255)
<S>  New H3:  domainnamelength(left) >= 1
<S>  New H8:  domainnamelength(right) >= 1
###  Established a contradiction [false-hypothesis] using hypothesis H25.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_12.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
***  Proved C3:  domainnamelength(left) + 1 >= domainnamestringtypeindex__first
     using hypothesis H3.
***  Proved C5:  domainnamelength(left) + 1 >= integer__base__first
     using hypothesis H22.
***  Proved C6:  domainnamelength(left) + 1 <= integer__base__last
     using hypothesis H23.
-S-  Applied substitution rule appenddomain_rules(9).
     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(
          left, [i___1]) and element(left, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= character__last)
<S>  New C1:  true
-S-  Applied substitution rule appenddomain_rules(10).
     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(
          left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= 255)
<S>  New C2:  true
-S-  Applied substitution rule appenddomain_rules(20).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H4:  domainnamelength(left) <= 128
<S>  New H9:  domainnamelength(right) <= 128
<S>  New H15:  not domainnamelength(left) = 128
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= 128 -> 0 <= element(left, [i___1]) and element(
          left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= 128 -> 0 <= element(right, [i___1]) and element(
          right, [i___1]) <= 255)
<S>  New C4:  domainnamelength(left) <= 127
***  Proved C1:  true
***  Proved C2:  true
***  Proved C4:  domainnamelength(left) <= 127
     using hypotheses H4 & H15.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_13.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H38 has been replaced by "true".  (It is already present, as H9)
          .
-S-  Applied substitution rule appenddomain_rules(4).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C1:  domainnamelength(right) >= - 2147483648
<S>  New C3:  true
-S-  Applied substitution rule appenddomain_rules(5).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C2:  domainnamelength(right) <= 2147483647
<S>  New C4:  true
***  Proved C3:  true
***  Proved C4:  true
>>>  Restructured hypothesis H30 into:
     >>>  H30:  element(left, [domainnamelength(left)]) <> origin_char or 
          domainnamelength(left) <> 1
-S-  Applied substitution rule appenddomain_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 128 or element(
          left, [domainnamelength(left) + 1]) = 32 and for_all(q_ : integer, 1 
          <= q_ and q_ <= domainnamelength(left) -> element(left, [q_]) <> 32))
<S>  New H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 128 or 
          element(right, [domainnamelength(right) + 1]) = 32 and for_all(q_ : 
          integer, 1 <= q_ and q_ <= domainnamelength(right) -> element(right, [
          q_]) <> 32))
<S>  New H24:  domainnamelength(left) + 1 + domainnamelength(right) > 128
-S-  Applied substitution rule appenddomain_rules(2).
     This was achieved by replacing all occurrences of origin_char by:
          64.
<S>  New H30:  element(left, [domainnamelength(left)]) <> 64 or 
          domainnamelength(left) <> 1
-S-  Applied substitution rule appenddomain_rules(6).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H20:  domainnamelength(left) + 1 + domainnamelength(right) >= - 
          2147483648
<S>  New H22:  domainnamelength(left) >= - 2147483649
-S-  Applied substitution rule appenddomain_rules(7).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H21:  domainnamelength(left) + 1 + domainnamelength(right) <= 
          2147483647
<S>  New H23:  domainnamelength(left) <= 2147483646
-S-  Applied substitution rule appenddomain_rules(9).
     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(
          left, [i___1]) and element(left, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= character__last)
<S>  New H31:  true
-S-  Applied substitution rule appenddomain_rules(10).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H32:  true
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(19).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H3:  domainnamelength(left) >= 1
<S>  New H8:  domainnamelength(right) >= 1
<S>  New H33:  domainnamelength(left) >= 0
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(left, [i___1]) and 
          element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(right, [i___1]) and 
          element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(20).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H4:  domainnamelength(left) <= 128
<S>  New H9:  domainnamelength(right) <= 128
<S>  New H15:  domainnamelength(left) = 128
<S>  New H34:  domainnamelength(left) <= 127
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(right, [i___1]) and element(right, [i___1]) <= 255)
***  Proved C1:  domainnamelength(right) >= - 2147483648
     using hypothesis H8.
***  Proved C2:  domainnamelength(right) <= 2147483647
     using hypothesis H9.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H38 has been replaced by "true".  (It is already present, as H9)
          .
-S-  Applied substitution rule appenddomain_rules(4).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C1:  domainnamelength(right) >= - 2147483648
<S>  New C3:  true
-S-  Applied substitution rule appenddomain_rules(5).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C2:  domainnamelength(right) <= 2147483647
<S>  New C4:  true
***  Proved C3:  true
***  Proved C4:  true
>>>  Restructured hypothesis H15 into:
     >>>  H15:  domainnamelength(left) <> domainnamestringtypeindex__last
>>>  Restructured hypothesis H30 into:
     >>>  H30:  element(left, [domainnamelength(left)]) <> origin_char or 
          domainnamelength(left) <> 1
-S-  Applied substitution rule appenddomain_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 128 or element(
          left, [domainnamelength(left) + 1]) = 32 and for_all(q_ : integer, 1 
          <= q_ and q_ <= domainnamelength(left) -> element(left, [q_]) <> 32))
<S>  New H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 128 or 
          element(right, [domainnamelength(right) + 1]) = 32 and for_all(q_ : 
          integer, 1 <= q_ and q_ <= domainnamelength(right) -> element(right, [
          q_]) <> 32))
<S>  New H24:  domainnamelength(left) + 1 + domainnamelength(right) > 128
-S-  Applied substitution rule appenddomain_rules(2).
     This was achieved by replacing all occurrences of origin_char by:
          64.
<S>  New H30:  element(left, [domainnamelength(left)]) <> 64 or 
          domainnamelength(left) <> 1
-S-  Applied substitution rule appenddomain_rules(6).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H20:  domainnamelength(left) + 1 + domainnamelength(right) >= - 
          2147483648
<S>  New H22:  domainnamelength(left) >= - 2147483649
-S-  Applied substitution rule appenddomain_rules(7).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H21:  domainnamelength(left) + 1 + domainnamelength(right) <= 
          2147483647
<S>  New H23:  domainnamelength(left) <= 2147483646
-S-  Applied substitution rule appenddomain_rules(9).
     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(
          left, [i___1]) and element(left, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= character__last)
<S>  New H31:  true
-S-  Applied substitution rule appenddomain_rules(10).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H32:  true
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(19).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H3:  domainnamelength(left) >= 1
<S>  New H8:  domainnamelength(right) >= 1
<S>  New H33:  domainnamelength(left) >= 0
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(left, [i___1]) and 
          element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(right, [i___1]) and 
          element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(20).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H4:  domainnamelength(left) <= 128
<S>  New H9:  domainnamelength(right) <= 128
<S>  New H15:  domainnamelength(left) <> 128
<S>  New H34:  domainnamelength(left) <= 127
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(right, [i___1]) and element(right, [i___1]) <= 255)
%%%  Hypotheses H4 & H15 together imply that
          domainnamelength(left) < 128.
     H4 & H15 have therefore been deleted and a new H39 added to this effect.
***  Proved C1:  domainnamelength(right) >= - 2147483648
     using hypothesis H8.
***  Proved C2:  domainnamelength(right) <= 2147483647
     using hypothesis H9.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_15.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H38 has been replaced by "true".  (It is already present, as H9)
          .
-S-  Applied substitution rule appenddomain_rules(4).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C1:  domainnamelength(right) >= - 2147483648
<S>  New C3:  true
-S-  Applied substitution rule appenddomain_rules(5).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C2:  domainnamelength(right) <= 2147483647
<S>  New C4:  true
***  Proved C3:  true
***  Proved C4:  true
>>>  Restructured hypothesis H24 into:
     >>>  H24:  domainnamelength(left) + 1 + domainnamelength(right) <= 
          maxdomainnamelength
>>>  Restructured hypothesis H30 into:
     >>>  H30:  element(left, [domainnamelength(left)]) <> origin_char or 
          domainnamelength(left) <> 1
-S-  Applied substitution rule appenddomain_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 128 or element(
          left, [domainnamelength(left) + 1]) = 32 and for_all(q_ : integer, 1 
          <= q_ and q_ <= domainnamelength(left) -> element(left, [q_]) <> 32))
<S>  New H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 128 or 
          element(right, [domainnamelength(right) + 1]) = 32 and for_all(q_ : 
          integer, 1 <= q_ and q_ <= domainnamelength(right) -> element(right, [
          q_]) <> 32))
<S>  New H24:  domainnamelength(left) + 1 + domainnamelength(right) <= 128
-S-  Applied substitution rule appenddomain_rules(2).
     This was achieved by replacing all occurrences of origin_char by:
          64.
<S>  New H30:  element(left, [domainnamelength(left)]) <> 64 or 
          domainnamelength(left) <> 1
-S-  Applied substitution rule appenddomain_rules(6).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H20:  domainnamelength(left) + 1 + domainnamelength(right) >= - 
          2147483648
<S>  New H22:  domainnamelength(left) >= - 2147483649
-S-  Applied substitution rule appenddomain_rules(7).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H21:  domainnamelength(left) + 1 + domainnamelength(right) <= 
          2147483647
<S>  New H23:  domainnamelength(left) <= 2147483646
-S-  Applied substitution rule appenddomain_rules(9).
     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(
          left, [i___1]) and element(left, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= character__last)
<S>  New H31:  true
-S-  Applied substitution rule appenddomain_rules(10).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H32:  true
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(19).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H3:  domainnamelength(left) >= 1
<S>  New H8:  domainnamelength(right) >= 1
<S>  New H33:  domainnamelength(left) >= 0
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(left, [i___1]) and 
          element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(right, [i___1]) and 
          element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(20).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H4:  domainnamelength(left) <= 128
<S>  New H9:  domainnamelength(right) <= 128
<S>  New H15:  domainnamelength(left) = 128
<S>  New H34:  domainnamelength(left) <= 127
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(right, [i___1]) and element(right, [i___1]) <= 255)
***  Proved C1:  domainnamelength(right) >= - 2147483648
     using hypothesis H8.
***  Proved C2:  domainnamelength(right) <= 2147483647
     using hypothesis H9.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_16.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H38 has been replaced by "true".  (It is already present, as H9)
          .
-S-  Applied substitution rule appenddomain_rules(4).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C1:  domainnamelength(right) >= - 2147483648
<S>  New C3:  true
-S-  Applied substitution rule appenddomain_rules(5).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C2:  domainnamelength(right) <= 2147483647
<S>  New C4:  true
***  Proved C3:  true
***  Proved C4:  true
>>>  Restructured hypothesis H15 into:
     >>>  H15:  domainnamelength(left) <> domainnamestringtypeindex__last
>>>  Restructured hypothesis H24 into:
     >>>  H24:  domainnamelength(left) + 1 + domainnamelength(right) <= 
          maxdomainnamelength
>>>  Restructured hypothesis H30 into:
     >>>  H30:  element(left, [domainnamelength(left)]) <> origin_char or 
          domainnamelength(left) <> 1
-S-  Applied substitution rule appenddomain_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 128 or element(
          left, [domainnamelength(left) + 1]) = 32 and for_all(q_ : integer, 1 
          <= q_ and q_ <= domainnamelength(left) -> element(left, [q_]) <> 32))
<S>  New H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 128 or 
          element(right, [domainnamelength(right) + 1]) = 32 and for_all(q_ : 
          integer, 1 <= q_ and q_ <= domainnamelength(right) -> element(right, [
          q_]) <> 32))
<S>  New H24:  domainnamelength(left) + 1 + domainnamelength(right) <= 128
-S-  Applied substitution rule appenddomain_rules(2).
     This was achieved by replacing all occurrences of origin_char by:
          64.
<S>  New H30:  element(left, [domainnamelength(left)]) <> 64 or 
          domainnamelength(left) <> 1
-S-  Applied substitution rule appenddomain_rules(6).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H20:  domainnamelength(left) + 1 + domainnamelength(right) >= - 
          2147483648
<S>  New H22:  domainnamelength(left) >= - 2147483649
-S-  Applied substitution rule appenddomain_rules(7).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H21:  domainnamelength(left) + 1 + domainnamelength(right) <= 
          2147483647
<S>  New H23:  domainnamelength(left) <= 2147483646
-S-  Applied substitution rule appenddomain_rules(9).
     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(
          left, [i___1]) and element(left, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= character__last)
<S>  New H31:  true
-S-  Applied substitution rule appenddomain_rules(10).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H32:  true
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(19).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H3:  domainnamelength(left) >= 1
<S>  New H8:  domainnamelength(right) >= 1
<S>  New H33:  domainnamelength(left) >= 0
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(left, [i___1]) and 
          element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(right, [i___1]) and 
          element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(20).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H4:  domainnamelength(left) <= 128
<S>  New H9:  domainnamelength(right) <= 128
<S>  New H15:  domainnamelength(left) <> 128
<S>  New H34:  domainnamelength(left) <= 127
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(right, [i___1]) and element(right, [i___1]) <= 255)
%%%  Hypotheses H4 & H15 together imply that
          domainnamelength(left) < 128.
     H4 & H15 have therefore been deleted and a new H39 added to this effect.
***  Proved C1:  domainnamelength(right) >= - 2147483648
     using hypothesis H8.
***  Proved C2:  domainnamelength(right) <= 2147483647
     using hypothesis H9.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H38 has been replaced by "true".  (It is already present, as H9)
          .
***  Proved C1:  1 <= domainnamelength(right) -> domainnamelength(right) >= 
          integer__first and domainnamelength(right) <= integer__last
     using hypotheses H39 & H40.
***  Proved C2:  1 <= domainnamelength(right) -> 1 >= integer__first and 1 <= 
          integer__last
     using hypotheses H41 & H42.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_18.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H38 has been replaced by "true".  (It is already present, as H9)
          .
***  Proved C1:  1 <= domainnamelength(right) -> domainnamelength(right) >= 
          integer__first and domainnamelength(right) <= integer__last
     using hypotheses H39 & H40.
***  Proved C2:  1 <= domainnamelength(right) -> 1 >= integer__first and 1 <= 
          integer__last
     using hypotheses H41 & H42.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_19.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H38 has been replaced by "true".  (It is already present, as H9)
          .
***  Proved C1:  1 <= domainnamelength(right) -> domainnamelength(right) >= 
          integer__first and domainnamelength(right) <= integer__last
     using hypotheses H39 & H40.
***  Proved C2:  1 <= domainnamelength(right) -> 1 >= integer__first and 1 <= 
          integer__last
     using hypotheses H41 & H42.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H38 has been replaced by "true".  (It is already present, as H9)
          .
***  Proved C1:  1 <= domainnamelength(right) -> domainnamelength(right) >= 
          integer__first and domainnamelength(right) <= integer__last
     using hypotheses H39 & H40.
***  Proved C2:  1 <= domainnamelength(right) -> 1 >= integer__first and 1 <= 
          integer__last
     using hypotheses H41 & H42.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_21.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H38 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H45 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H46 has been replaced by "true".  (It is already present, as H9)
          .
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  true
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) and element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) <= character__last)
%%%  Simplified C6 on reading formula in, to give:
     %%%  C6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  true
***  Proved C1:  domainnamelength(left) >= domainnamestringtypeindex__first
     using hypothesis H3.
***  Proved C2:  domainnamelength(left) < domainnamestringtypeindex__last
     using hypothesis H34.
***  Proved C4:  true
***  Proved C5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) and element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) <= character__last)
     using hypotheses H1, H31, H32, H33 & H34.
***  Proved C6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
     using hypothesis H2.
***  Proved C7:  1 >= integer__first
     using hypothesis H41.
***  Proved C8:  1 <= integer__last
     using hypothesis H42.
***  Proved C9:  true
***  Proved C10:  1 <= domainnamelength(right)
     using hypothesis H47.
***  Proved C11:  domainnamelength(right) >= domainnamestringtypeindex__first
     using hypothesis H8.
***  Proved C12:  domainnamelength(right) <= domainnamestringtypeindex__last
     using hypothesis H9.
-S-  Applied substitution rule appenddomain_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 128 or element(
          left, [domainnamelength(left) + 1]) = 32 and for_all(q_ : integer, 1 
          <= q_ and q_ <= domainnamelength(left) -> element(left, [q_]) <> 32))
<S>  New H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 128 or 
          element(right, [domainnamelength(right) + 1]) = 32 and for_all(q_ : 
          integer, 1 <= q_ and q_ <= domainnamelength(right) -> element(right, [
          q_]) <> 32))
<S>  New H24:  domainnamelength(left) + 1 + domainnamelength(right) > 128
<S>  New C3:  domainnamelength(left) + 1 + domainnamelength(right) <= 128
>>>  Restructured hypothesis H30 into:
     >>>  H30:  element(left, [domainnamelength(left)]) <> origin_char or 
          domainnamelength(left) <> 1
+++  Using "A->B, A |- B" on hypotheses H43 & H47 yields a new hypothesis:
     +++  H48:  domainnamelength(right) >= integer__first and domainnamelength(
          right) <= integer__last
+++  Using "A->B, A |- B" on hypotheses H44 & H47 yields a new hypothesis:
     +++  H49:  1 >= integer__first and 1 <= integer__last
-S-  Applied substitution rule appenddomain_rules(2).
     This was achieved by replacing all occurrences of origin_char by:
          64.
<S>  New H30:  element(left, [domainnamelength(left)]) <> 64 or 
          domainnamelength(left) <> 1
-S-  Applied substitution rule appenddomain_rules(4).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H39:  domainnamelength(right) >= - 2147483648
<S>  New H41:  true
<S>  New H43:  1 <= domainnamelength(right) -> domainnamelength(right) >= - 
          2147483648 and domainnamelength(right) <= integer__last
<S>  New H44:  1 <= domainnamelength(right) -> 1 <= integer__last
<S>  New H48:  domainnamelength(right) >= - 2147483648 and domainnamelength(
          right) <= integer__last
<S>  New H49:  1 <= integer__last
-S-  Applied substitution rule appenddomain_rules(5).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H40:  domainnamelength(right) <= 2147483647
<S>  New H42:  true
<S>  New H43:  1 <= domainnamelength(right) -> domainnamelength(right) >= - 
          2147483648 and domainnamelength(right) <= 2147483647
<S>  New H44:  true
<S>  New H48:  domainnamelength(right) >= - 2147483648 and domainnamelength(
          right) <= 2147483647
<S>  New H49:  true
-S-  Applied substitution rule appenddomain_rules(6).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H20:  domainnamelength(left) + 1 + domainnamelength(right) >= - 
          2147483648
<S>  New H22:  domainnamelength(left) >= - 2147483649
-S-  Applied substitution rule appenddomain_rules(7).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H21:  domainnamelength(left) + 1 + domainnamelength(right) <= 
          2147483647
<S>  New H23:  domainnamelength(left) <= 2147483646
-S-  Applied substitution rule appenddomain_rules(9).
     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(
          left, [i___1]) and element(left, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= character__last)
<S>  New H31:  true
-S-  Applied substitution rule appenddomain_rules(10).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H32:  true
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(19).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H3:  domainnamelength(left) >= 1
<S>  New H8:  domainnamelength(right) >= 1
<S>  New H33:  domainnamelength(left) >= 0
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(left, [i___1]) and 
          element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(right, [i___1]) and 
          element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(20).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H4:  domainnamelength(left) <= 128
<S>  New H9:  domainnamelength(right) <= 128
<S>  New H15:  domainnamelength(left) = 128
<S>  New H34:  domainnamelength(left) <= 127
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(right, [i___1]) and element(right, [i___1]) <= 255)
###  Established a contradiction [false-hypothesis] using hypothesis H25.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_22.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H38 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H45 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H46 has been replaced by "true".  (It is already present, as H9)
          .
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  true
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) and element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) <= character__last)
%%%  Simplified C6 on reading formula in, to give:
     %%%  C6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  true
***  Proved C1:  domainnamelength(left) >= domainnamestringtypeindex__first
     using hypothesis H3.
***  Proved C2:  domainnamelength(left) < domainnamestringtypeindex__last
     using hypotheses H4 & H15.
***  Proved C4:  true
***  Proved C5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) and element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) <= character__last)
     using hypotheses H1, H31, H32, H33 & H34.
***  Proved C6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
     using hypothesis H2.
***  Proved C7:  1 >= integer__first
     using hypothesis H41.
***  Proved C8:  1 <= integer__last
     using hypothesis H42.
***  Proved C9:  true
***  Proved C10:  1 <= domainnamelength(right)
     using hypothesis H47.
***  Proved C11:  domainnamelength(right) >= domainnamestringtypeindex__first
     using hypothesis H8.
***  Proved C12:  domainnamelength(right) <= domainnamestringtypeindex__last
     using hypothesis H9.
-S-  Applied substitution rule appenddomain_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 128 or element(
          left, [domainnamelength(left) + 1]) = 32 and for_all(q_ : integer, 1 
          <= q_ and q_ <= domainnamelength(left) -> element(left, [q_]) <> 32))
<S>  New H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 128 or 
          element(right, [domainnamelength(right) + 1]) = 32 and for_all(q_ : 
          integer, 1 <= q_ and q_ <= domainnamelength(right) -> element(right, [
          q_]) <> 32))
<S>  New H24:  domainnamelength(left) + 1 + domainnamelength(right) > 128
<S>  New C3:  domainnamelength(left) + 1 + domainnamelength(right) <= 128
>>>  Restructured hypothesis H15 into:
     >>>  H15:  domainnamelength(left) <> domainnamestringtypeindex__last
>>>  Restructured hypothesis H30 into:
     >>>  H30:  element(left, [domainnamelength(left)]) <> origin_char or 
          domainnamelength(left) <> 1
+++  Using "A->B, A |- B" on hypotheses H43 & H47 yields a new hypothesis:
     +++  H48:  domainnamelength(right) >= integer__first and domainnamelength(
          right) <= integer__last
+++  Using "A->B, A |- B" on hypotheses H44 & H47 yields a new hypothesis:
     +++  H49:  1 >= integer__first and 1 <= integer__last
-S-  Applied substitution rule appenddomain_rules(2).
     This was achieved by replacing all occurrences of origin_char by:
          64.
<S>  New H30:  element(left, [domainnamelength(left)]) <> 64 or 
          domainnamelength(left) <> 1
-S-  Applied substitution rule appenddomain_rules(4).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H39:  domainnamelength(right) >= - 2147483648
<S>  New H41:  true
<S>  New H43:  1 <= domainnamelength(right) -> domainnamelength(right) >= - 
          2147483648 and domainnamelength(right) <= integer__last
<S>  New H44:  1 <= domainnamelength(right) -> 1 <= integer__last
<S>  New H48:  domainnamelength(right) >= - 2147483648 and domainnamelength(
          right) <= integer__last
<S>  New H49:  1 <= integer__last
-S-  Applied substitution rule appenddomain_rules(5).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H40:  domainnamelength(right) <= 2147483647
<S>  New H42:  true
<S>  New H43:  1 <= domainnamelength(right) -> domainnamelength(right) >= - 
          2147483648 and domainnamelength(right) <= 2147483647
<S>  New H44:  true
<S>  New H48:  domainnamelength(right) >= - 2147483648 and domainnamelength(
          right) <= 2147483647
<S>  New H49:  true
-S-  Applied substitution rule appenddomain_rules(6).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H20:  domainnamelength(left) + 1 + domainnamelength(right) >= - 
          2147483648
<S>  New H22:  domainnamelength(left) >= - 2147483649
-S-  Applied substitution rule appenddomain_rules(7).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H21:  domainnamelength(left) + 1 + domainnamelength(right) <= 
          2147483647
<S>  New H23:  domainnamelength(left) <= 2147483646
-S-  Applied substitution rule appenddomain_rules(9).
     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(
          left, [i___1]) and element(left, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= character__last)
<S>  New H31:  true
-S-  Applied substitution rule appenddomain_rules(10).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H32:  true
<S>  New H1:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(19).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H3:  domainnamelength(left) >= 1
<S>  New H8:  domainnamelength(right) >= 1
<S>  New H33:  domainnamelength(left) >= 0
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(left, [i___1]) and 
          element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(right, [i___1]) and 
          element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(20).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H4:  domainnamelength(left) <= 128
<S>  New H9:  domainnamelength(right) <= 128
<S>  New H15:  domainnamelength(left) <> 128
<S>  New H34:  domainnamelength(left) <= 127
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(right, [i___1]) and element(right, [i___1]) <= 255)
%%%  Hypotheses H4 & H15 together imply that
          domainnamelength(left) < 128.
     H4 & H15 have therefore been deleted and a new H50 added to this effect.
###  Established a contradiction [false-hypothesis] using hypothesis H25.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_23.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H38 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H45 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H46 has been replaced by "true".  (It is already present, as H9)
          .
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  true
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) and element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) <= character__last)
%%%  Simplified C6 on reading formula in, to give:
     %%%  C6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  true
***  Proved C1:  domainnamelength(left) >= domainnamestringtypeindex__first
     using hypothesis H3.
***  Proved C2:  domainnamelength(left) < domainnamestringtypeindex__last
     using hypothesis H34.
***  Proved C3:  domainnamelength(left) + 1 + domainnamelength(right) <= 
          maxdomainnamelength
     using hypothesis H24.
***  Proved C4:  true
***  Proved C5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) and element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) <= character__last)
     using hypotheses H1, H31, H32, H33 & H34.
***  Proved C6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
     using hypothesis H2.
***  Proved C7:  1 >= integer__first
     using hypothesis H41.
***  Proved C8:  1 <= integer__last
     using hypothesis H42.
***  Proved C9:  true
***  Proved C10:  1 <= domainnamelength(right)
     using hypothesis H47.
***  Proved C11:  domainnamelength(right) >= domainnamestringtypeindex__first
     using hypothesis H8.
***  Proved C12:  domainnamelength(right) <= domainnamestringtypeindex__last
     using hypothesis H9.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_24.  @@@@@@@@@@
%%%  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(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  domainnamelength(left) = 1 and (element(left, [1]) = 32 or 
          element(left, [2]) = 32) or (domainnamelength(left) = 
          maxdomainnamelength or element(left, [domainnamelength(left) + 1]) = 
          32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(left) 
          -> element(left, [q_]) <> 32))
---  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 H4).
%%%  Simplified H10 on reading formula in, to give:
     %%%  H10:  domainnamelength(right) = 1 and (element(right, [1]) = 32 or 
          element(right, [2]) = 32) or (domainnamelength(right) = 
          maxdomainnamelength or element(right, [domainnamelength(right) + 1]) 
          = 32 and for_all(q_ : integer, 1 <= q_ and q_ <= domainnamelength(
          right) -> element(right, [q_]) <> 32))
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H26 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H27 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H23).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H38 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H45 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H46 has been replaced by "true".  (It is already present, as H9)
          .
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  true
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) and element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) <= character__last)
%%%  Simplified C6 on reading formula in, to give:
     %%%  C6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  true
***  Proved C1:  domainnamelength(left) >= domainnamestringtypeindex__first
     using hypothesis H3.
***  Proved C2:  domainnamelength(left) < domainnamestringtypeindex__last
     using hypotheses H4 & H15.
***  Proved C3:  domainnamelength(left) + 1 + domainnamelength(right) <= 
          maxdomainnamelength
     using hypothesis H24.
***  Proved C4:  true
***  Proved C5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) and element(update(left, [domainnamelength(left) + 1]
          , 46), [i___1]) <= character__last)
     using hypotheses H1, H31, H32, H33 & H34.
***  Proved C6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
     using hypothesis H2.
***  Proved C7:  1 >= integer__first
     using hypothesis H41.
***  Proved C8:  1 <= integer__last
     using hypothesis H42.
***  Proved C9:  true
***  Proved C10:  1 <= domainnamelength(right)
     using hypothesis H47.
***  Proved C11:  domainnamelength(right) >= domainnamestringtypeindex__first
     using hypothesis H8.
***  Proved C12:  domainnamelength(right) <= domainnamestringtypeindex__last
     using hypothesis H9.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_25.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H6 on reading formula in, to give:
     %%%  H6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(update(left, [lengthl + 1 + loop__1__i], 
          element(right, [loop__1__i])), [i___1]) and element(update(left, [
          lengthl + 1 + loop__1__i], element(right, [loop__1__i])), [i___1]) <= 
          character__last)
%%%  Simplified C6 on reading formula in, to give:
     %%%  C6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  loop__1__i >= 0
***  Proved C1:  lengthl >= domainnamestringtypeindex__first
     using hypothesis H1.
***  Proved C2:  lengthl < domainnamestringtypeindex__last
     using hypothesis H2.
***  Proved C3:  lengthl + 1 + lengthr <= maxdomainnamelength
     using hypothesis H3.
***  Proved C4:  lengthr__entry__loop__1 = lengthr
     using hypothesis H4.
***  Proved C5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(update(left, [lengthl + 1 + loop__1__i], 
          element(right, [loop__1__i])), [i___1]) and element(update(left, [
          lengthl + 1 + loop__1__i], element(right, [loop__1__i])), [i___1]) <= 
          character__last)
     using hypotheses H5, H13, H14, H17 & H18.
***  Proved C6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
     using hypothesis H6.
***  Proved C7:  loop__1__i + 1 >= integer__first
     using hypothesis H7.
***  Proved C9:  loop__1__i >= 0
     using hypothesis H9.
***  Proved C11:  lengthr__entry__loop__1 >= domainnamestringtypeindex__first
     using hypothesis H11.
***  Proved C12:  lengthr__entry__loop__1 <= domainnamestringtypeindex__last
     using hypothesis H12.
-S-  Applied substitution rule appenddomain_rules(5).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H8:  loop__1__i <= 2147483647
<S>  New C8:  loop__1__i <= 2147483646
>>>  Restructured hypothesis H23 into:
     >>>  H23:  loop__1__i <> lengthr__entry__loop__1
-S-  Applied substitution rule appenddomain_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H3:  lengthl + 1 + lengthr <= 128
-S-  Applied substitution rule appenddomain_rules(4).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H7:  loop__1__i >= - 2147483648
-S-  Applied substitution rule appenddomain_rules(6).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H19:  lengthl + 1 + loop__1__i >= - 2147483648
<S>  New H21:  lengthl >= - 2147483649
-S-  Applied substitution rule appenddomain_rules(7).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H20:  lengthl + 1 + loop__1__i <= 2147483647
<S>  New H22:  lengthl <= 2147483646
-S-  Applied substitution rule appenddomain_rules(9).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          left, [i___1]) and element(left, [i___1]) <= character__last)
<S>  New H6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= character__last)
<S>  New H13:  element(right, [loop__1__i]) >= 0
-S-  Applied substitution rule appenddomain_rules(10).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H14:  element(right, [loop__1__i]) <= 255
<S>  New H5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(19).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H1:  lengthl >= 1
<S>  New H11:  lengthr__entry__loop__1 >= 1
<S>  New H15:  loop__1__i >= 1
<S>  New H17:  lengthl + 1 + loop__1__i >= 1
<S>  New H5:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(left, [i___1]) and 
          element(left, [i___1]) <= 255)
<S>  New H6:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(right, [i___1]) and 
          element(right, [i___1]) <= 255)
-S-  Applied substitution rule appenddomain_rules(20).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H2:  lengthl < 128
<S>  New H12:  lengthr__entry__loop__1 <= 128
<S>  New H16:  loop__1__i <= 128
<S>  New H18:  lengthl + 1 + loop__1__i <= 128
<S>  New H5:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H6:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(right, [i___1]) and element(right, [i___1]) <= 255)
%%%  Hypotheses H10 & H23 together imply that
          loop__1__i < lengthr__entry__loop__1.
     H10 & H23 have therefore been deleted and a new H24 added to this effect.
***  Proved C10:  loop__1__i + 1 <= lengthr__entry__loop__1
     via its standard form, which is:
     Std.Fm C10:  lengthr__entry__loop__1 - loop__1__i > 0
     using hypothesis H24.
***  Proved C8:  loop__1__i <= 2147483646
     using hypothesis H16.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_appenddomainnames_26.  @@@@@@@@@@
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(left, [i___1]) and element(left, [i___1]) 
          <= character__last)
%%%  Simplified H6 on reading formula in, to give:
     %%%  H6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 
          character__first <= element(right, [i___1]) and element(right, [i___1]
          ) <= character__last)
***  Proved C4:  loop__1__i <= domainnamestringtypeindex__last
     using hypotheses H10 & H12.
***  Proved C5:  lengthl + 1 + loop__1__i >= domainnamestringtypeindex__first
     using hypotheses H1 & H9.
-S-  Applied substitution rule appenddomain_rules(9).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          left, [i___1]) and element(left, [i___1]) <= character__last)
<S>  New H6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= character__last)
<S>  New C1:  element(right, [loop__1__i]) >= 0
-S-  Applied substitution rule appenddomain_rules(10).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H5:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H6:  for_all(i___1 : integer, domainnamestringtypeindex__first <= 
          i___1 and i___1 <= domainnamestringtypeindex__last -> 0 <= element(
          right, [i___1]) and element(right, [i___1]) <= 255)
<S>  New C2:  element(right, [loop__1__i]) <= 255
-S-  Applied substitution rule appenddomain_rules(19).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__first by:
          1.
<S>  New H1:  lengthl >= 1
<S>  New H11:  lengthr__entry__loop__1 >= 1
<S>  New H5:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(left, [i___1]) and 
          element(left, [i___1]) <= 255)
<S>  New H6:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          domainnamestringtypeindex__last -> 0 <= element(right, [i___1]) and 
          element(right, [i___1]) <= 255)
<S>  New C3:  loop__1__i >= 1
-S-  Applied substitution rule appenddomain_rules(20).
     This was achieved by replacing all occurrences of 
          domainnamestringtypeindex__last by:
          128.
<S>  New H2:  lengthl < 128
<S>  New H12:  lengthr__entry__loop__1 <= 128
<S>  New H5:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(left, [i___1]) and element(left, [i___1]) <= 255)
<S>  New H6:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(right, [i___1]) and element(right, [i___1]) <= 255)
<S>  New C6:  lengthl + 1 + loop__1__i <= 128
-S-  Applied substitution rule appenddomain_rules(6).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C7:  lengthl + 1 + loop__1__i >= - 2147483648
<S>  New C9:  lengthl >= - 2147483649
-S-  Applied substitution rule appenddomain_rules(7).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C8:  lengthl + 1 + loop__1__i <= 2147483647
<S>  New C10:  lengthl <= 2147483646
***  Proved C1:  element(right, [loop__1__i]) >= 0
     using hypotheses H6, H9, H10 & H12.
***  Proved C2:  element(right, [loop__1__i]) <= 255
     using hypotheses H6, H9, H10 & H12.
***  Proved C3:  loop__1__i >= 1
     using hypothesis H9.
***  Proved C7:  lengthl + 1 + loop__1__i >= - 2147483648
     using hypotheses H1 & H9.
***  Proved C9:  lengthl >= - 2147483649
     using hypothesis H1.
***  Proved C10:  lengthl <= 2147483646
     using hypothesis H2.
-S-  Applied substitution rule appenddomain_rules(1).
     This was achieved by replacing all occurrences of maxdomainnamelength by:
          128.
<S>  New H3:  lengthl + 1 + lengthr <= 128
-S-  Applied substitution rule appenddomain_rules(4).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H7:  loop__1__i >= - 2147483648
-S-  Applied substitution rule appenddomain_rules(5).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H8:  loop__1__i <= 2147483647
***  Proved C8:  lengthl + 1 + loop__1__i <= 2147483647
     via its standard form, which is:
     Std.Fm C8:  1 + (lengthl + loop__1__i) <= 2147483647
     using hypotheses H2, H10 & H12.
---  Eliminated hypothesis H2 (redundant, given H3, H4 & H11).
---  Eliminated hypothesis H7 (redundant, given H9).
---  Eliminated hypothesis H8 (redundant, given H10 & H12).
---  Eliminated hypothesis H12 (redundant, given H1, H3 & H4).
-S-  Eliminated hypothesis H4.
     This was achieved by replacing all occurrences of lengthr__entry__loop__1 
          by:
          lengthr.
<S>  New H10:  loop__1__i <= lengthr
<S>  New H11:  lengthr >= 1
***  Proved C6:  lengthl + 1 + loop__1__i <= 128
     via its standard form, which is:
     Std.Fm C6:  - lengthl - loop__1__i > - 128
     using hypotheses H3, H4 & H10.
***  PROVED VC.


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


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


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


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


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


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


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


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


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


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


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


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


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

