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






@@@@@@@@@@  VC: procedure_parseserialnumber_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 parseserialn_rules(23).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  true
-S-  Applied substitution rule parseserialn_rules(24).
     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_parseserialnumber_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 parseserialn_rules(8).
     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 parseserialn_rules(9).
     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 parseserialn_rules(23).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H4:  true
-S-  Applied substitution rule parseserialn_rules(24).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H5:  true
-S-  Applied substitution rule parseserialn_rules(70).
     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 parseserialn_rules(71).
     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_parseserialnumber_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_parseserialnumber_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).
-S-  Applied substitution rule parseserialn_rules(18).
     This was achieved by replacing all occurrences of long_long_integer__first 
          by:
          - 9223372036854775808.
<S>  New C1:  true
-S-  Applied substitution rule parseserialn_rules(19).
     This was achieved by replacing all occurrences of long_long_integer__last 
          by:
          9223372036854775807.
<S>  New C2:  true
***  Proved C1:  true
***  Proved C2:  true
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parseserialnumber_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 H34 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H18).
---  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).
-S-  Applied substitution rule parseserialn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New C1:  endidx__1 >= - 2147483648
<S>  New C3:  begidx__1 >= - 2147483648
-S-  Applied substitution rule parseserialn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New C2:  endidx__1 <= 2147483647
<S>  New C4:  begidx__1 <= 2147483647
>>>  Restructured hypothesis H31 into:
     >>>  H31:  foundtype__1 = rr_type__number
+++  Using "A->B, A |- B" on hypotheses H16 & H31 yields a new hypothesis:
     +++  H38:  for_all(i_ : integer, begidx__1 <= i_ and i_ <= endidx__1 -> 48 
          <= element(zonefileline, [i_]) and element(zonefileline, [i_]) <= 57)
-S-  Applied substitution rule parseserialn_rules(8).
     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 parseserialn_rules(9).
     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 parseserialn_rules(18).
     This was achieved by replacing all occurrences of long_long_integer__first 
          by:
          - 9223372036854775808.
<S>  New H32:  true
-S-  Applied substitution rule parseserialn_rules(19).
     This was achieved by replacing all occurrences of long_long_integer__last 
          by:
          9223372036854775807.
<S>  New H33:  true
-S-  Applied substitution rule parseserialn_rules(23).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H4:  true
-S-  Applied substitution rule parseserialn_rules(24).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H5:  true
-S-  Applied substitution rule parseserialn_rules(29).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__first by:
          rr_type__domainnameortimespec.
<S>  New H21:  rr_type__domainnameortimespec <= foundtype__1
-S-  Applied substitution rule parseserialn_rules(30).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__last by:
          rr_type__other.
<S>  New H22:  foundtype__1 <= rr_type__other
-S-  Applied substitution rule parseserialn_rules(70).
     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 H17:  begidx__1 >= 1
<S>  New H19:  endidx__1 >= 1
<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 parseserialn_rules(71).
     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 H18:  begidx__1 <= 256
<S>  New H20:  endidx__1 <= 256
<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 C1:  endidx__1 >= - 2147483648
     using hypothesis H19.
***  Proved C3:  begidx__1 >= - 2147483648
     using hypothesis H17.
***  Proved C2:  endidx__1 <= 2147483647
     using hypothesis H20.
***  Proved C4:  begidx__1 <= 2147483647
     using hypothesis H18.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parseserialnumber_6.  @@@@@@@@@@
%%%  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 H34 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H18).
---  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).
***  Proved C1:  begidx__1 <= endidx__1 -> endidx__1 >= integer__first and 
          endidx__1 <= integer__last
     using hypotheses H38 & H39.
***  Proved C2:  begidx__1 <= endidx__1 -> begidx__1 >= integer__first and 
          begidx__1 <= integer__last
     using hypotheses H40 & H41.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parseserialnumber_7.  @@@@@@@@@@
