ironsides/parser_utilities/converttimestring.slg

6273 lines
292 KiB
Plaintext

*****************************************************************************
Semantic Analysis of SPARK Text
Examiner GPL Edition
*****************************************************************************
SPARK Simplifier GPL 2011
Copyright (C) 2011 Altran Praxis Limited, Bath, U.K.
procedure Parser_Utilities.ConvertTimeString
@@@@@@@@@@ VC: procedure_converttimestring_1. @@@@@@@@@@
%%% Simplified H1 on reading formula in, to give:
%%% H1: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
%%% Simplified H2 on reading formula in, to give:
%%% H2: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified C2 on reading formula in, to give:
%%% C2: true
%%% Simplified C3 on reading formula in, to give:
%%% C3: true
%%% Simplified C4 on reading formula in, to give:
%%% C4: true
%%% Simplified C5 on reading formula in, to give:
%%% C5: true
%%% Simplified C6 on reading formula in, to give:
%%% C6: true
%%% Simplified C7 on reading formula in, to give:
%%% C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified C9 on reading formula in, to give:
%%% C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
%%% Simplified C10 on reading formula in, to give:
%%% C10: true
%%% Simplified C12 on reading formula in, to give:
%%% C12: true
*** Proved C2: true
*** Proved C3: true
*** Proved C4: true
*** Proved C5: true
*** Proved C6: true
*** Proved C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
using hypothesis H2.
*** Proved C8: true
*** Proved C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
using hypothesis H1.
*** Proved C10: true
*** Proved C12: true
-S- Applied substitution rule converttimes_rules(1).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__max_year by:
2020.
<S> New C1: true
-S- Applied substitution rule converttimes_rules(34).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__first by:
1.
<S> New H1: for_all(i_ : integer, 1 <= i_ and i_ <=
rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H2: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
<S> New C11: 1 <= rr_type__rrsig_record_type__timestringtypeindex__last
<S> New C13: 1 <= rr_type__rrsig_record_type__timestringtypeindex__last
-S- Applied substitution rule converttimes_rules(35).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__last by:
14.
<S> New H1: for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H2: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
<S> New C11: true
<S> New C13: true
*** Proved C1: true
*** Proved C11: true
*** Proved C13: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_2. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H21 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H27 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H28 has been replaced by "true". (It is already present, as
H24).
%%% Simplified C7 on reading formula in, to give:
%%% C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified C9 on reading formula in, to give:
%%% C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
*** Proved C2: month <= 12
using hypothesis H2.
*** Proved C3: day <= 31
using hypothesis H3.
*** Proved C4: hour <= 23
using hypothesis H4.
*** Proved C5: minute <= 59
using hypothesis H5.
*** Proved C6: second <= 59
using hypothesis H6.
*** Proved C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
using hypothesis H7.
*** Proved C8: true
*** Proved C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
using hypothesis H9.
*** Proved C10: loop__1__i + 1 >=
rr_type__rrsig_record_type__timestringtypeindex__first
using hypothesis H10.
*** Proved C12: loop__1__i + 1 >=
rr_type__rrsig_record_type__timestringtypeindex__first
using hypothesis H10.
-S- Applied substitution rule converttimes_rules(1).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__max_year by:
2020.
<S> New H1: year <= 2020
<S> New H39: not (10 * year + (element(timestring, [loop__1__i]) - 48) > 2020
or (month > monthsinayear or day > maxdaysinamonth or hour >=
hoursinaday or minute >= minutesinanhour or second >=
secondsinaminute))
<S> New C1: 10 * year + (element(timestring, [loop__1__i]) - 48) <= 2020
-S- Applied substitution rule converttimes_rules(35).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__last by:
14.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> character__first <= element(timestring, [i___1]) and
element(timestring, [i___1]) <= character__last)
<S> New H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= 14 -> 48 <= element(timestring, [i_]) and element(timestring, [i_])
<= 57)
<S> New H11: loop__1__i <= 14
<S> New H40: not loop__1__i = 14
<S> New C11: loop__1__i <= 13
<S> New C13: loop__1__i <= 13
*** Proved C11: loop__1__i <= 13
using hypotheses H11 & H40.
*** Proved C13: loop__1__i <= 13
using hypotheses H11 & H40.
>>> Restructured hypothesis H39 into:
>>> H39: 10 * year + (element(timestring, [loop__1__i]) - 48) <= 2020
and (month <= monthsinayear and day <= maxdaysinamonth and hour <
hoursinaday and minute < minutesinanhour and second <
secondsinaminute)
>>> Restructured hypothesis H40 into:
>>> H40: loop__1__i <> 14
>>> Hypothesis H39 has now been split into two, giving:
>>> H41: 10 * year + (element(timestring, [loop__1__i]) - 48) <= 2020
>>> H42: month <= monthsinayear and day <= maxdaysinamonth and hour <
hoursinaday and minute < minutesinanhour and second < secondsinaminute
>>> Hypothesis H42 has now been split into two, giving:
>>> H43: month <= monthsinayear and day <= maxdaysinamonth and hour <
hoursinaday and minute < minutesinanhour
>>> H44: second < secondsinaminute
>>> Hypothesis H43 has now been split into two, giving:
>>> H45: month <= monthsinayear and day <= maxdaysinamonth and hour <
hoursinaday
>>> H46: minute < minutesinanhour
>>> Hypothesis H45 has now been split into two, giving:
>>> H47: month <= monthsinayear and day <= maxdaysinamonth
>>> H48: hour < hoursinaday
>>> Hypothesis H47 has now been split into two, giving:
>>> H49: month <= monthsinayear
>>> H50: day <= maxdaysinamonth
-S- Applied substitution rule converttimes_rules(2).
This was achieved by replacing all occurrences of secondsinaminute by:
60.
<S> New H44: second < 60
-S- Applied substitution rule converttimes_rules(3).
This was achieved by replacing all occurrences of minutesinanhour by:
60.
<S> New H46: minute < 60
-S- Applied substitution rule converttimes_rules(4).
This was achieved by replacing all occurrences of hoursinaday by:
24.
<S> New H48: hour < 24
-S- Applied substitution rule converttimes_rules(5).
This was achieved by replacing all occurrences of maxdaysinamonth by:
31.
<S> New H50: day <= 31
-S- Applied substitution rule converttimes_rules(6).
This was achieved by replacing all occurrences of monthsinayear by:
12.
<S> New H49: month <= 12
-S- Applied substitution rule converttimes_rules(10).
This was achieved by replacing all occurrences of integer__base__first by:
- 2147483648.
<S> New H25: 10 * year >= - 2147483648
-S- Applied substitution rule converttimes_rules(11).
This was achieved by replacing all occurrences of integer__base__last by:
2147483647.
<S> New H26: 10 * year <= 2147483647
-S- Applied substitution rule converttimes_rules(13).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
-S- Applied substitution rule converttimes_rules(14).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= 255)
-S- Applied substitution rule converttimes_rules(18).
This was achieved by replacing all occurrences of natural__first by:
0.
<S> New H14: element(timestring, [loop__1__i]) >= 48
<S> New H19: year >= 0
<S> New H23: 10 * year + (element(timestring, [loop__1__i]) - 48) >= 0
<S> New H29: month >= 0
<S> New H31: day >= 0
<S> New H33: hour >= 0
<S> New H35: minute >= 0
<S> New H37: second >= 0
-S- Applied substitution rule converttimes_rules(19).
This was achieved by replacing all occurrences of natural__last by:
2147483647.
<S> New H15: element(timestring, [loop__1__i]) <= 2147483695
<S> New H20: year <= 2147483647
<S> New H24: 10 * year + (element(timestring, [loop__1__i]) - 48) <=
2147483647
<S> New H30: month <= 2147483647
<S> New H32: day <= 2147483647
<S> New H34: hour <= 2147483647
<S> New H36: minute <= 2147483647
<S> New H38: second <= 2147483647
-S- Applied substitution rule converttimes_rules(34).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__first by:
1.
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H10: loop__1__i >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <=
element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
%%% Hypotheses H11 & H40 together imply that
loop__1__i < 14.
H11 & H40 have therefore been deleted and a new H51 added to this effect.
*** Proved C1: 10 * year + (element(timestring, [loop__1__i]) - 48) <= 2020
using hypothesis H41.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_3. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H30 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H31 has been replaced by "true". (It is already present, as
H25).
%%% Simplified C7 on reading formula in, to give:
%%% C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified C9 on reading formula in, to give:
%%% C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
*** Proved C1: year <= rr_type__rrsig_record_type__max_year
using hypothesis H1.
*** Proved C3: day <= 31
using hypothesis H3.
*** Proved C4: hour <= 23
using hypothesis H4.
*** Proved C5: minute <= 59
using hypothesis H5.
*** Proved C6: second <= 59
using hypothesis H6.
*** Proved C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
using hypothesis H7.
*** Proved C8: true
*** Proved C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
using hypothesis H9.
*** Proved C10: loop__1__i + 1 >=
rr_type__rrsig_record_type__timestringtypeindex__first
using hypothesis H10.
*** Proved C12: loop__1__i + 1 >=
rr_type__rrsig_record_type__timestringtypeindex__first
using hypothesis H10.
-S- Applied substitution rule converttimes_rules(35).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__last by:
14.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> character__first <= element(timestring, [i___1]) and
element(timestring, [i___1]) <= character__last)
<S> New H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= 14 -> 48 <= element(timestring, [i_]) and element(timestring, [i_])
<= 57)
<S> New H11: loop__1__i <= 14
<S> New H41: not loop__1__i = 14
<S> New C11: loop__1__i <= 13
<S> New C13: loop__1__i <= 13
*** Proved C11: loop__1__i <= 13
using hypotheses H11 & H41.
*** Proved C13: loop__1__i <= 13
using hypotheses H11 & H41.
>>> Restructured hypothesis H18 into:
>>> H18: 4 < loop__1__i
>>> Restructured hypothesis H40 into:
>>> H40: year <= rr_type__rrsig_record_type__max_year and (10 * month + (
element(timestring, [loop__1__i]) - 48) <= monthsinayear and day <=
maxdaysinamonth and hour < hoursinaday and minute < minutesinanhour
and second < secondsinaminute)
>>> Restructured hypothesis H41 into:
>>> H41: loop__1__i <> 14
--- Attempted addition of new hypothesis:
year <= rr_type__rrsig_record_type__max_year
eliminated: this already exists (as H1).
>>> Hypothesis H40 has now been split into two, giving:
>>> H1: year <= rr_type__rrsig_record_type__max_year
>>> H42: 10 * month + (element(timestring, [loop__1__i]) - 48) <=
monthsinayear and day <= maxdaysinamonth and hour < hoursinaday and
minute < minutesinanhour and second < secondsinaminute
>>> Hypothesis H42 has now been split into two, giving:
>>> H43: 10 * month + (element(timestring, [loop__1__i]) - 48) <=
monthsinayear and day <= maxdaysinamonth and hour < hoursinaday and
minute < minutesinanhour
>>> H44: second < secondsinaminute
>>> Hypothesis H43 has now been split into two, giving:
>>> H45: 10 * month + (element(timestring, [loop__1__i]) - 48) <=
monthsinayear and day <= maxdaysinamonth and hour < hoursinaday
>>> H46: minute < minutesinanhour
>>> Hypothesis H45 has now been split into two, giving:
>>> H47: 10 * month + (element(timestring, [loop__1__i]) - 48) <=
monthsinayear and day <= maxdaysinamonth
>>> H48: hour < hoursinaday
>>> Hypothesis H47 has now been split into two, giving:
>>> H49: 10 * month + (element(timestring, [loop__1__i]) - 48) <=
monthsinayear
>>> H50: day <= maxdaysinamonth
-S- Applied substitution rule converttimes_rules(1).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__max_year by:
2020.
<S> New H1: year <= 2020
-S- Applied substitution rule converttimes_rules(2).
This was achieved by replacing all occurrences of secondsinaminute by:
60.
<S> New H44: second < 60
-S- Applied substitution rule converttimes_rules(3).
This was achieved by replacing all occurrences of minutesinanhour by:
60.
<S> New H46: minute < 60
-S- Applied substitution rule converttimes_rules(4).
This was achieved by replacing all occurrences of hoursinaday by:
24.
<S> New H48: hour < 24
-S- Applied substitution rule converttimes_rules(5).
This was achieved by replacing all occurrences of maxdaysinamonth by:
31.
<S> New H50: day <= 31
-S- Applied substitution rule converttimes_rules(6).
This was achieved by replacing all occurrences of monthsinayear by:
12.
<S> New H49: 10 * month + (element(timestring, [loop__1__i]) - 48) <= 12
-S- Applied substitution rule converttimes_rules(10).
This was achieved by replacing all occurrences of integer__base__first by:
- 2147483648.
<S> New H26: 10 * month >= - 2147483648
-S- Applied substitution rule converttimes_rules(11).
This was achieved by replacing all occurrences of integer__base__last by:
2147483647.
<S> New H27: 10 * month <= 2147483647
-S- Applied substitution rule converttimes_rules(13).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
-S- Applied substitution rule converttimes_rules(14).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= 255)
-S- Applied substitution rule converttimes_rules(18).
This was achieved by replacing all occurrences of natural__first by:
0.
<S> New H14: element(timestring, [loop__1__i]) >= 48
<S> New H20: month >= 0
<S> New H24: 10 * month + (element(timestring, [loop__1__i]) - 48) >= 0
<S> New H28: year >= 0
<S> New H32: day >= 0
<S> New H34: hour >= 0
<S> New H36: minute >= 0
<S> New H38: second >= 0
-S- Applied substitution rule converttimes_rules(19).
This was achieved by replacing all occurrences of natural__last by:
2147483647.
<S> New H15: element(timestring, [loop__1__i]) <= 2147483695
<S> New H21: month <= 2147483647
<S> New H25: 10 * month + (element(timestring, [loop__1__i]) - 48) <=
2147483647
<S> New H29: year <= 2147483647
<S> New H33: day <= 2147483647
<S> New H35: hour <= 2147483647
<S> New H37: minute <= 2147483647
<S> New H39: second <= 2147483647
-S- Applied substitution rule converttimes_rules(34).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__first by:
1.
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H10: loop__1__i >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <=
element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
%%% Hypotheses H11 & H41 together imply that
loop__1__i < 14.
H11 & H41 have therefore been deleted and a new H51 added to this effect.
*** Proved C2: 10 * month + (element(timestring, [loop__1__i]) - 48) <= 12
using hypothesis H49.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_4. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H33 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H34 has been replaced by "true". (It is already present, as
H26).
%%% Simplified C7 on reading formula in, to give:
%%% C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified C9 on reading formula in, to give:
%%% C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
*** Proved C1: year <= rr_type__rrsig_record_type__max_year
using hypothesis H1.
*** Proved C2: month <= 12
using hypothesis H2.
*** Proved C4: hour <= 23
using hypothesis H4.
*** Proved C5: minute <= 59
using hypothesis H5.
*** Proved C6: second <= 59
using hypothesis H6.
*** Proved C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
using hypothesis H7.
*** Proved C8: true
*** Proved C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
using hypothesis H9.
*** Proved C10: loop__1__i + 1 >=
rr_type__rrsig_record_type__timestringtypeindex__first
using hypothesis H10.
*** Proved C12: loop__1__i + 1 >=
rr_type__rrsig_record_type__timestringtypeindex__first
using hypothesis H10.
-S- Applied substitution rule converttimes_rules(35).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__last by:
14.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> character__first <= element(timestring, [i___1]) and
element(timestring, [i___1]) <= character__last)
<S> New H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= 14 -> 48 <= element(timestring, [i_]) and element(timestring, [i_])
<= 57)
<S> New H11: loop__1__i <= 14
<S> New H42: not loop__1__i = 14
<S> New C11: loop__1__i <= 13
<S> New C13: loop__1__i <= 13
*** Proved C11: loop__1__i <= 13
using hypotheses H11 & H42.
*** Proved C13: loop__1__i <= 13
using hypotheses H11 & H42.
>>> Restructured hypothesis H18 into:
>>> H18: 4 < loop__1__i
>>> Restructured hypothesis H19 into:
>>> H19: 6 < loop__1__i
>>> Restructured hypothesis H41 into:
>>> H41: year <= rr_type__rrsig_record_type__max_year and (month <=
monthsinayear and 10 * day + (element(timestring, [loop__1__i]) - 48)
<= maxdaysinamonth and hour < hoursinaday and minute <
minutesinanhour and second < secondsinaminute)
>>> Restructured hypothesis H42 into:
>>> H42: loop__1__i <> 14
--- Attempted addition of new hypothesis:
year <= rr_type__rrsig_record_type__max_year
eliminated: this already exists (as H1).
>>> Hypothesis H41 has now been split into two, giving:
>>> H1: year <= rr_type__rrsig_record_type__max_year
>>> H43: month <= monthsinayear and 10 * day + (element(timestring, [
loop__1__i]) - 48) <= maxdaysinamonth and hour < hoursinaday and
minute < minutesinanhour and second < secondsinaminute
>>> Hypothesis H43 has now been split into two, giving:
>>> H44: month <= monthsinayear and 10 * day + (element(timestring, [
loop__1__i]) - 48) <= maxdaysinamonth and hour < hoursinaday and
minute < minutesinanhour
>>> H45: second < secondsinaminute
>>> Hypothesis H44 has now been split into two, giving:
>>> H46: month <= monthsinayear and 10 * day + (element(timestring, [
loop__1__i]) - 48) <= maxdaysinamonth and hour < hoursinaday
>>> H47: minute < minutesinanhour
>>> Hypothesis H46 has now been split into two, giving:
>>> H48: month <= monthsinayear and 10 * day + (element(timestring, [
loop__1__i]) - 48) <= maxdaysinamonth
>>> H49: hour < hoursinaday
>>> Hypothesis H48 has now been split into two, giving:
>>> H50: month <= monthsinayear
>>> H51: 10 * day + (element(timestring, [loop__1__i]) - 48) <=
maxdaysinamonth
-S- Applied substitution rule converttimes_rules(1).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__max_year by:
2020.
<S> New H1: year <= 2020
-S- Applied substitution rule converttimes_rules(2).
This was achieved by replacing all occurrences of secondsinaminute by:
60.
<S> New H45: second < 60
-S- Applied substitution rule converttimes_rules(3).
This was achieved by replacing all occurrences of minutesinanhour by:
60.
<S> New H47: minute < 60
-S- Applied substitution rule converttimes_rules(4).
This was achieved by replacing all occurrences of hoursinaday by:
24.
<S> New H49: hour < 24
-S- Applied substitution rule converttimes_rules(5).
This was achieved by replacing all occurrences of maxdaysinamonth by:
31.
<S> New H51: 10 * day + (element(timestring, [loop__1__i]) - 48) <= 31
-S- Applied substitution rule converttimes_rules(6).
This was achieved by replacing all occurrences of monthsinayear by:
12.
<S> New H50: month <= 12
-S- Applied substitution rule converttimes_rules(10).
This was achieved by replacing all occurrences of integer__base__first by:
- 2147483648.
<S> New H27: 10 * day >= - 2147483648
-S- Applied substitution rule converttimes_rules(11).
This was achieved by replacing all occurrences of integer__base__last by:
2147483647.
<S> New H28: 10 * day <= 2147483647
-S- Applied substitution rule converttimes_rules(13).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
-S- Applied substitution rule converttimes_rules(14).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= 255)
-S- Applied substitution rule converttimes_rules(18).
This was achieved by replacing all occurrences of natural__first by:
0.
<S> New H14: element(timestring, [loop__1__i]) >= 48
<S> New H21: day >= 0
<S> New H25: 10 * day + (element(timestring, [loop__1__i]) - 48) >= 0
<S> New H29: year >= 0
<S> New H31: month >= 0
<S> New H35: hour >= 0
<S> New H37: minute >= 0
<S> New H39: second >= 0
-S- Applied substitution rule converttimes_rules(19).
This was achieved by replacing all occurrences of natural__last by:
2147483647.
<S> New H15: element(timestring, [loop__1__i]) <= 2147483695
<S> New H22: day <= 2147483647
<S> New H26: 10 * day + (element(timestring, [loop__1__i]) - 48) <= 2147483647
<S> New H30: year <= 2147483647
<S> New H32: month <= 2147483647
<S> New H36: hour <= 2147483647
<S> New H38: minute <= 2147483647
<S> New H40: second <= 2147483647
-S- Applied substitution rule converttimes_rules(34).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__first by:
1.
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H10: loop__1__i >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <=
element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
%%% Hypotheses H11 & H42 together imply that
loop__1__i < 14.
H11 & H42 have therefore been deleted and a new H52 added to this effect.
*** Proved C3: 10 * day + (element(timestring, [loop__1__i]) - 48) <= 31
using hypothesis H51.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_5. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H36 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H37 has been replaced by "true". (It is already present, as
H27).
%%% Simplified C7 on reading formula in, to give:
%%% C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified C9 on reading formula in, to give:
%%% C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
*** Proved C1: year <= rr_type__rrsig_record_type__max_year
using hypothesis H1.
*** Proved C2: month <= 12
using hypothesis H2.
*** Proved C3: day <= 31
using hypothesis H3.
*** Proved C5: minute <= 59
using hypothesis H5.
*** Proved C6: second <= 59
using hypothesis H6.
*** Proved C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
using hypothesis H7.
*** Proved C8: true
*** Proved C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
using hypothesis H9.
*** Proved C10: loop__1__i + 1 >=
rr_type__rrsig_record_type__timestringtypeindex__first
using hypothesis H10.
*** Proved C12: loop__1__i + 1 >=
rr_type__rrsig_record_type__timestringtypeindex__first
using hypothesis H10.
-S- Applied substitution rule converttimes_rules(35).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__last by:
14.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> character__first <= element(timestring, [i___1]) and
element(timestring, [i___1]) <= character__last)
<S> New H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= 14 -> 48 <= element(timestring, [i_]) and element(timestring, [i_])
<= 57)
<S> New H11: loop__1__i <= 14
<S> New H43: not loop__1__i = 14
<S> New C11: loop__1__i <= 13
<S> New C13: loop__1__i <= 13
*** Proved C11: loop__1__i <= 13
using hypotheses H11 & H43.
*** Proved C13: loop__1__i <= 13
using hypotheses H11 & H43.
>>> Restructured hypothesis H18 into:
>>> H18: 4 < loop__1__i
>>> Restructured hypothesis H19 into:
>>> H19: 6 < loop__1__i
>>> Restructured hypothesis H20 into:
>>> H20: 8 < loop__1__i
>>> Restructured hypothesis H42 into:
>>> H42: year <= rr_type__rrsig_record_type__max_year and (month <=
monthsinayear and day <= maxdaysinamonth and 10 * hour + (element(
timestring, [loop__1__i]) - 48) < hoursinaday and minute <
minutesinanhour and second < secondsinaminute)
>>> Restructured hypothesis H43 into:
>>> H43: loop__1__i <> 14
--- Attempted addition of new hypothesis:
year <= rr_type__rrsig_record_type__max_year
eliminated: this already exists (as H1).
>>> Hypothesis H42 has now been split into two, giving:
>>> H1: year <= rr_type__rrsig_record_type__max_year
>>> H44: month <= monthsinayear and day <= maxdaysinamonth and 10 * hour
+ (element(timestring, [loop__1__i]) - 48) < hoursinaday and minute <
minutesinanhour and second < secondsinaminute
>>> Hypothesis H44 has now been split into two, giving:
>>> H45: month <= monthsinayear and day <= maxdaysinamonth and 10 * hour
+ (element(timestring, [loop__1__i]) - 48) < hoursinaday and minute <
minutesinanhour
>>> H46: second < secondsinaminute
>>> Hypothesis H45 has now been split into two, giving:
>>> H47: month <= monthsinayear and day <= maxdaysinamonth and 10 * hour
+ (element(timestring, [loop__1__i]) - 48) < hoursinaday
>>> H48: minute < minutesinanhour
>>> Hypothesis H47 has now been split into two, giving:
>>> H49: month <= monthsinayear and day <= maxdaysinamonth
>>> H50: 10 * hour + (element(timestring, [loop__1__i]) - 48) <
hoursinaday
>>> Hypothesis H49 has now been split into two, giving:
>>> H51: month <= monthsinayear
>>> H52: day <= maxdaysinamonth
-S- Applied substitution rule converttimes_rules(1).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__max_year by:
2020.
<S> New H1: year <= 2020
-S- Applied substitution rule converttimes_rules(2).
This was achieved by replacing all occurrences of secondsinaminute by:
60.
<S> New H46: second < 60
-S- Applied substitution rule converttimes_rules(3).
This was achieved by replacing all occurrences of minutesinanhour by:
60.
<S> New H48: minute < 60
-S- Applied substitution rule converttimes_rules(4).
This was achieved by replacing all occurrences of hoursinaday by:
24.
<S> New H50: 10 * hour + (element(timestring, [loop__1__i]) - 48) < 24
-S- Applied substitution rule converttimes_rules(5).
This was achieved by replacing all occurrences of maxdaysinamonth by:
31.
<S> New H52: day <= 31
-S- Applied substitution rule converttimes_rules(6).
This was achieved by replacing all occurrences of monthsinayear by:
12.
<S> New H51: month <= 12
-S- Applied substitution rule converttimes_rules(10).
This was achieved by replacing all occurrences of integer__base__first by:
- 2147483648.
<S> New H28: 10 * hour >= - 2147483648
-S- Applied substitution rule converttimes_rules(11).
This was achieved by replacing all occurrences of integer__base__last by:
2147483647.
<S> New H29: 10 * hour <= 2147483647
-S- Applied substitution rule converttimes_rules(13).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
-S- Applied substitution rule converttimes_rules(14).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= 255)
-S- Applied substitution rule converttimes_rules(18).
This was achieved by replacing all occurrences of natural__first by:
0.
<S> New H14: element(timestring, [loop__1__i]) >= 48
<S> New H22: hour >= 0
<S> New H26: 10 * hour + (element(timestring, [loop__1__i]) - 48) >= 0
<S> New H30: year >= 0
<S> New H32: month >= 0
<S> New H34: day >= 0
<S> New H38: minute >= 0
<S> New H40: second >= 0
-S- Applied substitution rule converttimes_rules(19).
This was achieved by replacing all occurrences of natural__last by:
2147483647.
<S> New H15: element(timestring, [loop__1__i]) <= 2147483695
<S> New H23: hour <= 2147483647
<S> New H27: 10 * hour + (element(timestring, [loop__1__i]) - 48) <=
2147483647
<S> New H31: year <= 2147483647
<S> New H33: month <= 2147483647
<S> New H35: day <= 2147483647
<S> New H39: minute <= 2147483647
<S> New H41: second <= 2147483647
-S- Applied substitution rule converttimes_rules(34).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__first by:
1.
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H10: loop__1__i >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <=
element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
%%% Hypotheses H11 & H43 together imply that
loop__1__i < 14.
H11 & H43 have therefore been deleted and a new H53 added to this effect.
*** Proved C4: 10 * hour + (element(timestring, [loop__1__i]) - 48) <= 23
using hypothesis H50.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_6. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H39 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H28).
%%% Simplified C7 on reading formula in, to give:
%%% C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified C9 on reading formula in, to give:
%%% C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
*** Proved C1: year <= rr_type__rrsig_record_type__max_year
using hypothesis H1.
*** Proved C2: month <= 12
using hypothesis H2.
*** Proved C3: day <= 31
using hypothesis H3.
*** Proved C4: hour <= 23
using hypothesis H4.
*** Proved C6: second <= 59
using hypothesis H6.
*** Proved C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
using hypothesis H7.
*** Proved C8: true
*** Proved C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
using hypothesis H9.
*** Proved C10: loop__1__i + 1 >=
rr_type__rrsig_record_type__timestringtypeindex__first
using hypothesis H10.
*** Proved C12: loop__1__i + 1 >=
rr_type__rrsig_record_type__timestringtypeindex__first
using hypothesis H10.
-S- Applied substitution rule converttimes_rules(35).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__last by:
14.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> character__first <= element(timestring, [i___1]) and
element(timestring, [i___1]) <= character__last)
<S> New H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= 14 -> 48 <= element(timestring, [i_]) and element(timestring, [i_])
<= 57)
<S> New H11: loop__1__i <= 14
<S> New H44: not loop__1__i = 14
<S> New C11: loop__1__i <= 13
<S> New C13: loop__1__i <= 13
*** Proved C11: loop__1__i <= 13
using hypotheses H11 & H44.
*** Proved C13: loop__1__i <= 13
using hypotheses H11 & H44.
>>> Restructured hypothesis H18 into:
>>> H18: 4 < loop__1__i
>>> Restructured hypothesis H19 into:
>>> H19: 6 < loop__1__i
>>> Restructured hypothesis H20 into:
>>> H20: 8 < loop__1__i
>>> Restructured hypothesis H21 into:
>>> H21: 10 < loop__1__i
>>> Restructured hypothesis H43 into:
>>> H43: year <= rr_type__rrsig_record_type__max_year and (month <=
monthsinayear and day <= maxdaysinamonth and hour < hoursinaday and
10 * minute + (element(timestring, [loop__1__i]) - 48) <
minutesinanhour and second < secondsinaminute)
>>> Restructured hypothesis H44 into:
>>> H44: loop__1__i <> 14
--- Attempted addition of new hypothesis:
year <= rr_type__rrsig_record_type__max_year
eliminated: this already exists (as H1).
>>> Hypothesis H43 has now been split into two, giving:
>>> H1: year <= rr_type__rrsig_record_type__max_year
>>> H45: month <= monthsinayear and day <= maxdaysinamonth and hour <
hoursinaday and 10 * minute + (element(timestring, [loop__1__i]) - 48)
< minutesinanhour and second < secondsinaminute
>>> Hypothesis H45 has now been split into two, giving:
>>> H46: month <= monthsinayear and day <= maxdaysinamonth and hour <
hoursinaday and 10 * minute + (element(timestring, [loop__1__i]) - 48)
< minutesinanhour
>>> H47: second < secondsinaminute
>>> Hypothesis H46 has now been split into two, giving:
>>> H48: month <= monthsinayear and day <= maxdaysinamonth and hour <
hoursinaday
>>> H49: 10 * minute + (element(timestring, [loop__1__i]) - 48) <
minutesinanhour
>>> Hypothesis H48 has now been split into two, giving:
>>> H50: month <= monthsinayear and day <= maxdaysinamonth
>>> H51: hour < hoursinaday
>>> Hypothesis H50 has now been split into two, giving:
>>> H52: month <= monthsinayear
>>> H53: day <= maxdaysinamonth
-S- Applied substitution rule converttimes_rules(1).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__max_year by:
2020.
<S> New H1: year <= 2020
-S- Applied substitution rule converttimes_rules(2).
This was achieved by replacing all occurrences of secondsinaminute by:
60.
<S> New H47: second < 60
-S- Applied substitution rule converttimes_rules(3).
This was achieved by replacing all occurrences of minutesinanhour by:
60.
<S> New H49: 10 * minute + (element(timestring, [loop__1__i]) - 48) < 60
-S- Applied substitution rule converttimes_rules(4).
This was achieved by replacing all occurrences of hoursinaday by:
24.
<S> New H51: hour < 24
-S- Applied substitution rule converttimes_rules(5).
This was achieved by replacing all occurrences of maxdaysinamonth by:
31.
<S> New H53: day <= 31
-S- Applied substitution rule converttimes_rules(6).
This was achieved by replacing all occurrences of monthsinayear by:
12.
<S> New H52: month <= 12
-S- Applied substitution rule converttimes_rules(10).
This was achieved by replacing all occurrences of integer__base__first by:
- 2147483648.
<S> New H29: 10 * minute >= - 2147483648
-S- Applied substitution rule converttimes_rules(11).
This was achieved by replacing all occurrences of integer__base__last by:
2147483647.
<S> New H30: 10 * minute <= 2147483647
-S- Applied substitution rule converttimes_rules(13).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
-S- Applied substitution rule converttimes_rules(14).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= 255)
-S- Applied substitution rule converttimes_rules(18).
This was achieved by replacing all occurrences of natural__first by:
0.
<S> New H14: element(timestring, [loop__1__i]) >= 48
<S> New H23: minute >= 0
<S> New H27: 10 * minute + (element(timestring, [loop__1__i]) - 48) >= 0
<S> New H31: year >= 0
<S> New H33: month >= 0
<S> New H35: day >= 0
<S> New H37: hour >= 0
<S> New H41: second >= 0
-S- Applied substitution rule converttimes_rules(19).
This was achieved by replacing all occurrences of natural__last by:
2147483647.
<S> New H15: element(timestring, [loop__1__i]) <= 2147483695
<S> New H24: minute <= 2147483647
<S> New H28: 10 * minute + (element(timestring, [loop__1__i]) - 48) <=
2147483647
<S> New H32: year <= 2147483647
<S> New H34: month <= 2147483647
<S> New H36: day <= 2147483647
<S> New H38: hour <= 2147483647
<S> New H42: second <= 2147483647
-S- Applied substitution rule converttimes_rules(34).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__first by:
1.
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H10: loop__1__i >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <=
element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
%%% Hypotheses H11 & H44 together imply that
loop__1__i < 14.
H11 & H44 have therefore been deleted and a new H54 added to this effect.
*** Proved C5: 10 * minute + (element(timestring, [loop__1__i]) - 48) <= 59
using hypothesis H49.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_7. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H27 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
%%% Simplified C7 on reading formula in, to give:
%%% C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified C9 on reading formula in, to give:
%%% C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
*** Proved C1: year <= rr_type__rrsig_record_type__max_year
using hypothesis H1.
*** Proved C2: month <= 12
using hypothesis H2.
*** Proved C3: day <= 31
using hypothesis H3.
*** Proved C4: hour <= 23
using hypothesis H4.
*** Proved C5: minute <= 59
using hypothesis H5.
*** Proved C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
using hypothesis H7.
*** Proved C8: true
*** Proved C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
using hypothesis H9.
*** Proved C10: loop__1__i + 1 >=
rr_type__rrsig_record_type__timestringtypeindex__first
using hypothesis H10.
*** Proved C12: loop__1__i + 1 >=
rr_type__rrsig_record_type__timestringtypeindex__first
using hypothesis H10.
-S- Applied substitution rule converttimes_rules(35).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__last by:
14.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> character__first <= element(timestring, [i___1]) and
element(timestring, [i___1]) <= character__last)
<S> New H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= 14 -> 48 <= element(timestring, [i_]) and element(timestring, [i_])
<= 57)
<S> New H11: loop__1__i <= 14
<S> New H45: not loop__1__i = 14
<S> New C11: loop__1__i <= 13
<S> New C13: loop__1__i <= 13
*** Proved C11: loop__1__i <= 13
using hypotheses H23 & H45.
*** Proved C13: loop__1__i <= 13
using hypotheses H23 & H45.
>>> Restructured hypothesis H18 into:
>>> H18: 4 < loop__1__i
>>> Restructured hypothesis H19 into:
>>> H19: 6 < loop__1__i
>>> Restructured hypothesis H20 into:
>>> H20: 8 < loop__1__i
>>> Restructured hypothesis H21 into:
>>> H21: 10 < loop__1__i
>>> Restructured hypothesis H22 into:
>>> H22: 12 < loop__1__i
>>> Restructured hypothesis H44 into:
>>> H44: year <= rr_type__rrsig_record_type__max_year and (month <=
monthsinayear and day <= maxdaysinamonth and hour < hoursinaday and
minute < minutesinanhour and 10 * second + (element(timestring, [
loop__1__i]) - 48) < secondsinaminute)
>>> Restructured hypothesis H45 into:
>>> H45: loop__1__i <> 14
--- Attempted addition of new hypothesis:
year <= rr_type__rrsig_record_type__max_year
eliminated: this already exists (as H1).
>>> Hypothesis H44 has now been split into two, giving:
>>> H1: year <= rr_type__rrsig_record_type__max_year
>>> H46: month <= monthsinayear and day <= maxdaysinamonth and hour <
hoursinaday and minute < minutesinanhour and 10 * second + (element(
timestring, [loop__1__i]) - 48) < secondsinaminute
>>> Hypothesis H46 has now been split into two, giving:
>>> H47: month <= monthsinayear and day <= maxdaysinamonth and hour <
hoursinaday and minute < minutesinanhour
>>> H48: 10 * second + (element(timestring, [loop__1__i]) - 48) <
secondsinaminute
>>> Hypothesis H47 has now been split into two, giving:
>>> H49: month <= monthsinayear and day <= maxdaysinamonth and hour <
hoursinaday
>>> H50: minute < minutesinanhour
>>> Hypothesis H49 has now been split into two, giving:
>>> H51: month <= monthsinayear and day <= maxdaysinamonth
>>> H52: hour < hoursinaday
>>> Hypothesis H51 has now been split into two, giving:
>>> H53: month <= monthsinayear
>>> H54: day <= maxdaysinamonth
-S- Applied substitution rule converttimes_rules(1).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__max_year by:
2020.
<S> New H1: year <= 2020
-S- Applied substitution rule converttimes_rules(2).
This was achieved by replacing all occurrences of secondsinaminute by:
60.
<S> New H48: 10 * second + (element(timestring, [loop__1__i]) - 48) < 60
-S- Applied substitution rule converttimes_rules(3).
This was achieved by replacing all occurrences of minutesinanhour by:
60.
<S> New H50: minute < 60
-S- Applied substitution rule converttimes_rules(4).
This was achieved by replacing all occurrences of hoursinaday by:
24.
<S> New H52: hour < 24
-S- Applied substitution rule converttimes_rules(5).
This was achieved by replacing all occurrences of maxdaysinamonth by:
31.
<S> New H54: day <= 31
-S- Applied substitution rule converttimes_rules(6).
This was achieved by replacing all occurrences of monthsinayear by:
12.
<S> New H53: month <= 12
-S- Applied substitution rule converttimes_rules(10).
This was achieved by replacing all occurrences of integer__base__first by:
- 2147483648.
<S> New H30: 10 * second >= - 2147483648
-S- Applied substitution rule converttimes_rules(11).
This was achieved by replacing all occurrences of integer__base__last by:
2147483647.
<S> New H31: 10 * second <= 2147483647
-S- Applied substitution rule converttimes_rules(13).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
-S- Applied substitution rule converttimes_rules(14).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> 0 <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= 255)
-S- Applied substitution rule converttimes_rules(18).
This was achieved by replacing all occurrences of natural__first by:
0.
<S> New H14: element(timestring, [loop__1__i]) >= 48
<S> New H24: second >= 0
<S> New H28: 10 * second + (element(timestring, [loop__1__i]) - 48) >= 0
<S> New H32: year >= 0
<S> New H34: month >= 0
<S> New H36: day >= 0
<S> New H38: hour >= 0
<S> New H40: minute >= 0
-S- Applied substitution rule converttimes_rules(19).
This was achieved by replacing all occurrences of natural__last by:
2147483647.
<S> New H15: element(timestring, [loop__1__i]) <= 2147483695
<S> New H25: second <= 2147483647
<S> New H29: 10 * second + (element(timestring, [loop__1__i]) - 48) <=
2147483647
<S> New H33: year <= 2147483647
<S> New H35: month <= 2147483647
<S> New H37: day <= 2147483647
<S> New H39: hour <= 2147483647
<S> New H41: minute <= 2147483647
-S- Applied substitution rule converttimes_rules(34).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__first by:
1.
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H10: loop__1__i >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <=
element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
%%% Hypotheses H11 & H45 together imply that
loop__1__i < 14.
H11 & H45 have therefore been deleted and a new H55 added to this effect.
*** Proved C6: 10 * second + (element(timestring, [loop__1__i]) - 48) <= 59
using hypothesis H48.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_8. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
%%% Simplified C7 on reading formula in, to give:
%%% C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified C9 on reading formula in, to give:
%%% C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
*** Proved C1: year <= rr_type__rrsig_record_type__max_year
using hypothesis H1.
*** Proved C2: month <= 12
using hypothesis H2.
*** Proved C3: day <= 31
using hypothesis H3.
*** Proved C4: hour <= 23
using hypothesis H4.
*** Proved C5: minute <= 59
using hypothesis H5.
*** Proved C6: second <= 59
using hypothesis H6.
*** Proved C7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
using hypothesis H7.
*** Proved C8: true
*** Proved C9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
using hypothesis H9.
*** Proved C10: loop__1__i + 1 >=
rr_type__rrsig_record_type__timestringtypeindex__first
using hypothesis H10.
*** Proved C12: loop__1__i + 1 >=
rr_type__rrsig_record_type__timestringtypeindex__first
using hypothesis H10.
-S- Applied substitution rule converttimes_rules(35).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__last by:
14.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= 14 -> character__first <= element(timestring, [i___1]) and
element(timestring, [i___1]) <= character__last)
<S> New H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= 14 -> 48 <= element(timestring, [i_]) and element(timestring, [i_])
<= 57)
<S> New H11: loop__1__i <= 14
<S> New H37: not loop__1__i = 14
<S> New C11: loop__1__i <= 13
<S> New C13: loop__1__i <= 13
*** Proved C11: loop__1__i <= 13
using hypotheses H11 & H37.
*** Proved C13: loop__1__i <= 13
using hypotheses H11 & H37.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_9. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
*** Proved C3: loop__1__i >=
rr_type__rrsig_record_type__timestringtypeindex__first
using hypothesis H10.
*** Proved C4: loop__1__i <=
rr_type__rrsig_record_type__timestringtypeindex__last
using hypothesis H11.
-S- Applied substitution rule converttimes_rules(18).
This was achieved by replacing all occurrences of natural__first by:
0.
<S> New C1: element(timestring, [loop__1__i]) >= 48
-S- Applied substitution rule converttimes_rules(19).
This was achieved by replacing all occurrences of natural__last by:
2147483647.
<S> New C2: element(timestring, [loop__1__i]) <= 2147483695
*** Proved C1: element(timestring, [loop__1__i]) >= 48
using hypotheses H9, H10 & H11.
*** Proved C2: element(timestring, [loop__1__i]) <= 2147483695
using hypotheses H9, H10 & H11.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_10. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H21 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H15).
-S- Applied substitution rule converttimes_rules(18).
This was achieved by replacing all occurrences of natural__first by:
0.
<S> New H14: element(timestring, [loop__1__i]) >= 48
<S> New H19: year >= 0
<S> New C1: 10 * year + (element(timestring, [loop__1__i]) - 48) >= 0
-S- Applied substitution rule converttimes_rules(19).
This was achieved by replacing all occurrences of natural__last by:
2147483647.
<S> New H15: element(timestring, [loop__1__i]) <= 2147483695
<S> New H20: year <= 2147483647
<S> New C2: 10 * year + (element(timestring, [loop__1__i]) - 48) <= 2147483647
-S- Applied substitution rule converttimes_rules(10).
This was achieved by replacing all occurrences of integer__base__first by:
- 2147483648.
<S> New C3: 10 * year >= - 2147483648
-S- Applied substitution rule converttimes_rules(11).
This was achieved by replacing all occurrences of integer__base__last by:
2147483647.
<S> New C4: 10 * year <= 2147483647
*** Proved C3: 10 * year >= - 2147483648
using hypothesis H19.
-S- Applied substitution rule converttimes_rules(1).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__max_year by:
2020.
<S> New H1: year <= 2020
-S- Applied substitution rule converttimes_rules(13).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0
<= element(timestring, [i___1]) and element(timestring, [i___1]) <=
character__last)
-S- Applied substitution rule converttimes_rules(14).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0
<= element(timestring, [i___1]) and element(timestring, [i___1]) <=
255)
-S- Applied substitution rule converttimes_rules(34).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__first by:
1.
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <=
rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H10: loop__1__i >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
rr_type__rrsig_record_type__timestringtypeindex__last -> 0 <= element(
timestring, [i___1]) and element(timestring, [i___1]) <= 255)
-S- Applied substitution rule converttimes_rules(35).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__last by:
14.
<S> New H11: loop__1__i <= 14
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <=
element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
*** Proved C1: 10 * year + (element(timestring, [loop__1__i]) - 48) >= 0
via its standard form, which is:
Std.Fm C1: - 48 + (10 * year + element(timestring, [loop__1__i])) >= 0
using hypotheses H14 & H19.
*** Proved C4: 10 * year <= 2147483647
using hypothesis H1.
--- Eliminated hypothesis H8 (true-hypothesis).
--- Eliminated hypothesis H12 (true-hypothesis).
--- Eliminated hypothesis H13 (true-hypothesis).
--- Eliminated hypothesis H16 (true-hypothesis).
--- Eliminated hypothesis H17 (true-hypothesis).
--- Eliminated hypothesis H21 (true-hypothesis).
--- Eliminated hypothesis H22 (true-hypothesis).
--- Eliminated hypothesis H11 (redundant, given H18).
--- Eliminated hypothesis H20 (redundant, given H1).
*** Proved C2: 10 * year + (element(timestring, [loop__1__i]) - 48) <=
2147483647
using hypotheses H1, H9, H10 & H11.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_11. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H15).
-S- Applied substitution rule converttimes_rules(18).
This was achieved by replacing all occurrences of natural__first by:
0.
<S> New H14: element(timestring, [loop__1__i]) >= 48
<S> New H20: month >= 0
<S> New C1: 10 * month + (element(timestring, [loop__1__i]) - 48) >= 0
-S- Applied substitution rule converttimes_rules(19).
This was achieved by replacing all occurrences of natural__last by:
2147483647.
<S> New H15: element(timestring, [loop__1__i]) <= 2147483695
<S> New H21: month <= 2147483647
<S> New C2: 10 * month + (element(timestring, [loop__1__i]) - 48) <=
2147483647
-S- Applied substitution rule converttimes_rules(10).
This was achieved by replacing all occurrences of integer__base__first by:
- 2147483648.
<S> New C3: 10 * month >= - 2147483648
-S- Applied substitution rule converttimes_rules(11).
This was achieved by replacing all occurrences of integer__base__last by:
2147483647.
<S> New C4: 10 * month <= 2147483647
*** Proved C3: 10 * month >= - 2147483648
using hypothesis H20.
*** Proved C4: 10 * month <= 2147483647
using hypothesis H2.
>>> Restructured hypothesis H18 into:
>>> H18: 4 < loop__1__i
-S- Applied substitution rule converttimes_rules(1).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__max_year by:
2020.
<S> New H1: year <= 2020
-S- Applied substitution rule converttimes_rules(13).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0
<= element(timestring, [i___1]) and element(timestring, [i___1]) <=
character__last)
-S- Applied substitution rule converttimes_rules(14).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0
<= element(timestring, [i___1]) and element(timestring, [i___1]) <=
255)
-S- Applied substitution rule converttimes_rules(34).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__first by:
1.
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <=
rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H10: loop__1__i >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
rr_type__rrsig_record_type__timestringtypeindex__last -> 0 <= element(
timestring, [i___1]) and element(timestring, [i___1]) <= 255)
-S- Applied substitution rule converttimes_rules(35).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__last by:
14.
<S> New H11: loop__1__i <= 14
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <=
element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
*** Proved C1: 10 * month + (element(timestring, [loop__1__i]) - 48) >= 0
via its standard form, which is:
Std.Fm C1: - 48 + (10 * month + element(timestring, [loop__1__i])) >= 0
using hypotheses H14 & H20.
--- Eliminated hypothesis H8 (true-hypothesis).
--- Eliminated hypothesis H12 (true-hypothesis).
--- Eliminated hypothesis H13 (true-hypothesis).
--- Eliminated hypothesis H16 (true-hypothesis).
--- Eliminated hypothesis H17 (true-hypothesis).
--- Eliminated hypothesis H22 (true-hypothesis).
--- Eliminated hypothesis H23 (true-hypothesis).
--- Eliminated hypothesis H10 (redundant, given H18).
--- Eliminated hypothesis H11 (redundant, given H19).
--- Eliminated hypothesis H21 (redundant, given H2).
*** Proved C2: 10 * month + (element(timestring, [loop__1__i]) - 48) <=
2147483647
using hypotheses H2, H9, H10 & H11.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_12. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H15).
-S- Applied substitution rule converttimes_rules(18).
This was achieved by replacing all occurrences of natural__first by:
0.
<S> New H14: element(timestring, [loop__1__i]) >= 48
<S> New H21: day >= 0
<S> New C1: 10 * day + (element(timestring, [loop__1__i]) - 48) >= 0
-S- Applied substitution rule converttimes_rules(19).
This was achieved by replacing all occurrences of natural__last by:
2147483647.
<S> New H15: element(timestring, [loop__1__i]) <= 2147483695
<S> New H22: day <= 2147483647
<S> New C2: 10 * day + (element(timestring, [loop__1__i]) - 48) <= 2147483647
-S- Applied substitution rule converttimes_rules(10).
This was achieved by replacing all occurrences of integer__base__first by:
- 2147483648.
<S> New C3: 10 * day >= - 2147483648
-S- Applied substitution rule converttimes_rules(11).
This was achieved by replacing all occurrences of integer__base__last by:
2147483647.
<S> New C4: 10 * day <= 2147483647
*** Proved C3: 10 * day >= - 2147483648
using hypothesis H21.
*** Proved C4: 10 * day <= 2147483647
using hypothesis H3.
>>> Restructured hypothesis H18 into:
>>> H18: 4 < loop__1__i
>>> Restructured hypothesis H19 into:
>>> H19: 6 < loop__1__i
-S- Applied substitution rule converttimes_rules(1).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__max_year by:
2020.
<S> New H1: year <= 2020
-S- Applied substitution rule converttimes_rules(13).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0
<= element(timestring, [i___1]) and element(timestring, [i___1]) <=
character__last)
-S- Applied substitution rule converttimes_rules(14).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0
<= element(timestring, [i___1]) and element(timestring, [i___1]) <=
255)
-S- Applied substitution rule converttimes_rules(34).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__first by:
1.
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <=
rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H10: loop__1__i >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
rr_type__rrsig_record_type__timestringtypeindex__last -> 0 <= element(
timestring, [i___1]) and element(timestring, [i___1]) <= 255)
-S- Applied substitution rule converttimes_rules(35).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__last by:
14.
<S> New H11: loop__1__i <= 14
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <=
element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
*** Proved C1: 10 * day + (element(timestring, [loop__1__i]) - 48) >= 0
via its standard form, which is:
Std.Fm C1: - 48 + (10 * day + element(timestring, [loop__1__i])) >= 0
using hypotheses H14 & H21.
--- Eliminated hypothesis H8 (true-hypothesis).
--- Eliminated hypothesis H12 (true-hypothesis).
--- Eliminated hypothesis H13 (true-hypothesis).
--- Eliminated hypothesis H16 (true-hypothesis).
--- Eliminated hypothesis H17 (true-hypothesis).
--- Eliminated hypothesis H23 (true-hypothesis).
--- Eliminated hypothesis H24 (true-hypothesis).
--- Eliminated hypothesis H10 (redundant, given H18).
--- Eliminated hypothesis H11 (redundant, given H20).
--- Eliminated hypothesis H18 (redundant, given H19).
--- Eliminated hypothesis H22 (redundant, given H3).
*** Proved C2: 10 * day + (element(timestring, [loop__1__i]) - 48) <=
2147483647
using hypotheses H3, H9, H10 & H11.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_13. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H15).
-S- Applied substitution rule converttimes_rules(18).
This was achieved by replacing all occurrences of natural__first by:
0.
<S> New H14: element(timestring, [loop__1__i]) >= 48
<S> New H22: hour >= 0
<S> New C1: 10 * hour + (element(timestring, [loop__1__i]) - 48) >= 0
-S- Applied substitution rule converttimes_rules(19).
This was achieved by replacing all occurrences of natural__last by:
2147483647.
<S> New H15: element(timestring, [loop__1__i]) <= 2147483695
<S> New H23: hour <= 2147483647
<S> New C2: 10 * hour + (element(timestring, [loop__1__i]) - 48) <= 2147483647
-S- Applied substitution rule converttimes_rules(10).
This was achieved by replacing all occurrences of integer__base__first by:
- 2147483648.
<S> New C3: 10 * hour >= - 2147483648
-S- Applied substitution rule converttimes_rules(11).
This was achieved by replacing all occurrences of integer__base__last by:
2147483647.
<S> New C4: 10 * hour <= 2147483647
*** Proved C3: 10 * hour >= - 2147483648
using hypothesis H22.
*** Proved C4: 10 * hour <= 2147483647
using hypothesis H4.
>>> Restructured hypothesis H18 into:
>>> H18: 4 < loop__1__i
>>> Restructured hypothesis H19 into:
>>> H19: 6 < loop__1__i
>>> Restructured hypothesis H20 into:
>>> H20: 8 < loop__1__i
-S- Applied substitution rule converttimes_rules(1).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__max_year by:
2020.
<S> New H1: year <= 2020
-S- Applied substitution rule converttimes_rules(13).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0
<= element(timestring, [i___1]) and element(timestring, [i___1]) <=
character__last)
-S- Applied substitution rule converttimes_rules(14).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0
<= element(timestring, [i___1]) and element(timestring, [i___1]) <=
255)
-S- Applied substitution rule converttimes_rules(34).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__first by:
1.
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <=
rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H10: loop__1__i >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
rr_type__rrsig_record_type__timestringtypeindex__last -> 0 <= element(
timestring, [i___1]) and element(timestring, [i___1]) <= 255)
-S- Applied substitution rule converttimes_rules(35).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__last by:
14.
<S> New H11: loop__1__i <= 14
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <=
element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
*** Proved C1: 10 * hour + (element(timestring, [loop__1__i]) - 48) >= 0
via its standard form, which is:
Std.Fm C1: - 48 + (10 * hour + element(timestring, [loop__1__i])) >= 0
using hypotheses H14 & H22.
--- Eliminated hypothesis H8 (true-hypothesis).
--- Eliminated hypothesis H12 (true-hypothesis).
--- Eliminated hypothesis H13 (true-hypothesis).
--- Eliminated hypothesis H16 (true-hypothesis).
--- Eliminated hypothesis H17 (true-hypothesis).
--- Eliminated hypothesis H24 (true-hypothesis).
--- Eliminated hypothesis H25 (true-hypothesis).
--- Eliminated hypothesis H10 (redundant, given H18).
--- Eliminated hypothesis H11 (redundant, given H21).
--- Eliminated hypothesis H18 (redundant, given H19).
--- Eliminated hypothesis H19 (redundant, given H20).
--- Eliminated hypothesis H23 (redundant, given H4).
*** Proved C2: 10 * hour + (element(timestring, [loop__1__i]) - 48) <=
2147483647
using hypotheses H4, H9, H10 & H11.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_14. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H15).
-S- Applied substitution rule converttimes_rules(18).
This was achieved by replacing all occurrences of natural__first by:
0.
<S> New H14: element(timestring, [loop__1__i]) >= 48
<S> New H23: minute >= 0
<S> New C1: 10 * minute + (element(timestring, [loop__1__i]) - 48) >= 0
-S- Applied substitution rule converttimes_rules(19).
This was achieved by replacing all occurrences of natural__last by:
2147483647.
<S> New H15: element(timestring, [loop__1__i]) <= 2147483695
<S> New H24: minute <= 2147483647
<S> New C2: 10 * minute + (element(timestring, [loop__1__i]) - 48) <=
2147483647
-S- Applied substitution rule converttimes_rules(10).
This was achieved by replacing all occurrences of integer__base__first by:
- 2147483648.
<S> New C3: 10 * minute >= - 2147483648
-S- Applied substitution rule converttimes_rules(11).
This was achieved by replacing all occurrences of integer__base__last by:
2147483647.
<S> New C4: 10 * minute <= 2147483647
*** Proved C3: 10 * minute >= - 2147483648
using hypothesis H23.
*** Proved C4: 10 * minute <= 2147483647
using hypothesis H5.
>>> Restructured hypothesis H18 into:
>>> H18: 4 < loop__1__i
>>> Restructured hypothesis H19 into:
>>> H19: 6 < loop__1__i
>>> Restructured hypothesis H20 into:
>>> H20: 8 < loop__1__i
>>> Restructured hypothesis H21 into:
>>> H21: 10 < loop__1__i
-S- Applied substitution rule converttimes_rules(1).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__max_year by:
2020.
<S> New H1: year <= 2020
-S- Applied substitution rule converttimes_rules(13).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0
<= element(timestring, [i___1]) and element(timestring, [i___1]) <=
character__last)
-S- Applied substitution rule converttimes_rules(14).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0
<= element(timestring, [i___1]) and element(timestring, [i___1]) <=
255)
-S- Applied substitution rule converttimes_rules(34).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__first by:
1.
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <=
rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H10: loop__1__i >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
rr_type__rrsig_record_type__timestringtypeindex__last -> 0 <= element(
timestring, [i___1]) and element(timestring, [i___1]) <= 255)
-S- Applied substitution rule converttimes_rules(35).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__last by:
14.
<S> New H11: loop__1__i <= 14
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <=
element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
*** Proved C1: 10 * minute + (element(timestring, [loop__1__i]) - 48) >= 0
via its standard form, which is:
Std.Fm C1: - 48 + (10 * minute + element(timestring, [loop__1__i])) >= 0
using hypotheses H14 & H23.
--- Eliminated hypothesis H8 (true-hypothesis).
--- Eliminated hypothesis H12 (true-hypothesis).
--- Eliminated hypothesis H13 (true-hypothesis).
--- Eliminated hypothesis H16 (true-hypothesis).
--- Eliminated hypothesis H17 (true-hypothesis).
--- Eliminated hypothesis H25 (true-hypothesis).
--- Eliminated hypothesis H26 (true-hypothesis).
--- Eliminated hypothesis H10 (redundant, given H18).
--- Eliminated hypothesis H11 (redundant, given H22).
--- Eliminated hypothesis H18 (redundant, given H19).
--- Eliminated hypothesis H19 (redundant, given H20).
--- Eliminated hypothesis H20 (redundant, given H21).
--- Eliminated hypothesis H24 (redundant, given H5).
*** Proved C2: 10 * minute + (element(timestring, [loop__1__i]) - 48) <=
2147483647
using hypotheses H5, H9, H10 & H11.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_15. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H27 has been replaced by "true". (It is already present, as
H15).
-S- Applied substitution rule converttimes_rules(18).
This was achieved by replacing all occurrences of natural__first by:
0.
<S> New H14: element(timestring, [loop__1__i]) >= 48
<S> New H24: second >= 0
<S> New C1: 10 * second + (element(timestring, [loop__1__i]) - 48) >= 0
-S- Applied substitution rule converttimes_rules(19).
This was achieved by replacing all occurrences of natural__last by:
2147483647.
<S> New H15: element(timestring, [loop__1__i]) <= 2147483695
<S> New H25: second <= 2147483647
<S> New C2: 10 * second + (element(timestring, [loop__1__i]) - 48) <=
2147483647
-S- Applied substitution rule converttimes_rules(10).
This was achieved by replacing all occurrences of integer__base__first by:
- 2147483648.
<S> New C3: 10 * second >= - 2147483648
-S- Applied substitution rule converttimes_rules(11).
This was achieved by replacing all occurrences of integer__base__last by:
2147483647.
<S> New C4: 10 * second <= 2147483647
*** Proved C3: 10 * second >= - 2147483648
using hypothesis H24.
*** Proved C4: 10 * second <= 2147483647
using hypothesis H6.
>>> Restructured hypothesis H18 into:
>>> H18: 4 < loop__1__i
>>> Restructured hypothesis H19 into:
>>> H19: 6 < loop__1__i
>>> Restructured hypothesis H20 into:
>>> H20: 8 < loop__1__i
>>> Restructured hypothesis H21 into:
>>> H21: 10 < loop__1__i
>>> Restructured hypothesis H22 into:
>>> H22: 12 < loop__1__i
-S- Applied substitution rule converttimes_rules(1).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__max_year by:
2020.
<S> New H1: year <= 2020
-S- Applied substitution rule converttimes_rules(13).
This was achieved by replacing all occurrences of character__first by:
0.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0
<= element(timestring, [i___1]) and element(timestring, [i___1]) <=
character__last)
-S- Applied substitution rule converttimes_rules(14).
This was achieved by replacing all occurrences of character__last by:
255.
<S> New H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last -> 0
<= element(timestring, [i___1]) and element(timestring, [i___1]) <=
255)
-S- Applied substitution rule converttimes_rules(34).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__first by:
1.
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <=
rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H10: loop__1__i >= 1
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <=
rr_type__rrsig_record_type__timestringtypeindex__last -> 0 <= element(
timestring, [i___1]) and element(timestring, [i___1]) <= 255)
-S- Applied substitution rule converttimes_rules(35).
This was achieved by replacing all occurrences of
rr_type__rrsig_record_type__timestringtypeindex__last by:
14.
<S> New H11: loop__1__i <= 14
<S> New H9: for_all(i_ : integer, 1 <= i_ and i_ <= 14 -> 48 <= element(
timestring, [i_]) and element(timestring, [i_]) <= 57)
<S> New H7: for_all(i___1 : integer, 1 <= i___1 and i___1 <= 14 -> 0 <=
element(timestring, [i___1]) and element(timestring, [i___1]) <= 255)
*** Proved C1: 10 * second + (element(timestring, [loop__1__i]) - 48) >= 0
via its standard form, which is:
Std.Fm C1: - 48 + (10 * second + element(timestring, [loop__1__i])) >= 0
using hypotheses H14 & H24.
--- Eliminated hypothesis H8 (true-hypothesis).
--- Eliminated hypothesis H12 (true-hypothesis).
--- Eliminated hypothesis H13 (true-hypothesis).
--- Eliminated hypothesis H16 (true-hypothesis).
--- Eliminated hypothesis H17 (true-hypothesis).
--- Eliminated hypothesis H26 (true-hypothesis).
--- Eliminated hypothesis H27 (true-hypothesis).
--- Eliminated hypothesis H23 (duplicate of H11).
--- Eliminated hypothesis H10 (redundant, given H18).
--- Eliminated hypothesis H18 (redundant, given H19).
--- Eliminated hypothesis H19 (redundant, given H20).
--- Eliminated hypothesis H20 (redundant, given H21).
--- Eliminated hypothesis H21 (redundant, given H22).
--- Eliminated hypothesis H25 (redundant, given H6).
*** Proved C2: 10 * second + (element(timestring, [loop__1__i]) - 48) <=
2147483647
using hypotheses H6, H9, H10 & H23.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_16. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H21 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H27 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H28 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H41 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H39).
-S- Applied substitution rule converttimes_rules(28).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New C1: true
-S- Applied substitution rule converttimes_rules(29).
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_converttimestring_17. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H30 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H31 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H41 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H40).
-S- Applied substitution rule converttimes_rules(28).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New C1: true
-S- Applied substitution rule converttimes_rules(29).
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_converttimestring_18. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H33 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H34 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H41).
-S- Applied substitution rule converttimes_rules(28).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New C1: true
-S- Applied substitution rule converttimes_rules(29).
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_converttimestring_19. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H36 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H37 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H42).
-S- Applied substitution rule converttimes_rules(28).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New C1: true
-S- Applied substitution rule converttimes_rules(29).
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_converttimestring_20. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H39 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H42).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H43).
-S- Applied substitution rule converttimes_rules(28).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New C1: true
-S- Applied substitution rule converttimes_rules(29).
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_converttimestring_21. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H27 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H44).
-S- Applied substitution rule converttimes_rules(28).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New C1: true
-S- Applied substitution rule converttimes_rules(29).
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_converttimestring_22. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H37 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H38 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H39 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H41 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
-S- Applied substitution rule converttimes_rules(28).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New C1: true
-S- Applied substitution rule converttimes_rules(29).
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_converttimestring_23. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H21 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H27 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H28 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H41 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
-S- Applied substitution rule converttimes_rules(28).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New C1: true
-S- Applied substitution rule converttimes_rules(29).
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_converttimestring_24. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H30 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H31 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H39).
-S- Applied substitution rule converttimes_rules(28).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New C1: true
-S- Applied substitution rule converttimes_rules(29).
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_converttimestring_25. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H33 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H34 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H40).
-S- Applied substitution rule converttimes_rules(28).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New C1: true
-S- Applied substitution rule converttimes_rules(29).
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_converttimestring_26. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H36 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H37 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H41).
-S- Applied substitution rule converttimes_rules(28).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New C1: true
-S- Applied substitution rule converttimes_rules(29).
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_converttimestring_27. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H39 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H42).
-S- Applied substitution rule converttimes_rules(28).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New C1: true
-S- Applied substitution rule converttimes_rules(29).
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_converttimestring_28. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H27 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H29).
-S- Applied substitution rule converttimes_rules(28).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New C1: true
-S- Applied substitution rule converttimes_rules(29).
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_converttimestring_29. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H38 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H39 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H41 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
-S- Applied substitution rule converttimes_rules(28).
This was achieved by replacing all occurrences of
unsigned_types__unsigned32__first by:
0.
<S> New C1: true
-S- Applied substitution rule converttimes_rules(29).
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_converttimestring_30. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H21 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H27 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H28 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H41 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H38).
*** Proved C1: second >= natural__first
using hypothesis H37.
*** Proved C2: second <= natural__last
using hypothesis H38.
*** Proved C3: minute >= natural__first
using hypothesis H35.
*** Proved C4: minute <= natural__last
using hypothesis H36.
*** Proved C5: hour >= natural__first
using hypothesis H33.
*** Proved C6: hour <= natural__last
using hypothesis H34.
*** Proved C7: day >= natural__first
using hypothesis H31.
*** Proved C8: day <= natural__last
using hypothesis H32.
*** Proved C9: month >= natural__first
using hypothesis H29.
*** Proved C10: month <= natural__last
using hypothesis H30.
*** Proved C11: 10 * year + (element(timestring, [loop__1__i]) - 48) >=
natural__first
using hypothesis H23.
*** Proved C12: 10 * year + (element(timestring, [loop__1__i]) - 48) <=
natural__last
using hypothesis H24.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_31. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H30 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H31 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H41 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H39).
*** Proved C1: second >= natural__first
using hypothesis H38.
*** Proved C2: second <= natural__last
using hypothesis H39.
*** Proved C3: minute >= natural__first
using hypothesis H36.
*** Proved C4: minute <= natural__last
using hypothesis H37.
*** Proved C5: hour >= natural__first
using hypothesis H34.
*** Proved C6: hour <= natural__last
using hypothesis H35.
*** Proved C7: day >= natural__first
using hypothesis H32.
*** Proved C8: day <= natural__last
using hypothesis H33.
*** Proved C9: 10 * month + (element(timestring, [loop__1__i]) - 48) >=
natural__first
using hypothesis H24.
*** Proved C10: 10 * month + (element(timestring, [loop__1__i]) - 48) <=
natural__last
using hypothesis H25.
*** Proved C11: year >= natural__first
using hypothesis H28.
*** Proved C12: year <= natural__last
using hypothesis H29.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_32. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H33 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H34 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H40).
*** Proved C1: second >= natural__first
using hypothesis H39.
*** Proved C2: second <= natural__last
using hypothesis H40.
*** Proved C3: minute >= natural__first
using hypothesis H37.
*** Proved C4: minute <= natural__last
using hypothesis H38.
*** Proved C5: hour >= natural__first
using hypothesis H35.
*** Proved C6: hour <= natural__last
using hypothesis H36.
*** Proved C7: 10 * day + (element(timestring, [loop__1__i]) - 48) >=
natural__first
using hypothesis H25.
*** Proved C8: 10 * day + (element(timestring, [loop__1__i]) - 48) <=
natural__last
using hypothesis H26.
*** Proved C9: month >= natural__first
using hypothesis H31.
*** Proved C10: month <= natural__last
using hypothesis H32.
*** Proved C11: year >= natural__first
using hypothesis H29.
*** Proved C12: year <= natural__last
using hypothesis H30.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_33. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H36 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H37 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H41).
*** Proved C1: second >= natural__first
using hypothesis H40.
*** Proved C2: second <= natural__last
using hypothesis H41.
*** Proved C3: minute >= natural__first
using hypothesis H38.
*** Proved C4: minute <= natural__last
using hypothesis H39.
*** Proved C5: 10 * hour + (element(timestring, [loop__1__i]) - 48) >=
natural__first
using hypothesis H26.
*** Proved C6: 10 * hour + (element(timestring, [loop__1__i]) - 48) <=
natural__last
using hypothesis H27.
*** Proved C7: day >= natural__first
using hypothesis H34.
*** Proved C8: day <= natural__last
using hypothesis H35.
*** Proved C9: month >= natural__first
using hypothesis H32.
*** Proved C10: month <= natural__last
using hypothesis H33.
*** Proved C11: year >= natural__first
using hypothesis H30.
*** Proved C12: year <= natural__last
using hypothesis H31.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_34. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H39 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H42).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H42).
*** Proved C1: second >= natural__first
using hypothesis H41.
*** Proved C2: second <= natural__last
using hypothesis H42.
*** Proved C3: 10 * minute + (element(timestring, [loop__1__i]) - 48) >=
natural__first
using hypothesis H27.
*** Proved C4: 10 * minute + (element(timestring, [loop__1__i]) - 48) <=
natural__last
using hypothesis H28.
*** Proved C5: hour >= natural__first
using hypothesis H37.
*** Proved C6: hour <= natural__last
using hypothesis H38.
*** Proved C7: day >= natural__first
using hypothesis H35.
*** Proved C8: day <= natural__last
using hypothesis H36.
*** Proved C9: month >= natural__first
using hypothesis H33.
*** Proved C10: month <= natural__last
using hypothesis H34.
*** Proved C11: year >= natural__first
using hypothesis H31.
*** Proved C12: year <= natural__last
using hypothesis H32.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_35. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H27 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H29).
*** Proved C1: 10 * second + (element(timestring, [loop__1__i]) - 48) >=
natural__first
using hypothesis H28.
*** Proved C2: 10 * second + (element(timestring, [loop__1__i]) - 48) <=
natural__last
using hypothesis H29.
*** Proved C3: minute >= natural__first
using hypothesis H40.
*** Proved C4: minute <= natural__last
using hypothesis H41.
*** Proved C5: hour >= natural__first
using hypothesis H38.
*** Proved C6: hour <= natural__last
using hypothesis H39.
*** Proved C7: day >= natural__first
using hypothesis H36.
*** Proved C8: day <= natural__last
using hypothesis H37.
*** Proved C9: month >= natural__first
using hypothesis H34.
*** Proved C10: month <= natural__last
using hypothesis H35.
*** Proved C11: year >= natural__first
using hypothesis H32.
*** Proved C12: year <= natural__last
using hypothesis H33.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_36. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H37 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H38 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H39 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H41 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H35).
*** Proved C1: second >= natural__first
using hypothesis H34.
*** Proved C2: second <= natural__last
using hypothesis H35.
*** Proved C3: minute >= natural__first
using hypothesis H32.
*** Proved C4: minute <= natural__last
using hypothesis H33.
*** Proved C5: hour >= natural__first
using hypothesis H30.
*** Proved C6: hour <= natural__last
using hypothesis H31.
*** Proved C7: day >= natural__first
using hypothesis H28.
*** Proved C8: day <= natural__last
using hypothesis H29.
*** Proved C9: month >= natural__first
using hypothesis H26.
*** Proved C10: month <= natural__last
using hypothesis H27.
*** Proved C11: year >= natural__first
using hypothesis H24.
*** Proved C12: year <= natural__last
using hypothesis H25.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_37. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H21 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H27 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H28 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H41 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H38).
*** Proved C1: second >= natural__first
using hypothesis H37.
*** Proved C2: second <= natural__last
using hypothesis H38.
*** Proved C3: minute >= natural__first
using hypothesis H35.
*** Proved C4: minute <= natural__last
using hypothesis H36.
*** Proved C5: hour >= natural__first
using hypothesis H33.
*** Proved C6: hour <= natural__last
using hypothesis H34.
*** Proved C7: day >= natural__first
using hypothesis H31.
*** Proved C8: day <= natural__last
using hypothesis H32.
*** Proved C9: month >= natural__first
using hypothesis H29.
*** Proved C10: month <= natural__last
using hypothesis H30.
*** Proved C11: 10 * year + (element(timestring, [loop__1__i]) - 48) >=
natural__first
using hypothesis H23.
*** Proved C12: 10 * year + (element(timestring, [loop__1__i]) - 48) <=
natural__last
using hypothesis H24.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_38. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H30 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H31 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H39).
*** Proved C1: second >= natural__first
using hypothesis H38.
*** Proved C2: second <= natural__last
using hypothesis H39.
*** Proved C3: minute >= natural__first
using hypothesis H36.
*** Proved C4: minute <= natural__last
using hypothesis H37.
*** Proved C5: hour >= natural__first
using hypothesis H34.
*** Proved C6: hour <= natural__last
using hypothesis H35.
*** Proved C7: day >= natural__first
using hypothesis H32.
*** Proved C8: day <= natural__last
using hypothesis H33.
*** Proved C9: 10 * month + (element(timestring, [loop__1__i]) - 48) >=
natural__first
using hypothesis H24.
*** Proved C10: 10 * month + (element(timestring, [loop__1__i]) - 48) <=
natural__last
using hypothesis H25.
*** Proved C11: year >= natural__first
using hypothesis H28.
*** Proved C12: year <= natural__last
using hypothesis H29.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_39. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H33 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H34 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H40).
*** Proved C1: second >= natural__first
using hypothesis H39.
*** Proved C2: second <= natural__last
using hypothesis H40.
*** Proved C3: minute >= natural__first
using hypothesis H37.
*** Proved C4: minute <= natural__last
using hypothesis H38.
*** Proved C5: hour >= natural__first
using hypothesis H35.
*** Proved C6: hour <= natural__last
using hypothesis H36.
*** Proved C7: 10 * day + (element(timestring, [loop__1__i]) - 48) >=
natural__first
using hypothesis H25.
*** Proved C8: 10 * day + (element(timestring, [loop__1__i]) - 48) <=
natural__last
using hypothesis H26.
*** Proved C9: month >= natural__first
using hypothesis H31.
*** Proved C10: month <= natural__last
using hypothesis H32.
*** Proved C11: year >= natural__first
using hypothesis H29.
*** Proved C12: year <= natural__last
using hypothesis H30.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_40. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H36 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H37 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H42).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H41).
*** Proved C1: second >= natural__first
using hypothesis H40.
*** Proved C2: second <= natural__last
using hypothesis H41.
*** Proved C3: minute >= natural__first
using hypothesis H38.
*** Proved C4: minute <= natural__last
using hypothesis H39.
*** Proved C5: 10 * hour + (element(timestring, [loop__1__i]) - 48) >=
natural__first
using hypothesis H26.
*** Proved C6: 10 * hour + (element(timestring, [loop__1__i]) - 48) <=
natural__last
using hypothesis H27.
*** Proved C7: day >= natural__first
using hypothesis H34.
*** Proved C8: day <= natural__last
using hypothesis H35.
*** Proved C9: month >= natural__first
using hypothesis H32.
*** Proved C10: month <= natural__last
using hypothesis H33.
*** Proved C11: year >= natural__first
using hypothesis H30.
*** Proved C12: year <= natural__last
using hypothesis H31.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_41. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H39 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H42).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H43).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H42).
*** Proved C1: second >= natural__first
using hypothesis H41.
*** Proved C2: second <= natural__last
using hypothesis H42.
*** Proved C3: 10 * minute + (element(timestring, [loop__1__i]) - 48) >=
natural__first
using hypothesis H27.
*** Proved C4: 10 * minute + (element(timestring, [loop__1__i]) - 48) <=
natural__last
using hypothesis H28.
*** Proved C5: hour >= natural__first
using hypothesis H37.
*** Proved C6: hour <= natural__last
using hypothesis H38.
*** Proved C7: day >= natural__first
using hypothesis H35.
*** Proved C8: day <= natural__last
using hypothesis H36.
*** Proved C9: month >= natural__first
using hypothesis H33.
*** Proved C10: month <= natural__last
using hypothesis H34.
*** Proved C11: year >= natural__first
using hypothesis H31.
*** Proved C12: year <= natural__last
using hypothesis H32.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_42. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H27 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H44).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H70 has been replaced by "true". (It is already present, as
H29).
*** Proved C1: 10 * second + (element(timestring, [loop__1__i]) - 48) >=
natural__first
using hypothesis H28.
*** Proved C2: 10 * second + (element(timestring, [loop__1__i]) - 48) <=
natural__last
using hypothesis H29.
*** Proved C3: minute >= natural__first
using hypothesis H40.
*** Proved C4: minute <= natural__last
using hypothesis H41.
*** Proved C5: hour >= natural__first
using hypothesis H38.
*** Proved C6: hour <= natural__last
using hypothesis H39.
*** Proved C7: day >= natural__first
using hypothesis H36.
*** Proved C8: day <= natural__last
using hypothesis H37.
*** Proved C9: month >= natural__first
using hypothesis H34.
*** Proved C10: month <= natural__last
using hypothesis H35.
*** Proved C11: year >= natural__first
using hypothesis H32.
*** Proved C12: year <= natural__last
using hypothesis H33.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_43. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H38 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H39 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H41 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H35).
*** Proved C1: second >= natural__first
using hypothesis H34.
*** Proved C2: second <= natural__last
using hypothesis H35.
*** Proved C3: minute >= natural__first
using hypothesis H32.
*** Proved C4: minute <= natural__last
using hypothesis H33.
*** Proved C5: hour >= natural__first
using hypothesis H30.
*** Proved C6: hour <= natural__last
using hypothesis H31.
*** Proved C7: day >= natural__first
using hypothesis H28.
*** Proved C8: day <= natural__last
using hypothesis H29.
*** Proved C9: month >= natural__first
using hypothesis H26.
*** Proved C10: month <= natural__last
using hypothesis H27.
*** Proved C11: year >= natural__first
using hypothesis H24.
*** Proved C12: year <= natural__last
using hypothesis H25.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_44. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H21 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H27 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H28 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H41 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H70 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H71 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H72 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H73 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H74 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H75 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H76 has been replaced by "true". (It is already present, as
H24).
*** Proved C1: non_spark_stuff__time_of(10 * year + (element(timestring, [
loop__1__i]) - 48), month, day, hour, minute, second) >=
unsigned_types__unsigned32__first
using hypothesis H77.
*** Proved C2: non_spark_stuff__time_of(10 * year + (element(timestring, [
loop__1__i]) - 48), month, day, hour, minute, second) <=
unsigned_types__unsigned32__last
using hypothesis H78.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_45. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H30 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H31 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H41 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H70 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H71 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H72 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H73 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H74 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H75 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H76 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H77 has been replaced by "true". (It is already present, as
H29).
*** Proved C1: non_spark_stuff__time_of(year, 10 * month + (element(
timestring, [loop__1__i]) - 48), day, hour, minute, second) >=
unsigned_types__unsigned32__first
using hypothesis H78.
*** Proved C2: non_spark_stuff__time_of(year, 10 * month + (element(
timestring, [loop__1__i]) - 48), day, hour, minute, second) <=
unsigned_types__unsigned32__last
using hypothesis H79.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_46. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H33 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H34 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H70 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H71 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H72 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H73 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H74 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H75 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H76 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H77 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H78 has been replaced by "true". (It is already present, as
H30).
*** Proved C1: non_spark_stuff__time_of(year, month, 10 * day + (element(
timestring, [loop__1__i]) - 48), hour, minute, second) >=
unsigned_types__unsigned32__first
using hypothesis H79.
*** Proved C2: non_spark_stuff__time_of(year, month, 10 * day + (element(
timestring, [loop__1__i]) - 48), hour, minute, second) <=
unsigned_types__unsigned32__last
using hypothesis H80.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_47. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H36 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H37 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H70 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H71 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H72 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H73 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H74 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H75 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H76 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H77 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H78 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H79 has been replaced by "true". (It is already present, as
H31).
*** Proved C1: non_spark_stuff__time_of(year, month, day, 10 * hour + (
element(timestring, [loop__1__i]) - 48), minute, second) >=
unsigned_types__unsigned32__first
using hypothesis H80.
*** Proved C2: non_spark_stuff__time_of(year, month, day, 10 * hour + (
element(timestring, [loop__1__i]) - 48), minute, second) <=
unsigned_types__unsigned32__last
using hypothesis H81.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_48. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H39 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H42).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H42).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H70 has been replaced by "true". (It is already present, as
H42).
--- Hypothesis H71 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H72 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H73 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H74 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H75 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H76 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H77 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H78 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H79 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H80 has been replaced by "true". (It is already present, as
H32).
*** Proved C1: non_spark_stuff__time_of(year, month, day, hour, 10 * minute +
(element(timestring, [loop__1__i]) - 48), second) >=
unsigned_types__unsigned32__first
using hypothesis H81.
*** Proved C2: non_spark_stuff__time_of(year, month, day, hour, 10 * minute +
(element(timestring, [loop__1__i]) - 48), second) <=
unsigned_types__unsigned32__last
using hypothesis H82.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_49. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H27 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H70 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H71 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H72 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H73 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H74 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H75 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H76 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H77 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H78 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H79 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H80 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H81 has been replaced by "true". (It is already present, as
H33).
*** Proved C1: non_spark_stuff__time_of(year, month, day, hour, minute, 10 *
second + (element(timestring, [loop__1__i]) - 48)) >=
unsigned_types__unsigned32__first
using hypothesis H82.
*** Proved C2: non_spark_stuff__time_of(year, month, day, hour, minute, 10 *
second + (element(timestring, [loop__1__i]) - 48)) <=
unsigned_types__unsigned32__last
using hypothesis H83.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_50. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H37 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H38 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H39 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H41 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H70 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H71 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H72 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H73 has been replaced by "true". (It is already present, as
H25).
*** Proved C1: non_spark_stuff__time_of(year, month, day, hour, minute,
second) >= unsigned_types__unsigned32__first
using hypothesis H74.
*** Proved C2: non_spark_stuff__time_of(year, month, day, hour, minute,
second) <= unsigned_types__unsigned32__last
using hypothesis H75.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_51. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H21 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H27 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H28 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H41 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H70 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H71 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H72 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H73 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H74 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H75 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H76 has been replaced by "true". (It is already present, as
H23).
--- Hypothesis H77 has been replaced by "true". (It is already present, as
H24).
*** Proved C1: non_spark_stuff__time_of(10 * year + (element(timestring, [
loop__1__i]) - 48), month, day, hour, minute, second) >=
unsigned_types__unsigned32__first
using hypothesis H78.
*** Proved C2: non_spark_stuff__time_of(10 * year + (element(timestring, [
loop__1__i]) - 48), month, day, hour, minute, second) <=
unsigned_types__unsigned32__last
using hypothesis H79.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_52. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H22 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H30 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H31 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H70 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H71 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H72 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H73 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H74 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H75 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H76 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H77 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H78 has been replaced by "true". (It is already present, as
H29).
*** Proved C1: non_spark_stuff__time_of(year, 10 * month + (element(
timestring, [loop__1__i]) - 48), day, hour, minute, second) >=
unsigned_types__unsigned32__first
using hypothesis H79.
*** Proved C2: non_spark_stuff__time_of(year, 10 * month + (element(
timestring, [loop__1__i]) - 48), day, hour, minute, second) <=
unsigned_types__unsigned32__last
using hypothesis H80.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_53. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H23 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H33 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H34 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H70 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H71 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H72 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H73 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H74 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H75 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H76 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H77 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H78 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H79 has been replaced by "true". (It is already present, as
H30).
*** Proved C1: non_spark_stuff__time_of(year, month, 10 * day + (element(
timestring, [loop__1__i]) - 48), hour, minute, second) >=
unsigned_types__unsigned32__first
using hypothesis H80.
*** Proved C2: non_spark_stuff__time_of(year, month, 10 * day + (element(
timestring, [loop__1__i]) - 48), hour, minute, second) <=
unsigned_types__unsigned32__last
using hypothesis H81.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_54. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H24 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H36 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H37 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H42).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H70 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H71 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H72 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H73 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H74 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H75 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H76 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H77 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H78 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H79 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H80 has been replaced by "true". (It is already present, as
H31).
*** Proved C1: non_spark_stuff__time_of(year, month, day, 10 * hour + (
element(timestring, [loop__1__i]) - 48), minute, second) >=
unsigned_types__unsigned32__first
using hypothesis H81.
*** Proved C2: non_spark_stuff__time_of(year, month, day, 10 * hour + (
element(timestring, [loop__1__i]) - 48), minute, second) <=
unsigned_types__unsigned32__last
using hypothesis H82.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_55. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H25 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H39 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H42).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H43).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H42).
--- Hypothesis H70 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H71 has been replaced by "true". (It is already present, as
H42).
--- Hypothesis H72 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H73 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H74 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H75 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H76 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H77 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H78 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H79 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H80 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H81 has been replaced by "true". (It is already present, as
H32).
*** Proved C1: non_spark_stuff__time_of(year, month, day, hour, 10 * minute +
(element(timestring, [loop__1__i]) - 48), second) >=
unsigned_types__unsigned32__first
using hypothesis H82.
*** Proved C2: non_spark_stuff__time_of(year, month, day, hour, 10 * minute +
(element(timestring, [loop__1__i]) - 48), second) <=
unsigned_types__unsigned32__last
using hypothesis H83.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_56. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H26 has been replaced by "true". (It is already present, as
H14).
--- Hypothesis H27 has been replaced by "true". (It is already present, as
H15).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H44).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H70 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H71 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H72 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H73 has been replaced by "true". (It is already present, as
H40).
--- Hypothesis H74 has been replaced by "true". (It is already present, as
H41).
--- Hypothesis H75 has been replaced by "true". (It is already present, as
H38).
--- Hypothesis H76 has been replaced by "true". (It is already present, as
H39).
--- Hypothesis H77 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H78 has been replaced by "true". (It is already present, as
H37).
--- Hypothesis H79 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H80 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H81 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H82 has been replaced by "true". (It is already present, as
H33).
*** Proved C1: non_spark_stuff__time_of(year, month, day, hour, minute, 10 *
second + (element(timestring, [loop__1__i]) - 48)) >=
unsigned_types__unsigned32__first
using hypothesis H83.
*** Proved C2: non_spark_stuff__time_of(year, month, day, hour, minute, 10 *
second + (element(timestring, [loop__1__i]) - 48)) <=
unsigned_types__unsigned32__last
using hypothesis H84.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_57. @@@@@@@@@@
%%% Simplified H7 on reading formula in, to give:
%%% H7: for_all(i___1 : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i___1 and
i___1 <= rr_type__rrsig_record_type__timestringtypeindex__last ->
character__first <= element(timestring, [i___1]) and element(
timestring, [i___1]) <= character__last)
%%% Simplified H9 on reading formula in, to give:
%%% H9: for_all(i_ : integer,
rr_type__rrsig_record_type__timestringtypeindex__first <= i_ and i_
<= rr_type__rrsig_record_type__timestringtypeindex__last -> 48 <=
element(timestring, [i_]) and element(timestring, [i_]) <= 57)
--- Hypothesis H12 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H13 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H16 has been replaced by "true". (It is already present, as
H10).
--- Hypothesis H17 has been replaced by "true". (It is already present, as
H11).
--- Hypothesis H38 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H39 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H40 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H41 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H42 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H43 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H44 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H45 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H46 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H47 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H48 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H49 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H50 has been replaced by "true". (It is already present, as
H36).
--- Hypothesis H51 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H52 has been replaced by "true". (It is already present, as
H25).
--- Hypothesis H53 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H54 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H55 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H56 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H57 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H58 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H59 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H60 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H61 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H62 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H63 has been replaced by "true". (It is already present, as
H34).
--- Hypothesis H64 has been replaced by "true". (It is already present, as
H35).
--- Hypothesis H65 has been replaced by "true". (It is already present, as
H32).
--- Hypothesis H66 has been replaced by "true". (It is already present, as
H33).
--- Hypothesis H67 has been replaced by "true". (It is already present, as
H30).
--- Hypothesis H68 has been replaced by "true". (It is already present, as
H31).
--- Hypothesis H69 has been replaced by "true". (It is already present, as
H28).
--- Hypothesis H70 has been replaced by "true". (It is already present, as
H29).
--- Hypothesis H71 has been replaced by "true". (It is already present, as
H26).
--- Hypothesis H72 has been replaced by "true". (It is already present, as
H27).
--- Hypothesis H73 has been replaced by "true". (It is already present, as
H24).
--- Hypothesis H74 has been replaced by "true". (It is already present, as
H25).
*** Proved C1: non_spark_stuff__time_of(year, month, day, hour, minute,
second) >= unsigned_types__unsigned32__first
using hypothesis H75.
*** Proved C2: non_spark_stuff__time_of(year, month, day, hour, minute,
second) <= unsigned_types__unsigned32__last
using hypothesis H76.
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_58. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_59. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_60. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_61. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_62. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_63. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_64. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_65. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_66. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_67. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_68. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_69. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_70. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_71. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_72. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_73. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_74. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_75. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_76. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_77. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_78. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_79. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_80. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_81. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_82. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_83. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_84. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.
@@@@@@@@@@ VC: procedure_converttimestring_85. @@@@@@@@@@
*** Proved C1: true
*** PROVED VC.