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

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



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

function Process_Dns_Request.Lookup






@@@@@@@@@@  VC: function_lookup_1.  @@@@@@@@@@
-S-  Applied substitution rule lookup_rules(8).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New C1:  (arg - 65) mod dns_types__byte__modulus >= 0
-S-  Applied substitution rule lookup_rules(9).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New C2:  (arg - 65) mod dns_types__byte__modulus <= 255
-S-  Applied substitution rule lookup_rules(2).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  arg >= 0
-S-  Applied substitution rule lookup_rules(3).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H2:  arg <= 255
-S-  Applied substitution rule lookup_rules(12).
     This was achieved by replacing all occurrences of dns_types__byte__modulus 
          by:
          256.
<S>  New C1:  (arg - 65) mod 256 >= 0
<S>  New C2:  (arg - 65) mod 256 <= 255
***  Proved C1:  (arg - 65) mod 256 >= 0
***  Proved C2:  (arg - 65) mod 256 <= 255
***  PROVED VC.


@@@@@@@@@@  VC: function_lookup_2.  @@@@@@@@@@
-S-  Applied substitution rule lookup_rules(8).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New C1:  ((arg - 97) mod dns_types__byte__modulus + 26) mod 
          dns_types__byte__modulus >= 0
-S-  Applied substitution rule lookup_rules(9).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New C2:  ((arg - 97) mod dns_types__byte__modulus + 26) mod 
          dns_types__byte__modulus <= 255
-S-  Applied substitution rule lookup_rules(2).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  arg >= 0
-S-  Applied substitution rule lookup_rules(3).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H2:  arg <= 255
-S-  Applied substitution rule lookup_rules(12).
     This was achieved by replacing all occurrences of dns_types__byte__modulus 
          by:
          256.
<S>  New C1:  ((arg - 97) mod 256 + 26) mod 256 >= 0
<S>  New C2:  ((arg - 97) mod 256 + 26) mod 256 <= 255
***  Proved C1:  ((arg - 97) mod 256 + 26) mod 256 >= 0
***  Proved C2:  ((arg - 97) mod 256 + 26) mod 256 <= 255
***  PROVED VC.


@@@@@@@@@@  VC: function_lookup_3.  @@@@@@@@@@
-S-  Applied substitution rule lookup_rules(8).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New C1:  ((arg - 48) mod dns_types__byte__modulus + 52) mod 
          dns_types__byte__modulus >= 0
-S-  Applied substitution rule lookup_rules(9).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New C2:  ((arg - 48) mod dns_types__byte__modulus + 52) mod 
          dns_types__byte__modulus <= 255
-S-  Applied substitution rule lookup_rules(2).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  arg >= 0
-S-  Applied substitution rule lookup_rules(3).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H2:  arg <= 255
-S-  Applied substitution rule lookup_rules(12).
     This was achieved by replacing all occurrences of dns_types__byte__modulus 
          by:
          256.
<S>  New C1:  ((arg - 48) mod 256 + 52) mod 256 >= 0
<S>  New C2:  ((arg - 48) mod 256 + 52) mod 256 <= 255
***  Proved C1:  ((arg - 48) mod 256 + 52) mod 256 >= 0
***  Proved C2:  ((arg - 48) mod 256 + 52) mod 256 <= 255
***  PROVED VC.


@@@@@@@@@@  VC: function_lookup_4.  @@@@@@@@@@
-S-  Applied substitution rule lookup_rules(8).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule lookup_rules(9).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: function_lookup_5.  @@@@@@@@@@
-S-  Applied substitution rule lookup_rules(8).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule lookup_rules(9).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: function_lookup_6.  @@@@@@@@@@
-S-  Applied substitution rule lookup_rules(8).
     This was achieved by replacing all occurrences of dns_types__byte__first 
          by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule lookup_rules(9).
     This was achieved by replacing all occurrences of dns_types__byte__last by:
          255.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: function_lookup_7.  @@@@@@@@@@
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H6).
***  Proved C1:  (arg - 65) mod dns_types__byte__modulus >= 
          dns_types__byte__first
     using hypothesis H5.
***  Proved C2:  (arg - 65) mod dns_types__byte__modulus <= 
          dns_types__byte__last
     using hypothesis H6.
***  PROVED VC.


@@@@@@@@@@  VC: function_lookup_8.  @@@@@@@@@@
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H6).
***  Proved C1:  ((arg - 97) mod dns_types__byte__modulus + 26) mod 
          dns_types__byte__modulus >= dns_types__byte__first
     using hypothesis H5.
***  Proved C2:  ((arg - 97) mod dns_types__byte__modulus + 26) mod 
          dns_types__byte__modulus <= dns_types__byte__last
     using hypothesis H6.
***  PROVED VC.


@@@@@@@@@@  VC: function_lookup_9.  @@@@@@@@@@
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H6).
***  Proved C1:  ((arg - 48) mod dns_types__byte__modulus + 52) mod 
          dns_types__byte__modulus >= dns_types__byte__first
     using hypothesis H5.
***  Proved C2:  ((arg - 48) mod dns_types__byte__modulus + 52) mod 
          dns_types__byte__modulus <= dns_types__byte__last
     using hypothesis H6.
***  PROVED VC.


@@@@@@@@@@  VC: function_lookup_10.  @@@@@@@@@@
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H4).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
***  Proved C1:  62 >= dns_types__byte__first
     using hypothesis H4.
***  Proved C2:  62 <= dns_types__byte__last
     using hypothesis H5.
***  PROVED VC.


@@@@@@@@@@  VC: function_lookup_11.  @@@@@@@@@@
---  Hypothesis H6 has been replaced by "true".  (It is already present, as H4).
---  Hypothesis H7 has been replaced by "true".  (It is already present, as H5).
***  Proved C1:  63 >= dns_types__byte__first
     using hypothesis H4.
***  Proved C2:  63 <= dns_types__byte__last
     using hypothesis H5.
***  PROVED VC.


@@@@@@@@@@  VC: function_lookup_12.  @@@@@@@@@@
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H8)
          .
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H9)
          .
***  Proved C1:  0 >= dns_types__byte__first
     using hypothesis H8.
***  Proved C2:  0 <= dns_types__byte__last
     using hypothesis H9.
***  PROVED VC.

