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

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



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

procedure Parser_Utilities.checkValidHostName






@@@@@@@@@@  VC: procedure_checkvalidhostname_1.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  rr_type__domainnamelength(name) = 1 and (element(name, [1]) = 32 
          or element(name, [2]) = 32) or (rr_type__domainnamelength(name) = 
          rr_type__maxdomainnamelength or element(name, [
          rr_type__domainnamelength(name) + 1]) = 32 and for_all(q_ : integer, 
          1 <= q_ and q_ <= rr_type__domainnamelength(name) -> element(name, [
          q_]) <> 32))
***  Proved C1:  rr_type__domainnamelength(name) >= 
          rr_type__domainnamestringtypeindex__first
     using hypothesis H2.
***  Proved C2:  rr_type__domainnamelength(name) <= 
          rr_type__domainnamestringtypeindex__last
     using hypothesis H3.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkvalidhostname_2.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  rr_type__domainnamelength(name) = 1 and (element(name, [1]) = 32 
          or element(name, [2]) = 32) or (rr_type__domainnamelength(name) = 
          rr_type__maxdomainnamelength or element(name, [
          rr_type__domainnamelength(name) + 1]) = 32 and for_all(q_ : integer, 
          1 <= q_ and q_ <= rr_type__domainnamelength(name) -> element(name, [
          q_]) <> 32))
---  Hypothesis H5 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H3).
-S-  Applied substitution rule checkvalidho_rules(18).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__first by:
          1.
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
<S>  New H2:  rr_type__domainnamelength(name) >= 1
<S>  New C1:  rr_type__domainnamelength(name) > 1 -> rr_type__domainnamelength(
          name) >= 2 and rr_type__domainnamelength(name) - 1 <= 
          rr_type__domainnamestringtypeindex__last
<S>  New C3:  rr_type__domainnamelength(name) > 1 -> rr_type__domainnamelength(
          name) >= 2 and rr_type__domainnamelength(name) - 1 <= 
          rr_type__domainnamestringtypeindex__last
<S>  New C5:  true
<S>  New C7:  true
-S-  Applied substitution rule checkvalidho_rules(19).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__last by:
          128.
<S>  New H3:  rr_type__domainnamelength(name) <= 128
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 
          character__first <= element(name, [i___1]) and element(name, [i___1]) 
          <= character__last)
<S>  New C6:  true
<S>  New C8:  true
<S>  New C1:  rr_type__domainnamelength(name) > 1 -> rr_type__domainnamelength(
          name) >= 2 and rr_type__domainnamelength(name) <= 129
<S>  New C3:  rr_type__domainnamelength(name) > 1 -> rr_type__domainnamelength(
          name) >= 2 and rr_type__domainnamelength(name) <= 129
***  Proved C5:  true
***  Proved C7:  true
***  Proved C6:  true
***  Proved C8:  true
-S-  Applied substitution rule checkvalidho_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H4:  rr_type__domainnamelength(name) = 1 and (element(name, [1]) = 32 
          or element(name, [2]) = 32) or (rr_type__domainnamelength(name) = 128 
          or element(name, [rr_type__domainnamelength(name) + 1]) = 32 and 
          for_all(q_ : integer, 1 <= q_ and q_ <= rr_type__domainnamelength(
          name) -> element(name, [q_]) <> 32))
-S-  Applied substitution rule checkvalidho_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C2:  rr_type__domainnamelength(name) > 1 -> rr_type__domainnamelength(
          name) >= - 2147483647 and rr_type__domainnamelength(name) - 1 <= 
          integer__base__last
<S>  New C4:  rr_type__domainnamelength(name) > 1 -> rr_type__domainnamelength(
          name) >= - 2147483647 and rr_type__domainnamelength(name) - 1 <= 
          integer__base__last
-S-  Applied substitution rule checkvalidho_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C2:  rr_type__domainnamelength(name) > 1 -> rr_type__domainnamelength(
          name) >= - 2147483647 and rr_type__domainnamelength(name) <= 
          2147483648
