*****************************************************************************
                       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.Same






@@@@@@@@@@  VC: function_same_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(x, [i___1]) and element(x, [i___1]) <= 
          character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(y, [i___1]) and element(y, [i___1]) <= 
          character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  rr_type__wirenamelength(x) = rr_type__maxdomainnamelength + 1 or 
          element(x, [rr_type__wirenamelength(x)]) = 0 and for_all(q_ : 
          integer, 1 <= q_ and q_ <= rr_type__wirenamelength(x) - 1 -> element(
          x, [q_]) <> 0)
***  Proved C1:  rr_type__wirenamelength(x) >= 
          rr_type__wirestringtypeindex__first
     using hypothesis H3.
***  Proved C2:  rr_type__wirenamelength(x) <= 
          rr_type__wirestringtypeindex__last
     using hypothesis H4.
***  PROVED VC.


@@@@@@@@@@  VC: function_same_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(x, [i___1]) and element(x, [i___1]) <= 
          character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(y, [i___1]) and element(y, [i___1]) <= 
          character__last)
%%%  Simplified H5 on reading formula in, to give:
     %%%  H5:  rr_type__wirenamelength(x) = rr_type__maxdomainnamelength + 1 or 
          element(x, [rr_type__wirenamelength(x)]) = 0 and for_all(q_ : 
          integer, 1 <= q_ and q_ <= rr_type__wirenamelength(x) - 1 -> element(
          x, [q_]) <> 0)
---  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).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H3).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H4).
-S-  Applied substitution rule same_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C1:  rr_type__wirenamelength(x) >= - 2147483648
<S>  New C3:  true
-S-  Applied substitution rule same_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C2:  rr_type__wirenamelength(x) <= 2147483647
<S>  New C4:  true
***  Proved C3:  true
***  Proved C4:  true
-S-  Applied substitution rule same_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__maxdomainnamelength by:
          128.
<S>  New H5:  rr_type__wirenamelength(x) = 129 or element(x, [
          rr_type__wirenamelength(x)]) = 0 and for_all(q_ : integer, 1 <= q_ 
          and q_ <= rr_type__wirenamelength(x) - 1 -> element(x, [q_]) <> 0)
-S-  Applied substitution rule same_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(
          x, [i___1]) and element(x, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          y, [i___1]) and element(y, [i___1]) <= character__last)
-S-  Applied substitution rule same_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(
          x, [i___1]) and element(x, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          y, [i___1]) and element(y, [i___1]) <= 255)
-S-  Applied substitution rule same_rules(18).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H3:  rr_type__wirenamelength(x) >= 1
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(x, [i___1]) and 
          element(x, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(y, [i___1]) and 
          element(y, [i___1]) <= 255)
-S-  Applied substitution rule same_rules(19).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H4:  rr_type__wirenamelength(x) <= 129
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(x, [i___1]) and element(x, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(y, [i___1]) and element(y, [i___1]) <= 255)
***  Proved C1:  rr_type__wirenamelength(x) >= - 2147483648
     using hypothesis H3.
***  Proved C2:  rr_type__wirenamelength(x) <= 2147483647
     using hypothesis H4.
***  PROVED VC.


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


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


@@@@@@@@@@  VC: function_same_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(x, [i___1]) and element(x, [i___1]) <= 
          character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(y, [i___1]) and element(y, [i___1]) <= 
          character__last)
---  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).
%%%  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(x, [i___1]) and element(x, [i___1]) <= 
          character__last)
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(y, [i___1]) and element(y, [i___1]) <= 
          character__last)
%%%  Simplified C5 on reading formula in, to give:
     %%%  C5:  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(x, [i___1]) and element(x, [i___1]) <= 
          character__last)
     using hypothesis H1.
***  Proved C2:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first 
          <= i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(y, [i___1]) and element(y, [i___1]) <= 
          character__last)
     using hypothesis H2.
***  Proved C3:  loop__1__i + 1 >= integer__first
     using hypothesis H3.
***  Proved C5:  loop__1__i >= 0
     using hypothesis H5.
***  Proved C7:  length__entry__loop__1 >= rr_type__wirestringtypeindex__first
     using hypothesis H7.
***  Proved C8:  length__entry__loop__1 <= rr_type__wirestringtypeindex__last
     using hypothesis H8.
-S-  Applied substitution rule same_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H4:  loop__1__i <= 2147483647
<S>  New C4:  loop__1__i <= 2147483646
>>>  Restructured hypothesis H13 into:
     >>>  H13:  element(x, [loop__1__i]) = element(y, [loop__1__i])
>>>  Restructured hypothesis H14 into:
     >>>  H14:  loop__1__i <> length__entry__loop__1
-S-  Applied substitution rule same_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H3:  loop__1__i >= - 2147483648
-S-  Applied substitution rule same_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(
          x, [i___1]) and element(x, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          y, [i___1]) and element(y, [i___1]) <= character__last)
-S-  Applied substitution rule same_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(
          x, [i___1]) and element(x, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 0 <= element(
          y, [i___1]) and element(y, [i___1]) <= 255)
-S-  Applied substitution rule same_rules(18).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H7:  length__entry__loop__1 >= 1
<S>  New H9:  loop__1__i >= 1
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(x, [i___1]) and 
          element(x, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> 0 <= element(y, [i___1]) and 
          element(y, [i___1]) <= 255)
-S-  Applied substitution rule same_rules(19).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__last by:
          129.
<S>  New H8:  length__entry__loop__1 <= 129
<S>  New H10:  loop__1__i <= 129
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(x, [i___1]) and element(x, [i___1]) <= 255)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 129 -> 0 <= 
          element(y, [i___1]) and element(y, [i___1]) <= 255)
%%%  Hypotheses H6 & H14 together imply that
          loop__1__i < length__entry__loop__1.
     H6 & H14 have therefore been deleted and a new H15 added to this effect.
***  Proved C6:  loop__1__i + 1 <= length__entry__loop__1
     via its standard form, which is:
     Std.Fm C6:  length__entry__loop__1 - loop__1__i > 0
     using hypothesis H15.
***  Proved C4:  loop__1__i <= 2147483646
     using hypothesis H10.
***  PROVED VC.


@@@@@@@@@@  VC: function_same_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(x, [i___1]) and element(x, [i___1]) <= 
          character__last)
%%%  Simplified H2 on reading formula in, to give:
     %%%  H2:  for_all(i___1 : integer, rr_type__wirestringtypeindex__first <= 
          i___1 and i___1 <= rr_type__wirestringtypeindex__last -> 
          character__first <= element(y, [i___1]) and element(y, [i___1]) <= 
          character__last)
***  Proved C2:  loop__1__i <= rr_type__wirestringtypeindex__last
     using hypotheses H6 & H8.
***  Proved C4:  loop__1__i <= rr_type__wirestringtypeindex__last
     using hypotheses H6 & H8.
-S-  Applied substitution rule same_rules(18).
     This was achieved by replacing all occurrences of 
          rr_type__wirestringtypeindex__first by:
          1.
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> character__first <= element(x, [
          i___1]) and element(x, [i___1]) <= character__last)
<S>  New H2:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__wirestringtypeindex__last -> character__first <= element(y, [
          i___1]) and element(y, [i___1]) <= character__last)
<S>  New H7:  length__entry__loop__1 >= 1
<S>  New C1:  loop__1__i >= 1
<S>  New C3:  loop__1__i >= 1
***  Proved C1:  loop__1__i >= 1
     using hypothesis H5.
***  Proved C3:  loop__1__i >= 1
     using hypothesis H5.
***  PROVED VC.


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


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


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

