src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.rls
changeset 41561 d1318f3c86ba
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/Liseq/liseq/liseq_length.rls	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,34 @@
     1.4 +           /*********************************************************/
     1.5 +                           /*Proof Rule Declarations*/
     1.6 +    /*Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039*/
     1.7 +             /*Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.*/
     1.8 +           /*********************************************************/
     1.9 +
    1.10 +
    1.11 +                        /*DATE : 29-NOV-2010 14:30:13.02*/
    1.12 +
    1.13 +                        /*procedure Liseq.Liseq_length*/
    1.14 +
    1.15 +
    1.16 +rule_family liseq_length_rules:
    1.17 +     X      requires [X:any] &
    1.18 +     X <= Y requires [X:ire, Y:ire] &
    1.19 +     X >= Y requires [X:ire, Y:ire].
    1.20 +
    1.21 +liseq_length_rules(1): integer__size >= 0 may_be_deduced.
    1.22 +liseq_length_rules(2): integer__first may_be_replaced_by -2147483648.
    1.23 +liseq_length_rules(3): integer__last may_be_replaced_by 2147483647.
    1.24 +liseq_length_rules(4): integer__base__first may_be_replaced_by -2147483648.
    1.25 +liseq_length_rules(5): integer__base__last may_be_replaced_by 2147483647.
    1.26 +liseq_length_rules(6): a__index__subtype__1__first >= integer__first may_be_deduced.
    1.27 +liseq_length_rules(7): a__index__subtype__1__last <= integer__last may_be_deduced.
    1.28 +liseq_length_rules(8): a__index__subtype__1__first <= 
    1.29 +     a__index__subtype__1__last may_be_deduced.
    1.30 +liseq_length_rules(9): a__index__subtype__1__last >= integer__first may_be_deduced.
    1.31 +liseq_length_rules(10): a__index__subtype__1__first <= integer__last may_be_deduced.
    1.32 +liseq_length_rules(11): l__index__subtype__1__first >= integer__first may_be_deduced.
    1.33 +liseq_length_rules(12): l__index__subtype__1__last <= integer__last may_be_deduced.
    1.34 +liseq_length_rules(13): l__index__subtype__1__first <= 
    1.35 +     l__index__subtype__1__last may_be_deduced.
    1.36 +liseq_length_rules(14): l__index__subtype__1__last >= integer__first may_be_deduced.
    1.37 +liseq_length_rules(15): l__index__subtype__1__first <= integer__last may_be_deduced.