src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_r.rls
changeset 41561 d1318f3c86ba
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/SPARK/Examples/RIPEMD-160/rmd/k_r.rls	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,35 @@
     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:19.76*/
    1.12 +
    1.13 +                              /*function RMD.K_R*/
    1.14 +
    1.15 +
    1.16 +rule_family k_r_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 +k_r_rules(1): interfaces__unsigned_32__size >= 0 may_be_deduced.
    1.22 +k_r_rules(2): interfaces__unsigned_32__first may_be_replaced_by 0.
    1.23 +k_r_rules(3): interfaces__unsigned_32__last may_be_replaced_by 4294967295.
    1.24 +k_r_rules(4): interfaces__unsigned_32__base__first may_be_replaced_by 0.
    1.25 +k_r_rules(5): interfaces__unsigned_32__base__last may_be_replaced_by 4294967295.
    1.26 +k_r_rules(6): interfaces__unsigned_32__modulus may_be_replaced_by 4294967296.
    1.27 +k_r_rules(7): word__size >= 0 may_be_deduced.
    1.28 +k_r_rules(8): word__first may_be_replaced_by 0.
    1.29 +k_r_rules(9): word__last may_be_replaced_by 4294967295.
    1.30 +k_r_rules(10): word__base__first may_be_replaced_by 0.
    1.31 +k_r_rules(11): word__base__last may_be_replaced_by 4294967295.
    1.32 +k_r_rules(12): word__modulus may_be_replaced_by 4294967296.
    1.33 +k_r_rules(13): round_index__size >= 0 may_be_deduced.
    1.34 +k_r_rules(14): round_index__first may_be_replaced_by 0.
    1.35 +k_r_rules(15): round_index__last may_be_replaced_by 79.
    1.36 +k_r_rules(16): round_index__base__first <= round_index__base__last may_be_deduced.
    1.37 +k_r_rules(17): round_index__base__first <= round_index__first may_be_deduced.
    1.38 +k_r_rules(18): round_index__base__last >= round_index__last may_be_deduced.