<S>  New C4:  rr_type__domainnamelength(name) > 1 -> rr_type__domainnamelength(
          name) >= - 2147483647 and rr_type__domainnamelength(name) <= 
          2147483648
-S-  Applied substitution rule checkvalidho_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
-S-  Applied substitution rule checkvalidho_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(name, [i___1]) and element(name, [i___1]) <= 255)
***  Proved C2:  rr_type__domainnamelength(name) > 1 -> 
          rr_type__domainnamelength(name) >= - 2147483647 and 
          rr_type__domainnamelength(name) <= 2147483648
     using hypotheses H2 & H3.
***  Proved C4:  rr_type__domainnamelength(name) > 1 -> 
          rr_type__domainnamelength(name) >= - 2147483647 and 
          rr_type__domainnamelength(name) <= 2147483648
     using hypotheses H2 & H3.
---  Eliminated hypothesis H5 (true-hypothesis).
---  Eliminated hypothesis H6 (true-hypothesis).
---  Eliminated hypothesis H7 (true-hypothesis).
---  Eliminated hypothesis H8 (true-hypothesis).
---  Eliminated conclusion C3, which is a duplicate of C1.
     +++  New H9:  integer__size >= 0
     +++  New H10:  character__size >= 0
     +++  New H11:  positive__size >= 0
     +++  New H12:  rr_type__domainnamestringtypeindex__size >= 0
>>>  Conclusion C1 is an implication formula [P->Q].
     Attempting to prove this by proving Q while adding P to the hypotheses.
+++  Added new hypotheses (in proving an implication formula).
     +++  New H13:  rr_type__domainnamelength(name) > 1
+++  New subgoal C1:  rr_type__domainnamelength(name) >= 2 and 
          rr_type__domainnamelength(name) <= 129
>>>  Conclusion C1 has now been split into two, giving:
     >>>  C1:  rr_type__domainnamelength(name) >= 2
     >>>  C2:  rr_type__domainnamelength(name) <= 129
***  Proved subgoal C1
     using hypothesis H13.
***  Proved subgoal C2
     using hypothesis H3.
***  Proved C1:  rr_type__domainnamelength(name) > 1 -> 
          rr_type__domainnamelength(name) >= 2 and rr_type__domainnamelength(
          name) <= 129
     by implication.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkvalidhostname_3.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  rr_type__domainnamelength(name) = 1 and (element(name, [1]) = 32 
          or element(name, [2]) = 32) or (rr_type__domainnamelength(name) = 
          rr_type__maxdomainnamelength or element(name, [
          rr_type__domainnamelength(name) + 1]) = 32 and for_all(q_ : integer, 
          1 <= q_ and q_ <= rr_type__domainnamelength(name) -> element(name, [
          q_]) <> 32))
---  Hypothesis H5 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
-S-  Applied substitution rule checkvalidho_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C1:  rr_type__domainnamelength(name) >= - 2147483646
<S>  New C5:  true
-S-  Applied substitution rule checkvalidho_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C2:  rr_type__domainnamelength(name) <= 2147483649
<S>  New C6:  true
-S-  Applied substitution rule checkvalidho_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H10:  rr_type__domainnamelength(name) > 1 -> rr_type__domainnamelength(
          name) >= - 2147483647 and rr_type__domainnamelength(name) - 1 <= 
          integer__base__last
<S>  New C3:  rr_type__domainnamelength(name) >= - 2147483646
-S-  Applied substitution rule checkvalidho_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H10:  rr_type__domainnamelength(name) > 1 -> rr_type__domainnamelength(
          name) >= - 2147483647 and rr_type__domainnamelength(name) <= 
          2147483648
<S>  New C4:  rr_type__domainnamelength(name) <= 2147483649
***  Proved C5:  true
***  Proved C6:  true
>>>  Restructured hypothesis H17 into:
     >>>  H17:  element(name, [1]) <> 46 and (element(name, [1]) <> 45 and (
          rr_type__domainnamelength(name) <= 1 or element(name, [
          rr_type__domainnamelength(name) - 1]) <> 46 and element(name, [
          rr_type__domainnamelength(name) - 1]) <> 45))
