src/HOL/SPARK/Examples/RIPEMD-160/rmd/r_l.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/r_l.rls	Sat Jan 15 12:35:29 2011 +0100
     1.3 @@ -0,0 +1,75 @@
     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.77*/
    1.12 +
    1.13 +                              /*function RMD.R_L*/
    1.14 +
    1.15 +
    1.16 +rule_family r_l_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 +r_l_rules(1): block_index__first <= element(r_values, [I]) may_be_deduced_from [0 <= I, I <= 79].
    1.22 +r_l_rules(2): element(r_values, [I]) <= block_index__last may_be_deduced_from [0 <= I, I <= 79].
    1.23 +r_l_rules(3): r_values may_be_replaced_by 
    1.24 +           mk__block_permutation([round_index__first] := 0, [
    1.25 +           round_index__first + 1] := 1, [round_index__first + 2] := 2, [
    1.26 +           round_index__first + 3] := 3, [round_index__first + 4] := 4, [
    1.27 +           round_index__first + 5] := 5, [round_index__first + 6] := 6, [
    1.28 +           round_index__first + 7] := 7, [round_index__first + 8] := 8, [
    1.29 +           round_index__first + 9] := 9, [round_index__first + 10] := 
    1.30 +           10, [round_index__first + 11] := 11, [
    1.31 +           round_index__first + 12] := 12, [round_index__first + 13] := 
    1.32 +           13, [round_index__first + 14] := 14, [
    1.33 +           round_index__first + 15] := 15, [round_index__first + 16] := 
    1.34 +           7, [round_index__first + 17] := 4, [round_index__first + 18] := 
    1.35 +           13, [round_index__first + 19] := 1, [round_index__first + 20] := 
    1.36 +           10, [round_index__first + 21] := 6, [round_index__first + 22] := 
    1.37 +           15, [round_index__first + 23] := 3, [round_index__first + 24] := 
    1.38 +           12, [round_index__first + 25] := 0, [round_index__first + 26] := 
    1.39 +           9, [round_index__first + 27] := 5, [round_index__first + 28] := 
    1.40 +           2, [round_index__first + 29] := 14, [round_index__first + 30] := 
    1.41 +           11, [round_index__first + 31] := 8, [round_index__first + 32] := 
    1.42 +           3, [round_index__first + 33] := 10, [round_index__first + 34] := 
    1.43 +           14, [round_index__first + 35] := 4, [round_index__first + 36] := 
    1.44 +           9, [round_index__first + 37] := 15, [round_index__first + 38] := 
    1.45 +           8, [round_index__first + 39] := 1, [round_index__first + 40] := 
    1.46 +           2, [round_index__first + 41] := 7, [round_index__first + 42] := 
    1.47 +           0, [round_index__first + 43] := 6, [round_index__first + 44] := 
    1.48 +           13, [round_index__first + 45] := 11, [
    1.49 +           round_index__first + 46] := 5, [round_index__first + 47] := 
    1.50 +           12, [round_index__first + 48] := 1, [round_index__first + 49] := 
    1.51 +           9, [round_index__first + 50] := 11, [round_index__first + 51] := 
    1.52 +           10, [round_index__first + 52] := 0, [round_index__first + 53] := 
    1.53 +           8, [round_index__first + 54] := 12, [round_index__first + 55] := 
    1.54 +           4, [round_index__first + 56] := 13, [round_index__first + 57] := 
    1.55 +           3, [round_index__first + 58] := 7, [round_index__first + 59] := 
    1.56 +           15, [round_index__first + 60] := 14, [
    1.57 +           round_index__first + 61] := 5, [round_index__first + 62] := 
    1.58 +           6, [round_index__first + 63] := 2, [round_index__first + 64] := 
    1.59 +           4, [round_index__first + 65] := 0, [round_index__first + 66] := 
    1.60 +           5, [round_index__first + 67] := 9, [round_index__first + 68] := 
    1.61 +           7, [round_index__first + 69] := 12, [round_index__first + 70] := 
    1.62 +           2, [round_index__first + 71] := 10, [round_index__first + 72] := 
    1.63 +           14, [round_index__first + 73] := 1, [round_index__first + 74] := 
    1.64 +           3, [round_index__first + 75] := 8, [round_index__first + 76] := 
    1.65 +           11, [round_index__first + 77] := 6, [round_index__first + 78] := 
    1.66 +           15, [round_index__first + 79] := 13).
    1.67 +r_l_rules(4): block_index__size >= 0 may_be_deduced.
    1.68 +r_l_rules(5): block_index__first may_be_replaced_by 0.
    1.69 +r_l_rules(6): block_index__last may_be_replaced_by 15.
    1.70 +r_l_rules(7): block_index__base__first <= block_index__base__last may_be_deduced.
    1.71 +r_l_rules(8): block_index__base__first <= block_index__first may_be_deduced.
    1.72 +r_l_rules(9): block_index__base__last >= block_index__last may_be_deduced.
    1.73 +r_l_rules(10): round_index__size >= 0 may_be_deduced.
    1.74 +r_l_rules(11): round_index__first may_be_replaced_by 0.
    1.75 +r_l_rules(12): round_index__last may_be_replaced_by 79.
    1.76 +r_l_rules(13): round_index__base__first <= round_index__base__last may_be_deduced.
    1.77 +r_l_rules(14): round_index__base__first <= round_index__first may_be_deduced.
    1.78 +r_l_rules(15): round_index__base__last >= round_index__last may_be_deduced.