%%%  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 H34 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H18).
---  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 H44 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H48 has been replaced by "true".  (It is already present, as 
          H13).
%%%  Simplified C2 on reading formula in, to give:
     %%%  C2:  true
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  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)
%%%  Simplified C9 on reading formula in, to give:
     %%%  C9:  true
***  Proved C2:  true
***  Proved C4:  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)
     using hypothesis H1.
***  Proved C5:  zlength >= rr_type__linelengthindex__first
     using hypothesis H2.
***  Proved C6:  zlength <= rr_type__linelengthindex__last
     using hypothesis H3.
***  Proved C7:  begidx__1 >= integer__first
     using hypothesis H40.
***  Proved C8:  begidx__1 <= integer__last
     using hypothesis H41.
***  Proved C9:  true
***  Proved C10:  begidx__1 <= endidx__1
     using hypothesis H13.
***  Proved C11:  endidx__1 >= rr_type__linelengthindex__first
     using hypothesis H19.
***  Proved C12:  endidx__1 <= rr_type__linelengthindex__last
     using hypothesis H20.
-S-  Applied substitution rule parseserialn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__soa_record_type__max_serial_val by:
          4294967295.
<S>  New C3:  true
***  Proved C3:  true
>>>  Restructured hypothesis H31 into:
     >>>  H31:  foundtype__1 = rr_type__number
+++  Using "A->B, A |- B" on hypotheses H16 & H31 yields a new hypothesis:
     +++  H49:  for_all(i_ : integer, begidx__1 <= i_ and i_ <= endidx__1 -> 48 
          <= element(zonefileline, [i_]) and element(zonefileline, [i_]) <= 57)
+++  Using "A->B, A |- B" on hypotheses H42 & H13 yields a new hypothesis:
     +++  H50:  endidx__1 >= integer__first and endidx__1 <= integer__last
+++  Using "A->B, A |- B" on hypotheses H43 & H13 yields a new hypothesis:
     +++  H51:  begidx__1 >= integer__first and begidx__1 <= integer__last
-S-  Applied substitution rule parseserialn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H38:  endidx__1 >= - 2147483648
<S>  New H40:  begidx__1 >= - 2147483648
<S>  New H42:  begidx__1 <= endidx__1 -> endidx__1 >= - 2147483648 and 
          endidx__1 <= integer__last
<S>  New H43:  begidx__1 <= endidx__1 -> begidx__1 >= - 2147483648 and 
          begidx__1 <= integer__last
<S>  New H50:  endidx__1 >= - 2147483648 and endidx__1 <= integer__last
<S>  New H51:  begidx__1 >= - 2147483648 and begidx__1 <= integer__last
-S-  Applied substitution rule parseserialn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H39:  endidx__1 <= 2147483647
<S>  New H41:  begidx__1 <= 2147483647
<S>  New H42:  begidx__1 <= endidx__1 -> endidx__1 >= - 2147483648 and 
          endidx__1 <= 2147483647
<S>  New H43:  begidx__1 <= endidx__1 -> begidx__1 >= - 2147483648 and 
          begidx__1 <= 2147483647
<S>  New H50:  endidx__1 >= - 2147483648 and endidx__1 <= 2147483647
<S>  New H51:  begidx__1 >= - 2147483648 and begidx__1 <= 2147483647
-S-  Applied substitution rule parseserialn_rules(8).
     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 parseserialn_rules(9).
     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 parseserialn_rules(18).
     This was achieved by replacing all occurrences of long_long_integer__first 
          by:
          - 9223372036854775808.
<S>  New H32:  true
-S-  Applied substitution rule parseserialn_rules(19).
     This was achieved by replacing all occurrences of long_long_integer__last 
          by:
          9223372036854775807.
<S>  New H33:  true
-S-  Applied substitution rule parseserialn_rules(23).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H4:  true
-S-  Applied substitution rule parseserialn_rules(24).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H5:  true
-S-  Applied substitution rule parseserialn_rules(29).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__first by:
          rr_type__domainnameortimespec.