>>>  Hypothesis H17 has now been split into two, giving:
     >>>  H20:  element(name, [1]) <> 46
     >>>  H21:  element(name, [1]) <> 45 and (rr_type__domainnamelength(name) 
          <= 1 or element(name, [rr_type__domainnamelength(name) - 1]) <> 46 
          and element(name, [rr_type__domainnamelength(name) - 1]) <> 45)
>>>  Hypothesis H21 has now been split into two, giving:
     >>>  H22:  element(name, [1]) <> 45
     >>>  H23:  rr_type__domainnamelength(name) <= 1 or element(name, [
          rr_type__domainnamelength(name) - 1]) <> 46 and element(name, [
          rr_type__domainnamelength(name) - 1]) <> 45
-S-  Applied substitution rule checkvalidho_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H4:  rr_type__domainnamelength(name) = 1 and (element(name, [1]) = 32 
          or element(name, [2]) = 32) or (rr_type__domainnamelength(name) = 128 
          or element(name, [rr_type__domainnamelength(name) + 1]) = 32 and 
          for_all(q_ : integer, 1 <= q_ and q_ <= rr_type__domainnamelength(
          name) -> element(name, [q_]) <> 32))
-S-  Applied substitution rule checkvalidho_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= character__last)
-S-  Applied substitution rule checkvalidho_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= 255)
-S-  Applied substitution rule checkvalidho_rules(18).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__first by:
          1.
<S>  New H2:  rr_type__domainnamelength(name) >= 1
<S>  New H9:  rr_type__domainnamelength(name) > 1 -> rr_type__domainnamelength(
          name) >= 2 and rr_type__domainnamelength(name) - 1 <= 
          rr_type__domainnamestringtypeindex__last
<S>  New H13:  true
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= 255)
-S-  Applied substitution rule checkvalidho_rules(19).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__last by:
          128.
<S>  New H3:  rr_type__domainnamelength(name) <= 128
<S>  New H14:  true
<S>  New H9:  rr_type__domainnamelength(name) > 1 -> rr_type__domainnamelength(
          name) >= 2 and rr_type__domainnamelength(name) <= 129
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(name, [i___1]) and element(name, [i___1]) <= 255)
***  Proved C1:  rr_type__domainnamelength(name) >= - 2147483646
     using hypothesis H2.
***  Proved C2:  rr_type__domainnamelength(name) <= 2147483649
     using hypothesis H3.
***  Proved C3:  rr_type__domainnamelength(name) >= - 2147483646
     using hypothesis H2.
***  Proved C4:  rr_type__domainnamelength(name) <= 2147483649
     using hypothesis H3.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkvalidhostname_4.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  rr_type__domainnamelength(name) = 1 and (element(name, [1]) = 32 
          or element(name, [2]) = 32) or (rr_type__domainnamelength(name) = 
          rr_type__maxdomainnamelength or element(name, [
          rr_type__domainnamelength(name) + 1]) = 32 and for_all(q_ : integer, 
          1 <= q_ and q_ <= rr_type__domainnamelength(name) -> element(name, [
          q_]) <> 32))
---  Hypothesis H5 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  4 <= rr_type__domainnamelength(name) -> 
          rr_type__domainnamelength(name) - 2 >= integer__first and 
          rr_type__domainnamelength(name) - 2 <= integer__last
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  4 <= rr_type__domainnamelength(name) -> 2 >= integer__first and 
          2 <= integer__last
***  Proved C1:  4 <= rr_type__domainnamelength(name) -> 
          rr_type__domainnamelength(name) - 2 >= integer__first and 
          rr_type__domainnamelength(name) - 2 <= integer__last
     using hypotheses H20 & H21.
