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

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



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

function Parser_Utilities.IsMult






@@@@@@@@@@  VC: function_ismult_1.  @@@@@@@@@@
***  Proved C1:  char >= character__first
     using hypothesis H1.
***  Proved C2:  char <= character__last
     using hypothesis H2.
***  PROVED VC.


@@@@@@@@@@  VC: function_ismult_2.  @@@@@@@@@@
---  Hypothesis H3 has been replaced by "true".  (It is already present, as H1).
---  Hypothesis H4 has been replaced by "true".  (It is already present, as H2).
***  Proved C1:  ada__characters__handling__to_upper(char) >= character__first
     using hypothesis H5.
***  Proved C2:  ada__characters__handling__to_upper(char) <= character__last
     using hypothesis H6.
***  PROVED VC.


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


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