<S>  New H21:  rr_type__domainnameortimespec <= foundtype__1
-S-  Applied substitution rule parseserialn_rules(30).
     This was achieved by replacing all occurrences of 
          rr_type__rritemtype__last by:
          rr_type__other.
<S>  New H22:  foundtype__1 <= rr_type__other
-S-  Applied substitution rule parseserialn_rules(70).
     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 H17:  begidx__1 >= 1
<S>  New H19:  endidx__1 >= 1
<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 parseserialn_rules(71).
     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 H18:  begidx__1 <= 256
<S>  New H20:  endidx__1 <= 256
<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 C1:  begidx__1 >= 1
     using hypothesis H17.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parseserialnumber_8.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  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 H17 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H22).
%%%  Simplified C4 on reading formula in, to give:
     %%%  C4:  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:  begidx >= 1
     using hypothesis H1.
***  Proved C3:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 
          rr_type__soa_record_type__max_serial_val
     using hypothesis H29.
***  Proved C4:  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)
     using hypothesis H4.
***  Proved C5:  zlength >= rr_type__linelengthindex__first
     using hypothesis H5.
***  Proved C6:  zlength <= rr_type__linelengthindex__last
     using hypothesis H6.
***  Proved C7:  loop__1__i + 1 >= integer__first
     using hypothesis H7.
***  Proved C9:  loop__1__i + 1 >= begidx
     using hypothesis H9.
***  Proved C11:  endidx__entry__loop__1 >= rr_type__linelengthindex__first
     using hypothesis H11.
***  Proved C12:  endidx__entry__loop__1 <= rr_type__linelengthindex__last
     using hypothesis H12.
-S-  Applied substitution rule parseserialn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H8:  loop__1__i <= 2147483647
<S>  New C8:  loop__1__i <= 2147483646
>>>  Restructured hypothesis H29 into:
     >>>  H29:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 
          rr_type__soa_record_type__max_serial_val
>>>  Restructured hypothesis H30 into:
     >>>  H30:  loop__1__i <> endidx__entry__loop__1
-S-  Applied substitution rule parseserialn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__soa_record_type__max_serial_val by:
          4294967295.
<S>  New H3:  tmpval <= 4294967295
<S>  New H29:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 4294967295
-S-  Applied substitution rule parseserialn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H7:  loop__1__i >= - 2147483648
-S-  Applied substitution rule parseserialn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H4:  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 parseserialn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H4:  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 parseserialn_rules(18).
     This was achieved by replacing all occurrences of long_long_integer__first 
          by:
          - 9223372036854775808.
<S>  New H19:  tmpval >= - 9223372036854775808
<S>  New H21:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= - 9223372036854775808
<S>  New H23:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= - 9223372036854775808
-S-  Applied substitution rule parseserialn_rules(19).
     This was achieved by replacing all occurrences of long_long_integer__last 
          by:
          9223372036854775807.
<S>  New H20:  tmpval <= 9223372036854775807
<S>  New H22:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 9223372036854775807
<S>  New H24:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 9223372036854775807
-S-  Applied substitution rule parseserialn_rules(20).
     This was achieved by replacing all occurrences of 
          long_long_integer__base__first by:
          - 9223372036854775808.
<S>  New H25:  10 * tmpval >= - 9223372036854775808
-S-  Applied substitution rule parseserialn_rules(21).
     This was achieved by replacing all occurrences of 
          long_long_integer__base__last by:
          9223372036854775807.
<S>  New H26:  10 * tmpval <= 9223372036854775807
-S-  Applied substitution rule parseserialn_rules(23).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H13:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= 0
-S-  Applied substitution rule parseserialn_rules(24).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H14:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 4294967295
-S-  Applied substitution rule parseserialn_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__modulus by:
          4294967296.