***  Proved C2:  4 <= rr_type__domainnamelength(name) -> 2 >= integer__first 
          and 2 <= integer__last
     using hypotheses H24 & H25.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkvalidhostname_5.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  rr_type__domainnamelength(name) = 1 and (element(name, [1]) = 32 
          or element(name, [2]) = 32) or (rr_type__domainnamelength(name) = 
          rr_type__maxdomainnamelength or element(name, [
          rr_type__domainnamelength(name) + 1]) = 32 and for_all(q_ : integer, 
          1 <= q_ and q_ <= rr_type__domainnamelength(name) -> element(name, [
          q_]) <> 32))
---  Hypothesis H5 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H15 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H18 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H19 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified H26 on reading formula in, to give:
     %%%  H26:  4 <= rr_type__domainnamelength(name) -> 
          rr_type__domainnamelength(name) - 2 >= integer__first and 
          rr_type__domainnamelength(name) - 2 <= integer__last
%%%  Simplified H27 on reading formula in, to give:
     %%%  H27:  4 <= rr_type__domainnamelength(name) -> 2 >= integer__first and 
          2 <= integer__last
---  Hypothesis H28 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H29 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified H30 on reading formula in, to give:
     %%%  H30:  4 <= rr_type__domainnamelength(name)
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  true
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  4 <= rr_type__domainnamelength(name)
***  Proved C1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
     using hypothesis H1.
***  Proved C2:  2 >= integer__first
     using hypothesis H24.
***  Proved C3:  2 <= integer__last
     using hypothesis H25.
***  Proved C4:  true
***  Proved C5:  4 <= rr_type__domainnamelength(name)
     using hypothesis H30.
***  Proved C6:  rr_type__domainnamelength(name) >= 
          rr_type__domainnamestringtypeindex__first
     using hypothesis H2.
***  Proved C7:  rr_type__domainnamelength(name) <= 
          rr_type__domainnamestringtypeindex__last
     using hypothesis H3.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkvalidhostname_6.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
---  Hypothesis H15 has been replaced by "true".  (It is already present, as 
          H11).
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H12).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H14).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  loop__1__i >= 1
***  Proved C1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
     using hypothesis H1.
***  Proved C2:  loop__1__i + 1 >= integer__first
     using hypothesis H2.
***  Proved C4:  loop__1__i >= 1
     using hypothesis H4.
***  Proved C6:  length__entry__loop__1 >= 
          rr_type__domainnamestringtypeindex__first
     using hypothesis H6.
***  Proved C7:  length__entry__loop__1 <= 
          rr_type__domainnamestringtypeindex__last
     using hypothesis H7.
-S-  Applied substitution rule checkvalidho_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H3:  loop__1__i <= 2147483647
<S>  New C3:  loop__1__i <= 2147483646
>>>  Restructured hypothesis H20 into:
     >>>  H20:  loop__1__i <> length__entry__loop__1 - 2
-S-  Applied substitution rule checkvalidho_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H2:  loop__1__i >= - 2147483648
-S-  Applied substitution rule checkvalidho_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H13:  loop__1__i >= - 2147483647
-S-  Applied substitution rule checkvalidho_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H14:  loop__1__i <= 2147483648
-S-  Applied substitution rule checkvalidho_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= character__last)
-S-  Applied substitution rule checkvalidho_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= 255)
-S-  Applied substitution rule checkvalidho_rules(18).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__first by:
          1.
<S>  New H6:  length__entry__loop__1 >= 1
<S>  New H8:  loop__1__i >= 1
<S>  New H11:  loop__1__i >= 2
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= 255)
-S-  Applied substitution rule checkvalidho_rules(19).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__last by:
          128.
<S>  New H7:  length__entry__loop__1 <= 128
<S>  New H9:  loop__1__i <= 128
<S>  New H12:  loop__1__i <= 129
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(name, [i___1]) and element(name, [i___1]) <= 255)
%%%  Hypotheses H5 & H20 together imply that
          loop__1__i < length__entry__loop__1 - 2.
     H5 & H20 have therefore been deleted and a new H21 added to this effect.
