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

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



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

function dns_table_pkg.DNS_Table_Type.To_Lower






@@@@@@@@@@  VC: function_to_lower_1.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  rr_type__wirenamelength(domainname) = 
          rr_type__maxdomainnamelength + 1 or element(domainname, [
          rr_type__wirenamelength(domainname)]) = 0 and for_all(q_ : integer, 1 
          <= q_ and q_ <= rr_type__wirenamelength(domainname) - 1 -> element(
          domainname, [q_]) <> 0)
***  Proved C1:  rr_type__wirenamelength(domainname) >= 
          rr_type__wirestringtypeindex__first
     using hypothesis H2.
***  Proved C2:  rr_type__wirenamelength(domainname) <= 
          rr_type__wirestringtypeindex__last
     using hypothesis H3.
***  PROVED VC.


@@@@@@@@@@  VC: function_to_lower_2.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  rr_type__wirenamelength(domainname) = 
          rr_type__maxdomainnamelength + 1 or element(domainname, [
          rr_type__wirenamelength(domainname)]) = 0 and for_all(q_ : integer, 1 
          <= q_ and q_ <= rr_type__wirenamelength(domainname) - 1 -> element(
          domainname, [q_]) <> 0)
---  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 to_lower_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C1:  rr_type__wirenamelength(domainname) >= - 2147483648
<S>  New C3:  true
-S-  Applied substitution rule to_lower_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C2:  rr_type__wirenamelength(domainname) <= 2147483647
<S>  New C4:  true
***  Proved C3:  true
***  Proved C4:  true
-S-  Applied substitution rule to_lower_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H4:  rr_type__wirenamelength(domainname) = 129 or element(domainname, [
          rr_type__wirenamelength(domainname)]) = 0 and for_all(q_ : integer, 1 
          <= q_ and q_ <= rr_type__wirenamelength(domainname) - 1 -> element(
          domainname, [q_]) <> 0)
-S-  Applied substitution rule to_lower_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 
          character__last)
-S-  Applied substitution rule to_lower_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 255)
-S-  Applied substitution rule to_lower_rules(18).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H2:  rr_type__wirenamelength(domainname) >= 1
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(domainname, [i___1]
          ) and element(domainname, [i___1]) <= 255)
-S-  Applied substitution rule to_lower_rules(19).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H3:  rr_type__wirenamelength(domainname) <= 129
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(domainname, [i___1]) and element(domainname, [i___1]) <= 255)
***  Proved C1:  rr_type__wirenamelength(domainname) >= - 2147483648
     using hypothesis H2.
***  Proved C2:  rr_type__wirenamelength(domainname) <= 2147483647
     using hypothesis H3.
***  PROVED VC.


@@@@@@@@@@  VC: function_to_lower_3.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  rr_type__wirenamelength(domainname) = 
          rr_type__maxdomainnamelength + 1 or element(domainname, [
          rr_type__wirenamelength(domainname)]) = 0 and for_all(q_ : integer, 1 
          <= q_ and q_ <= rr_type__wirenamelength(domainname) - 1 -> element(
          domainname, [q_]) <> 0)
---  Hypothesis H5 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H2).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H3).
***  Proved C1:  1 <= rr_type__wirenamelength(domainname) -> 
          rr_type__wirenamelength(domainname) >= integer__first and 
          rr_type__wirenamelength(domainname) <= integer__last
     using hypotheses H9 & H10.
***  Proved C2:  1 <= rr_type__wirenamelength(domainname) -> 1 >= 
          integer__first and 1 <= integer__last
     using hypotheses H11 & H12.
***  PROVED VC.


@@@@@@@@@@  VC: function_to_lower_4.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  rr_type__wirenamelength(domainname) = 
          rr_type__maxdomainnamelength + 1 or element(domainname, [
          rr_type__wirenamelength(domainname)]) = 0 and for_all(q_ : integer, 1 
          <= q_ and q_ <= rr_type__wirenamelength(domainname) - 1 -> element(
          domainname, [q_]) <> 0)
---  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 H15 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H16 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  true
***  Proved C1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first 
          <= i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
     using hypothesis H1.
***  Proved C2:  1 >= integer__first
     using hypothesis H11.
***  Proved C3:  1 <= integer__last
     using hypothesis H12.
***  Proved C4:  true
***  Proved C5:  1 <= rr_type__wirenamelength(domainname)
     using hypothesis H17.
***  Proved C6:  rr_type__wirenamelength(domainname) >= 
          rr_type__wirestringtypeindex__first
     using hypothesis H2.