<S>  New H29:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 4294967295
<S>  New H21:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 >= - 9223372036854775808
<S>  New H23:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 >= - 
          9223372036854775808
<S>  New H22:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 9223372036854775807
<S>  New H24:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 <= 
          9223372036854775807
<S>  New H13:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 >= 0
<S>  New H14:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 <= 
          4294967295
<S>  New C2:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 >= 0
-S-  Applied substitution rule parseserialn_rules(70).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H5:  zlength >= 1
<S>  New H11:  endidx__entry__loop__1 >= 1
<S>  New H15:  loop__1__i >= 1
<S>  New H4:  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 parseserialn_rules(71).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H6:  zlength <= 256
<S>  New H12:  endidx__entry__loop__1 <= 256
<S>  New H16:  loop__1__i <= 256
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
%%%  Hypotheses H10 & H30 together imply that
          loop__1__i < endidx__entry__loop__1.
     H10 & H30 have therefore been deleted and a new H31 added to this effect.
***  Proved C10:  loop__1__i + 1 <= endidx__entry__loop__1
     via its standard form, which is:
     Std.Fm C10:  endidx__entry__loop__1 - loop__1__i > 0
     using hypothesis H31.
***  Proved C8:  loop__1__i <= 2147483646
     using hypothesis H16.
***  Proved C2:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 >= 0
     using hypotheses H2 & H13.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parseserialnumber_9.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  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 C4:  loop__1__i <= rr_type__linelengthindex__last
     using hypotheses H10 & H12.
-S-  Applied substitution rule parseserialn_rules(23).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New C1:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= 0
-S-  Applied substitution rule parseserialn_rules(24).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New C2:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 4294967295
-S-  Applied substitution rule parseserialn_rules(70).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 
          rr_type__linelengthindex__last -> character__first <= element(
          zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          character__last)
<S>  New H5:  zlength >= 1
<S>  New H11:  endidx__entry__loop__1 >= 1
<S>  New C3:  loop__1__i >= 1
***  Proved C3:  loop__1__i >= 1
     using hypotheses H1 & H9.
-S-  Applied substitution rule parseserialn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__soa_record_type__max_serial_val by:
          4294967295.
<S>  New H3:  tmpval <= 4294967295
-S-  Applied substitution rule parseserialn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H7:  loop__1__i >= - 2147483648
-S-  Applied substitution rule parseserialn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H8:  loop__1__i <= 2147483647
-S-  Applied substitution rule parseserialn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H4:  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]) <= character__last)
-S-  Applied substitution rule parseserialn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H4:  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 parseserialn_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__modulus by:
          4294967296.
<S>  New C1:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 >= 0
<S>  New C2:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 <= 
          4294967295
-S-  Applied substitution rule parseserialn_rules(71).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H6:  zlength <= 256
<S>  New H12:  endidx__entry__loop__1 <= 256
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C1:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 >= 0
***  Proved C2:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 <= 
          4294967295
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parseserialnumber_10.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  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 H17 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H14).
-S-  Applied substitution rule parseserialn_rules(18).
     This was achieved by replacing all occurrences of long_long_integer__first 
          by:
          - 9223372036854775808.
<S>  New H19:  tmpval >= - 9223372036854775808
<S>  New C1:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= - 9223372036854775808
<S>  New C3:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= - 9223372036854775808
-S-  Applied substitution rule parseserialn_rules(19).
     This was achieved by replacing all occurrences of long_long_integer__last 
          by:
          9223372036854775807.
<S>  New H20:  tmpval <= 9223372036854775807
<S>  New C2:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 9223372036854775807
<S>  New C4:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 9223372036854775807
-S-  Applied substitution rule parseserialn_rules(20).
     This was achieved by replacing all occurrences of 
          long_long_integer__base__first by:
          - 9223372036854775808.
<S>  New C5:  10 * tmpval >= - 9223372036854775808
-S-  Applied substitution rule parseserialn_rules(21).
     This was achieved by replacing all occurrences of 
          long_long_integer__base__last by:
          9223372036854775807.