***  Proved C5:  loop__1__i + 1 <= length__entry__loop__1 - 2
     via its standard form, which is:
     Std.Fm C5:  length__entry__loop__1 - loop__1__i > 2
     using hypothesis H21.
***  Proved C3:  loop__1__i <= 2147483646
     using hypothesis H9.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkvalidhostname_7.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
---  Hypothesis H15 has been replaced by "true".  (It is already present, as 
          H11).
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H12).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H14).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  loop__1__i >= 1
***  Proved C1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
     using hypothesis H1.
***  Proved C2:  loop__1__i + 1 >= integer__first
     using hypothesis H2.
***  Proved C4:  loop__1__i >= 1
     using hypothesis H4.
***  Proved C6:  length__entry__loop__1 >= 
          rr_type__domainnamestringtypeindex__first
     using hypothesis H6.
***  Proved C7:  length__entry__loop__1 <= 
          rr_type__domainnamestringtypeindex__last
     using hypothesis H7.
-S-  Applied substitution rule checkvalidho_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H3:  loop__1__i <= 2147483647
<S>  New C3:  loop__1__i <= 2147483646
>>>  Restructured hypothesis H19 into:
     >>>  H19:  element(name, [loop__1__i - 1]) <> 46 and element(name, [
          loop__1__i - 1]) <> 45
>>>  Restructured hypothesis H20 into:
     >>>  H20:  loop__1__i <> length__entry__loop__1 - 2
>>>  Hypothesis H19 has now been split into two, giving:
     >>>  H21:  element(name, [loop__1__i - 1]) <> 46
     >>>  H22:  element(name, [loop__1__i - 1]) <> 45
-S-  Applied substitution rule checkvalidho_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H2:  loop__1__i >= - 2147483648
-S-  Applied substitution rule checkvalidho_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New H13:  loop__1__i >= - 2147483647
-S-  Applied substitution rule checkvalidho_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New H14:  loop__1__i <= 2147483648
-S-  Applied substitution rule checkvalidho_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= character__last)
-S-  Applied substitution rule checkvalidho_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= 255)
-S-  Applied substitution rule checkvalidho_rules(18).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__first by:
          1.
<S>  New H6:  length__entry__loop__1 >= 1
<S>  New H8:  loop__1__i >= 1
<S>  New H11:  loop__1__i >= 2
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= 255)
-S-  Applied substitution rule checkvalidho_rules(19).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__last by:
          128.
<S>  New H7:  length__entry__loop__1 <= 128
<S>  New H9:  loop__1__i <= 128
<S>  New H12:  loop__1__i <= 129
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(name, [i___1]) and element(name, [i___1]) <= 255)
%%%  Hypotheses H5 & H20 together imply that
          loop__1__i < length__entry__loop__1 - 2.
     H5 & H20 have therefore been deleted and a new H23 added to this effect.
***  Proved C5:  loop__1__i + 1 <= length__entry__loop__1 - 2
     via its standard form, which is:
     Std.Fm C5:  length__entry__loop__1 - loop__1__i > 2
     using hypothesis H23.
***  Proved C3:  loop__1__i <= 2147483646
     using hypothesis H9.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkvalidhostname_8.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H9)
          .
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  loop__1__i >= 1
***  Proved C1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
     using hypothesis H1.
***  Proved C2:  loop__1__i + 1 >= integer__first
     using hypothesis H2.
***  Proved C4:  loop__1__i >= 1
     using hypothesis H4.
***  Proved C6:  length__entry__loop__1 >= 
          rr_type__domainnamestringtypeindex__first
     using hypothesis H6.
***  Proved C7:  length__entry__loop__1 <= 
          rr_type__domainnamestringtypeindex__last
     using hypothesis H7.
-S-  Applied substitution rule checkvalidho_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H3:  loop__1__i <= 2147483647
<S>  New C3:  loop__1__i <= 2147483646
>>>  Restructured hypothesis H10 into:
     >>>  H10:  element(name, [loop__1__i]) <> 46
