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

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



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

function Parser_Utilities.isClass






@@@@@@@@@@  VC: function_isclass_1.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
-S-  Applied substitution rule isclass_rules(4).
     This was achieved by replacing all occurrences of integer__base__first by:
          - 2147483648.
<S>  New C1:  endidx >= - 2147483647
-S-  Applied substitution rule isclass_rules(5).
     This was achieved by replacing all occurrences of integer__base__last by:
          2147483647.
<S>  New C2:  endidx <= 2147483648
-S-  Applied substitution rule isclass_rules(7).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [i___1]
          ) and element(s, [i___1]) <= character__last)
-S-  Applied substitution rule isclass_rules(8).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= i___1 
          and i___1 <= rr_type__linelengthindex__last -> 0 <= element(s, [i___1]
          ) and element(s, [i___1]) <= 255)
-S-  Applied substitution rule isclass_rules(17).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H2:  begidx >= 1
<S>  New H4:  endidx >= 1
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(s, [i___1]) and 
          element(s, [i___1]) <= 255)
-S-  Applied substitution rule isclass_rules(18).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H3:  begidx <= 256
<S>  New H5:  endidx <= 256
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(s, [i___1]) and element(s, [i___1]) <= 255)
***  Proved C1:  endidx >= - 2147483647
     using hypothesis H4.
***  Proved C2:  endidx <= 2147483648
     using hypothesis H5.
***  PROVED VC.


@@@@@@@@@@  VC: function_isclass_2.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
***  Proved C1:  element(s, [begidx]) >= character__first
     using hypotheses H1, H2 & H3.
***  Proved C2:  element(s, [begidx]) <= character__last
     using hypotheses H1, H2 & H3.
***  Proved C3:  begidx >= rr_type__linelengthindex__first
     using hypothesis H2.
***  Proved C4:  begidx <= rr_type__linelengthindex__last
     using hypothesis H3.
-S-  Applied substitution rule isclass_rules(22).
     This was achieved by replacing all occurrences of two_range__first by:
          1.
<S>  New C5:  true
-S-  Applied substitution rule isclass_rules(23).
     This was achieved by replacing all occurrences of two_range__last by:
          2.
<S>  New C6:  true
***  Proved C5:  true
***  Proved C6:  true
***  PROVED VC.


@@@@@@@@@@  VC: function_isclass_3.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H3)
          .
***  Proved C1:  ada__characters__handling__to_upper(element(s, [begidx])) >= 
          character__first
     using hypothesis H15.
***  Proved C2:  ada__characters__handling__to_upper(element(s, [begidx])) <= 
          character__last
     using hypothesis H16.
***  PROVED VC.


@@@@@@@@@@  VC: function_isclass_4.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H16).
***  Proved C1:  element(s, [endidx]) >= character__first
     using hypotheses H1, H4 & H5.
***  Proved C2:  element(s, [endidx]) <= character__last
     using hypotheses H1, H4 & H5.
***  Proved C3:  endidx >= rr_type__linelengthindex__first
     using hypothesis H4.
***  Proved C4:  endidx <= rr_type__linelengthindex__last
     using hypothesis H5.
***  Proved C5:  2 >= two_range__first
     using hypothesis H13.
-S-  Applied substitution rule isclass_rules(23).
     This was achieved by replacing all occurrences of two_range__last by:
          2.
<S>  New H14:  true
<S>  New C6:  true
***  Proved C6:  true
***  PROVED VC.


@@@@@@@@@@  VC: function_isclass_5.  @@@@@@@@@@
%%%  Simplified H1 on reading formula in, to give:
     %%%  H1:  for_all(i___1 : integer, rr_type__linelengthindex__first <= 
          i___1 and i___1 <= rr_type__linelengthindex__last -> character__first 
          <= element(s, [i___1]) and element(s, [i___1]) <= character__last)
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H12 has been replaced by "true".  (It is already present, as H3)
          .
---  Hypothesis H17 has been replaced by "true".  (It is already present, as 
          H15).
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H16).
---  Hypothesis H21 has been replaced by "true".  (It is already present, as H4)
          .
---  Hypothesis H22 has been replaced by "true".  (It is already present, as H5)
          .
***  Proved C1:  ada__characters__handling__to_upper(element(s, [endidx])) >= 
          character__first
     using hypothesis H25.
***  Proved C2:  ada__characters__handling__to_upper(element(s, [endidx])) <= 
          character__last
     using hypothesis H26.
***  PROVED VC.


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


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