<S>  New C6:  10 * tmpval <= 9223372036854775807
***  Proved C5:  10 * tmpval >= - 9223372036854775808
     using hypothesis H2.
-S-  Applied substitution rule parseserialn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__soa_record_type__max_serial_val by:
          4294967295.
<S>  New H3:  tmpval <= 4294967295
-S-  Applied substitution rule parseserialn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H7:  loop__1__i >= - 2147483648
-S-  Applied substitution rule parseserialn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H8:  loop__1__i <= 2147483647
-S-  Applied substitution rule parseserialn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H4:  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 parseserialn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H4:  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 parseserialn_rules(23).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H13:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= 0
-S-  Applied substitution rule parseserialn_rules(24).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H14:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 4294967295
-S-  Applied substitution rule parseserialn_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__modulus by:
          4294967296.
<S>  New H13:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 >= 0
<S>  New H14:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 <= 
          4294967295
<S>  New C1:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 >= - 9223372036854775808
<S>  New C3:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 >= - 
          9223372036854775808
<S>  New C2:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 9223372036854775807
<S>  New C4:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 <= 
          9223372036854775807
-S-  Applied substitution rule parseserialn_rules(70).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H5:  zlength >= 1
<S>  New H11:  endidx__entry__loop__1 >= 1
<S>  New H15:  loop__1__i >= 1
<S>  New H4:  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 parseserialn_rules(71).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H6:  zlength <= 256
<S>  New H12:  endidx__entry__loop__1 <= 256
<S>  New H16:  loop__1__i <= 256
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C6:  10 * tmpval <= 9223372036854775807
     using hypothesis H3.
***  Proved C1:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 >= - 9223372036854775808
     using hypotheses H2 & H13.
***  Proved C3:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 >= - 
          9223372036854775808
     using hypothesis H13.
***  Proved C2:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 9223372036854775807
     using hypotheses H3 & H14.
***  Proved C4:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 <= 
          9223372036854775807
     using hypothesis H14.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parseserialnumber_11.  @@@@@@@@@@
%%%  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 H34 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H18).
---  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 H44 has been replaced by "true".  (It is already present, as 
          H17).
---  Hypothesis H45 has been replaced by "true".  (It is already present, as 
          H18).
---  Hypothesis H46 has been replaced by "true".  (It is already present, as 
          H19).
---  Hypothesis H47 has been replaced by "true".  (It is already present, as 
          H20).
---  Hypothesis H49 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H50 has been replaced by "true".  (It is already present, as 
          H33).
---  Hypothesis H52 has been replaced by "true".  (It is already present, as 
          H32).
---  Hypothesis H53 has been replaced by "true".  (It is already present, as 
          H33).
***  Proved C1:  0 >= unsigned_types__unsigned32__first
     using hypothesis H4.
***  Proved C2:  0 <= unsigned_types__unsigned32__last
     using hypothesis H5.
***  Proved C3:  0 >= unsigned_types__unsigned32__first
     using hypothesis H4.
***  Proved C4:  0 <= unsigned_types__unsigned32__last
     using hypothesis H5.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parseserialnumber_12.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  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 H17 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H30 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H22).
-S-  Applied substitution rule parseserialn_rules(23).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H13:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= 0
<S>  New C1:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= 0
<S>  New C3:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= 0
-S-  Applied substitution rule parseserialn_rules(24).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H14:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 4294967295
<S>  New C2:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 4294967295
<S>  New C4:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 4294967295
***  Proved C1:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= 0
     using hypotheses H2 & H13.
***  Proved C3:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= 0
     using hypotheses H2 & H13.
>>>  Restructured hypothesis H32 into:
     >>>  H32:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 
          rr_type__soa_record_type__max_serial_val
-S-  Applied substitution rule parseserialn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__soa_record_type__max_serial_val by:
          4294967295.