>>>  Restructured hypothesis H20 into:
     >>>  H20:  loop__1__i <> length__entry__loop__1 - 2
-S-  Applied substitution rule checkvalidho_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H2:  loop__1__i >= - 2147483648
-S-  Applied substitution rule checkvalidho_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= character__last)
<S>  New H11:  element(name, [loop__1__i]) >= 0
-S-  Applied substitution rule checkvalidho_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H12:  element(name, [loop__1__i]) <= 255
<S>  New H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= 255)
-S-  Applied substitution rule checkvalidho_rules(18).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__first by:
          1.
<S>  New H6:  length__entry__loop__1 >= 1
<S>  New H8:  loop__1__i >= 1
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= 255)
-S-  Applied substitution rule checkvalidho_rules(19).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__last by:
          128.
<S>  New H7:  length__entry__loop__1 <= 128
<S>  New H9:  loop__1__i <= 128
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(name, [i___1]) and element(name, [i___1]) <= 255)
%%%  Hypotheses H5 & H20 together imply that
          loop__1__i < length__entry__loop__1 - 2.
     H5 & H20 have therefore been deleted and a new H21 added to this effect.
***  Proved C5:  loop__1__i + 1 <= length__entry__loop__1 - 2
     via its standard form, which is:
     Std.Fm C5:  length__entry__loop__1 - loop__1__i > 2
     using hypothesis H21.
***  Proved C3:  loop__1__i <= 2147483646
     using hypothesis H9.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkvalidhostname_9.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H9)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as H9)
          .
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  loop__1__i >= 1
***  Proved C1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
     using hypothesis H1.
***  Proved C2:  loop__1__i + 1 >= integer__first
     using hypothesis H2.
***  Proved C4:  loop__1__i >= 1
     using hypothesis H4.
***  Proved C6:  length__entry__loop__1 >= 
          rr_type__domainnamestringtypeindex__first
     using hypothesis H6.
***  Proved C7:  length__entry__loop__1 <= 
          rr_type__domainnamestringtypeindex__last
     using hypothesis H7.
-S-  Applied substitution rule checkvalidho_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H3:  loop__1__i <= 2147483647
<S>  New C3:  loop__1__i <= 2147483646
>>>  Restructured hypothesis H10 into:
     >>>  H10:  element(name, [loop__1__i]) <> 46
>>>  Restructured hypothesis H18 into:
     >>>  H18:  ada__characters__handling__is_alphanumeric(element(name, [
          loop__1__i])) or element(name, [loop__1__i]) = 45
>>>  Restructured hypothesis H19 into:
     >>>  H19:  loop__1__i <> length__entry__loop__1 - 2
-S-  Applied substitution rule checkvalidho_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H2:  loop__1__i >= - 2147483648
-S-  Applied substitution rule checkvalidho_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= character__last)
<S>  New H11:  element(name, [loop__1__i]) >= 0
-S-  Applied substitution rule checkvalidho_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H12:  element(name, [loop__1__i]) <= 255
<S>  New H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= 255)
-S-  Applied substitution rule checkvalidho_rules(18).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__first by:
          1.
<S>  New H6:  length__entry__loop__1 >= 1
<S>  New H8:  loop__1__i >= 1
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= 255)
-S-  Applied substitution rule checkvalidho_rules(19).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__last by:
          128.
<S>  New H7:  length__entry__loop__1 <= 128
<S>  New H9:  loop__1__i <= 128
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(name, [i___1]) and element(name, [i___1]) <= 255)
%%%  Hypotheses H5 & H19 together imply that
          loop__1__i < length__entry__loop__1 - 2.
     H5 & H19 have therefore been deleted and a new H20 added to this effect.
***  Proved C5:  loop__1__i + 1 <= length__entry__loop__1 - 2
     via its standard form, which is:
     Std.Fm C5:  length__entry__loop__1 - loop__1__i > 2
     using hypothesis H20.
