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

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



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

procedure Zone_File_Parser.ParseTimeSpec






@@@@@@@@@@  VC: procedure_parsetimespec_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(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
-S-  Applied substitution rule parsetimespe_rules(17).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule parsetimespe_rules(18).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsetimespec_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(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
***  Proved C1:  1 >= rr_type__linelengthindex__first
     using hypothesis H6.
***  Proved C2:  1 <= rr_type__linelengthindex__last
     using hypothesis H7.
***  Proved C3:  zlength >= rr_type__linelengthindex__first
     using hypothesis H2.
***  Proved C4:  zlength <= rr_type__linelengthindex__last
     using hypothesis H3.
-S-  Applied substitution rule parsetimespe_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(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
-S-  Applied substitution rule parsetimespe_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(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsetimespe_rules(17).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H4:  true
-S-  Applied substitution rule parsetimespe_rules(18).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H5:  true
-S-  Applied substitution rule parsetimespe_rules(64).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H2:  zlength >= 1
<S>  New H6:  true
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> 0 <= element(zonefileline, [i___1]) 
          and element(zonefileline, [i___1]) <= 255)
-S-  Applied substitution rule parsetimespe_rules(65).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H3:  zlength <= 256
<S>  New H7:  true
<S>  New H1:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C5:  1 <= zlength
     using hypothesis H2.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsetimespec_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(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H6).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H7).
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified H16 on reading formula in, to give:
     %%%  H16:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  rr_type__rritemtype__first <= foundtype__1
%%%  Simplified C1 on reading formula in, to give:
     %%%  C1:  rr_type__rritemtype__first <= foundtype__1
***  Proved C1:  rr_type__rritemtype__first <= foundtype__1
     using hypothesis H21.
***  Proved C2:  foundtype__1 <= rr_type__rritemtype__last
     using hypothesis H22.
***  Proved C3:  endidx__1 >= rr_type__linelengthindex__first
     using hypothesis H19.
***  Proved C4:  endidx__1 <= rr_type__linelengthindex__last
     using hypothesis H20.
***  Proved C5:  begidx__1 >= rr_type__linelengthindex__first
     using hypothesis H17.
***  Proved C6:  begidx__1 <= rr_type__linelengthindex__last
     using hypothesis H18.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsetimespec_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(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H6).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H7).
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified H16 on reading formula in, to give:
     %%%  H16:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  rr_type__rritemtype__first <= foundtype__1
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H20).
***  Proved C1:  endidx__1 >= rr_type__linelengthindex__first
     using hypothesis H19.
***  Proved C2:  endidx__1 <= rr_type__linelengthindex__last
     using hypothesis H20.
***  Proved C3:  begidx__1 >= rr_type__linelengthindex__first
     using hypothesis H17.
***  Proved C4:  begidx__1 <= rr_type__linelengthindex__last
     using hypothesis H18.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parsetimespec_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(zonefileline, [i___1]) and element(zonefileline, [i___1]) 
          <= character__last)
---  Hypothesis H8 has been replaced by "true".  (It is already present, as H6).
---  Hypothesis H9 has been replaced by "true".  (It is already present, as H7).
---  Hypothesis H10 has been replaced by "true".  (It is already present, as H2)
          .
---  Hypothesis H11 has been replaced by "true".  (It is already present, as H3)
          .
%%%  Simplified H16 on reading formula in, to give:
     %%%  H16:  foundtype__1 = rr_type__number -> for_all(i_ : integer, 
          begidx__1 <= i_ and i_ <= endidx__1 -> 48 <= element(zonefileline, [
          i_]) and element(zonefileline, [i_]) <= 57)
%%%  Simplified H21 on reading formula in, to give:
     %%%  H21:  rr_type__rritemtype__first <= foundtype__1
---  Hypothesis H23 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H24 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H25 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H26 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H29 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H36 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H37 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H38 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H39 has been replaced by "true".  (It is already present, as 
          H18).
***  Proved C1:  newtimespec__2 >= unsigned_types__unsigned32__first
     using hypothesis H40.
***  Proved C2:  newtimespec__2 <= unsigned_types__unsigned32__last
     using hypothesis H41.
***  PROVED VC.


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


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