<S>  New H3:  tmpval <= 4294967295
<S>  New H29:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus > 4294967295
<S>  New H32:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 4294967295
-S-  Applied substitution rule parseserialn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H7:  loop__1__i >= - 2147483648
-S-  Applied substitution rule parseserialn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H8:  loop__1__i <= 2147483647
-S-  Applied substitution rule parseserialn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H4:  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 parseserialn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H4:  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 parseserialn_rules(18).
     This was achieved by replacing all occurrences of long_long_integer__first 
          by:
          - 9223372036854775808.
<S>  New H19:  tmpval >= - 9223372036854775808
<S>  New H21:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= - 9223372036854775808
<S>  New H23:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= - 9223372036854775808
-S-  Applied substitution rule parseserialn_rules(19).
     This was achieved by replacing all occurrences of long_long_integer__last 
          by:
          9223372036854775807.
<S>  New H20:  tmpval <= 9223372036854775807
<S>  New H22:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 9223372036854775807
<S>  New H24:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 9223372036854775807
-S-  Applied substitution rule parseserialn_rules(20).
     This was achieved by replacing all occurrences of 
          long_long_integer__base__first by:
          - 9223372036854775808.
<S>  New H25:  10 * tmpval >= - 9223372036854775808
-S-  Applied substitution rule parseserialn_rules(21).
     This was achieved by replacing all occurrences of 
          long_long_integer__base__last by:
          9223372036854775807.
<S>  New H26:  10 * tmpval <= 9223372036854775807
-S-  Applied substitution rule parseserialn_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__modulus by:
          4294967296.
<S>  New H13:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 >= 0
<S>  New H14:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 <= 
          4294967295
<S>  New H29:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 > 4294967295
<S>  New H32:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 4294967295
<S>  New H21:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 >= - 9223372036854775808
<S>  New H23:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 >= - 
          9223372036854775808
<S>  New H22:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 9223372036854775807
<S>  New H24:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 <= 
          9223372036854775807
<S>  New C2:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 4294967295
<S>  New C4:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 4294967295
-S-  Applied substitution rule parseserialn_rules(70).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H5:  zlength >= 1
<S>  New H11:  endidx__entry__loop__1 >= 1
<S>  New H15:  loop__1__i >= 1
<S>  New H4:  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 parseserialn_rules(71).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H6:  zlength <= 256
<S>  New H12:  endidx__entry__loop__1 <= 256
<S>  New H16:  loop__1__i <= 256
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C2:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 4294967295
     using hypothesis H32.
***  Proved C4:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 4294967295
     using hypothesis H32.
***  PROVED VC.


@@@@@@@@@@  VC: procedure_parseserialnumber_13.  @@@@@@@@@@
%%%  Simplified H4 on reading formula in, to give:
     %%%  H4:  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 H17 has been replaced by "true".  (It is already present, as 
          H13).
---  Hypothesis H18 has been replaced by "true".  (It is already present, as 
          H14).
---  Hypothesis H27 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H28 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H31 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H32 has been replaced by "true".  (It is already present, as 
          H22).
---  Hypothesis H33 has been replaced by "true".  (It is already present, as 
          H29).
---  Hypothesis H34 has been replaced by "true".  (It is already present, as 
          H21).
---  Hypothesis H35 has been replaced by "true".  (It is already present, as 
          H22).
-S-  Applied substitution rule parseserialn_rules(23).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__first by:
          0.
<S>  New H13:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= 0
<S>  New C1:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= 0
<S>  New C3:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= 0
-S-  Applied substitution rule parseserialn_rules(24).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__last by:
          4294967295.
<S>  New H14:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 4294967295
<S>  New C2:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 4294967295
<S>  New C4:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 4294967295
***  Proved C1:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= 0
     using hypotheses H2 & H13.
***  Proved C3:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= 0
     using hypotheses H2 & H13.
>>>  Restructured hypothesis H29 into:
     >>>  H29:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 
          rr_type__soa_record_type__max_serial_val