***  Proved C3:  loop__1__i <= 2147483646
     using hypothesis H9.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkvalidhostname_10.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
***  Proved C2:  loop__1__i <= rr_type__domainnamestringtypeindex__last
     using hypotheses H5 & H7.
-S-  Applied substitution rule checkvalidho_rules(18).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__first by:
          1.
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
<S>  New H6:  length__entry__loop__1 >= 1
<S>  New C1:  loop__1__i >= 1
***  Proved C1:  loop__1__i >= 1
     using hypothesis H4.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkvalidhostname_11.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
***  Proved C2:  loop__1__i - 1 <= rr_type__domainnamestringtypeindex__last
     using hypothesis H9.
***  Proved C6:  loop__1__i - 1 <= rr_type__domainnamestringtypeindex__last
     using hypothesis H9.
-S-  Applied substitution rule checkvalidho_rules(18).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__first by:
          1.
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
<S>  New H6:  length__entry__loop__1 >= 1
<S>  New H8:  loop__1__i >= 1
<S>  New C1:  loop__1__i >= 2
<S>  New C5:  loop__1__i >= 2
-S-  Applied substitution rule checkvalidho_rules(5).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C3:  loop__1__i >= - 2147483647
<S>  New C7:  loop__1__i >= - 2147483647
-S-  Applied substitution rule checkvalidho_rules(6).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C4:  loop__1__i <= 2147483648
<S>  New C8:  loop__1__i <= 2147483648
***  Proved C1:  loop__1__i >= 2
     using hypothesis H4.
***  Proved C5:  loop__1__i >= 2
     using hypothesis H4.
***  Proved C3:  loop__1__i >= - 2147483647
     using hypothesis H4.
***  Proved C7:  loop__1__i >= - 2147483647
     using hypothesis H4.
-S-  Applied substitution rule checkvalidho_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H2:  loop__1__i >= - 2147483648
-S-  Applied substitution rule checkvalidho_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H3:  loop__1__i <= 2147483647
-S-  Applied substitution rule checkvalidho_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= character__last)
-S-  Applied substitution rule checkvalidho_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> 0 <= element(name, [i___1]
          ) and element(name, [i___1]) <= 255)
-S-  Applied substitution rule checkvalidho_rules(19).
     This was achieved by replacing all occurrences of 
          rr_type__domainnamestringtypeindex__last by:
          128.
<S>  New H7:  length__entry__loop__1 <= 128
<S>  New H9:  loop__1__i <= 128
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 128 -> 0 <= 
          element(name, [i___1]) and element(name, [i___1]) <= 255)
***  Proved C4:  loop__1__i <= 2147483648
     using hypothesis H3.
***  Proved C8:  loop__1__i <= 2147483648
     using hypothesis H3.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkvalidhostname_12.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
***  Proved C1:  element(name, [loop__1__i]) >= character__first
     using hypotheses H1, H8 & H9.
***  Proved C2:  element(name, [loop__1__i]) <= character__last
     using hypotheses H1, H8 & H9.
***  Proved C3:  loop__1__i >= rr_type__domainnamestringtypeindex__first
     using hypothesis H8.
***  Proved C4:  loop__1__i <= rr_type__domainnamestringtypeindex__last
     using hypothesis H9.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_checkvalidhostname_13.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, 
          rr_type__domainnamestringtypeindex__first <= i___1 and i___1 <= 
          rr_type__domainnamestringtypeindex__last -> character__first <= 
          element(name, [i___1]) and element(name, [i___1]) <= character__last)
---  Hypothesis H13 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H14 has been replaced by "true".  (It is already present, as H9)
          .
***  Proved C1:  loop__1__i >= rr_type__domainnamestringtypeindex__first
     using hypothesis H8.
***  Proved C2:  loop__1__i <= rr_type__domainnamestringtypeindex__last
     using hypothesis H9.
***  PROVED VC.


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


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


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


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


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


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