***  Proved C7:  rr_type__wirenamelength(domainname) <= 
          rr_type__wirestringtypeindex__last
     using hypothesis H3.
***  PROVED VC.


@@@@@@@@@@  VC: function_to_lower_5.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H13 has been replaced by "true".  (It is already present, as 
          H11).
---  Hypothesis H16 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H17 has been replaced by "true".  (It is already present, as 
          H15).
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  loop__1__i >= 0
***  Proved C1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first 
          <= i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
     using hypothesis H1.
***  Proved C2:  loop__1__i + 1 >= integer__first
     using hypothesis H2.
***  Proved C4:  loop__1__i >= 0
     using hypothesis H4.
***  Proved C6:  length__entry__loop__1 >= rr_type__wirestringtypeindex__first
     using hypothesis H6.
***  Proved C7:  length__entry__loop__1 <= rr_type__wirestringtypeindex__last
     using hypothesis H7.
-S-  Applied substitution rule to_lower_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 H18 into:
     >>>  H18:  loop__1__i <> length__entry__loop__1
-S-  Applied substitution rule to_lower_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 to_lower_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 
          character__last)
<S>  New H8:  element(domainname, [loop__1__i]) >= 0
<S>  New H14:  ada__characters__handling__to_lower(element(domainname, [
          loop__1__i])) >= 0
-S-  Applied substitution rule to_lower_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H9:  element(domainname, [loop__1__i]) <= 255
<S>  New H15:  ada__characters__handling__to_lower(element(domainname, [
          loop__1__i])) <= 255
<S>  New H1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 255)
-S-  Applied substitution rule to_lower_rules(18).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H6:  length__entry__loop__1 >= 1
<S>  New H10:  loop__1__i >= 1
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(domainname, [i___1]
          ) and element(domainname, [i___1]) <= 255)
-S-  Applied substitution rule to_lower_rules(19).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H7:  length__entry__loop__1 <= 129
<S>  New H11:  loop__1__i <= 129
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(domainname, [i___1]) and element(domainname, [i___1]) <= 255)
%%%  Hypotheses H5 & H18 together imply that
          loop__1__i < length__entry__loop__1.
     H5 & H18 have therefore been deleted and a new H19 added to this effect.
***  Proved C5:  loop__1__i + 1 <= length__entry__loop__1
     via its standard form, which is:
     Std.Fm C5:  length__entry__loop__1 - loop__1__i > 0
     using hypothesis H19.
***  Proved C3:  loop__1__i <= 2147483646
     using hypothesis H11.
***  PROVED VC.


@@@@@@@@@@  VC: function_to_lower_6.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
***  Proved C4:  loop__1__i <= rr_type__wirestringtypeindex__last
     using hypotheses H5 & H7.
***  Proved C6:  loop__1__i <= rr_type__wirestringtypeindex__last
     using hypotheses H5 & H7.
-S-  Applied substitution rule to_lower_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 
          character__last)
<S>  New C1:  element(domainname, [loop__1__i]) >= 0
-S-  Applied substitution rule to_lower_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          domainname, [i___1]) and element(domainname, [i___1]) <= 255)
<S>  New C2:  element(domainname, [loop__1__i]) <= 255
-S-  Applied substitution rule to_lower_rules(18).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H6:  length__entry__loop__1 >= 1
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(domainname, [i___1]
          ) and element(domainname, [i___1]) <= 255)
<S>  New C3:  loop__1__i >= 1
<S>  New C5:  loop__1__i >= 1
***  Proved C1:  element(domainname, [loop__1__i]) >= 0
     using hypotheses H1, H4, H5 & H7.
***  Proved C2:  element(domainname, [loop__1__i]) <= 255
     using hypotheses H1, H4, H5 & H7.
***  Proved C3:  loop__1__i >= 1
     using hypothesis H4.
***  Proved C5:  loop__1__i >= 1
     using hypothesis H4.
***  PROVED VC.


@@@@@@@@@@  VC: function_to_lower_7.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(domainname, [i___1]) and element(
          domainname, [i___1]) <= character__last)
---  Hypothesis H12 has been replaced by "true".  (It is already present, as 
          H10).
---  Hypothesis H13 has been replaced by "true".  (It is already present, as 
          H11).
***  Proved C1:  ada__characters__handling__to_lower(element(domainname, [
          loop__1__i])) >= character__first
     using hypothesis H14.
***  Proved C2:  ada__characters__handling__to_lower(element(domainname, [
          loop__1__i])) <= character__last
     using hypothesis H15.
***  PROVED VC.


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


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