-S-  Applied substitution rule parseserialn_rules(1).
     This was achieved by replacing all occurrences of 
          rr_type__soa_record_type__max_serial_val by:
          4294967295.
<S>  New H3:  tmpval <= 4294967295
<S>  New H29:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 4294967295
-S-  Applied substitution rule parseserialn_rules(3).
     This was achieved by replacing all occurrences of integer__first by:
          - 2147483648.
<S>  New H7:  loop__1__i >= - 2147483648
-S-  Applied substitution rule parseserialn_rules(4).
     This was achieved by replacing all occurrences of integer__last by:
          2147483647.
<S>  New H8:  loop__1__i <= 2147483647
-S-  Applied substitution rule parseserialn_rules(8).
     This was achieved by replacing all occurrences of character__first by:
          0.
<S>  New H4:  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 parseserialn_rules(9).
     This was achieved by replacing all occurrences of character__last by:
          255.
<S>  New H4:  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 parseserialn_rules(18).
     This was achieved by replacing all occurrences of long_long_integer__first 
          by:
          - 9223372036854775808.
<S>  New H19:  tmpval >= - 9223372036854775808
<S>  New H21:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= - 9223372036854775808
<S>  New H23:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus >= - 9223372036854775808
-S-  Applied substitution rule parseserialn_rules(19).
     This was achieved by replacing all occurrences of long_long_integer__last 
          by:
          9223372036854775807.
<S>  New H20:  tmpval <= 9223372036854775807
<S>  New H22:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 9223372036854775807
<S>  New H24:  (element(zonefileline, [loop__1__i]) - 48) mod 
          unsigned_types__unsigned32__modulus <= 9223372036854775807
-S-  Applied substitution rule parseserialn_rules(20).
     This was achieved by replacing all occurrences of 
          long_long_integer__base__first by:
          - 9223372036854775808.
<S>  New H25:  10 * tmpval >= - 9223372036854775808
-S-  Applied substitution rule parseserialn_rules(21).
     This was achieved by replacing all occurrences of 
          long_long_integer__base__last by:
          9223372036854775807.
<S>  New H26:  10 * tmpval <= 9223372036854775807
-S-  Applied substitution rule parseserialn_rules(27).
     This was achieved by replacing all occurrences of 
          unsigned_types__unsigned32__modulus by:
          4294967296.
<S>  New H13:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 >= 0
<S>  New H14:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 <= 
          4294967295
<S>  New H29:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 4294967295
<S>  New H21:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 >= - 9223372036854775808
<S>  New H23:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 >= - 
          9223372036854775808
<S>  New H22:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 9223372036854775807
<S>  New H24:  (element(zonefileline, [loop__1__i]) - 48) mod 4294967296 <= 
          9223372036854775807
<S>  New C2:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 4294967295
<S>  New C4:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 4294967295
-S-  Applied substitution rule parseserialn_rules(70).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__first by:
          1.
<S>  New H5:  zlength >= 1
<S>  New H11:  endidx__entry__loop__1 >= 1
<S>  New H15:  loop__1__i >= 1
<S>  New H4:  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 parseserialn_rules(71).
     This was achieved by replacing all occurrences of 
          rr_type__linelengthindex__last by:
          256.
<S>  New H6:  zlength <= 256
<S>  New H12:  endidx__entry__loop__1 <= 256
<S>  New H16:  loop__1__i <= 256
<S>  New H4:  for_all(i___1 : integer, 1 <= i___1 and i___1 <= 256 -> 0 <= 
          element(zonefileline, [i___1]) and element(zonefileline, [i___1]) <= 
          255)
***  Proved C2:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 4294967295
     using hypothesis H29.
***  Proved C4:  10 * tmpval + (element(zonefileline, [loop__1__i]) - 48) mod 
          4294967296 <= 4294967295
     using hypothesis H29.
***  PROVED VC.


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


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


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


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


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


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


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

