src/HOL/SPARK/Examples/RIPEMD-160/rmd/r_l.siv

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/rmd/r_l.siv	Sat Jan 15 12:35:29 2011 +0100
@@ -0,0 +1,81 @@
+*****************************************************************************
+                       Semantic Analysis of SPARK Text
+    Examiner Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
+             Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
+*****************************************************************************
+
+
+CREATED 29-NOV-2010, 14:30:19  SIMPLIFIED 29-NOV-2010, 14:30:28
+
+SPARK Simplifier Pro Edition, Version 9.1.0, Build Date 20101119, Build 19039
+Copyright (C) 2010 Altran Praxis Limited, Bath, U.K.
+
+function RMD.R_L
+
+
+
+
+For path(s) from start to run-time check associated with statement of line 59:
+
+function_r_l_1.
+*** true .          /* all conclusions proved */
+
+
+For path(s) from start to finish:
+
+function_r_l_2.
+H1:    j >= 0 .
+H2:    j <= 79 .
+H3:    block_index__size >= 0 .
+H4:    block_index__base__first <= block_index__base__last .
+H5:    round_index__size >= 0 .
+H6:    round_index__base__first <= round_index__base__last .
+H7:    block_index__base__first <= 0 .
+H8:    block_index__base__last >= 15 .
+H9:    round_index__base__first <= 0 .
+H10:   round_index__base__last >= 79 .
+       ->
+C1:    element(mk__block_permutation([0] := 0, [1] := 1, [2] := 2, [3] := 3, [4]
+           := 4, [5] := 5, [6] := 6, [7] := 7, [8] := 8, [9] := 9, [10] := 10, [
+          11] := 11, [12] := 12, [13] := 13, [14] := 14, [15] := 15, [16] := 7, 
+          [17] := 4, [18] := 13, [19] := 1, [20] := 10, [21] := 6, [22] := 15, [
+          23] := 3, [24] := 12, [25] := 0, [26] := 9, [27] := 5, [28] := 2, [29]
+           := 14, [30] := 11, [31] := 8, [32] := 3, [33] := 10, [34] := 14, [35]
+           := 4, [36] := 9, [37] := 15, [38] := 8, [39] := 1, [40] := 2, [41] 
+          := 7, [42] := 0, [43] := 6, [44] := 13, [45] := 11, [46] := 5, [47] 
+          := 12, [48] := 1, [49] := 9, [50] := 11, [51] := 10, [52] := 0, [53] 
+          := 8, [54] := 12, [55] := 4, [56] := 13, [57] := 3, [58] := 7, [59] 
+          := 15, [60] := 14, [61] := 5, [62] := 6, [63] := 2, [64] := 4, [65] 
+          := 0, [66] := 5, [67] := 9, [68] := 7, [69] := 12, [70] := 2, [71] := 
+          10, [72] := 14, [73] := 1, [74] := 3, [75] := 8, [76] := 11, [77] := 
+          6, [78] := 15, [79] := 13), [j]) = r_l_spec(j) .
+C2:    element(mk__block_permutation([0] := 0, [1] := 1, [2] := 2, [3] := 3, [4]
+           := 4, [5] := 5, [6] := 6, [7] := 7, [8] := 8, [9] := 9, [10] := 10, [
+          11] := 11, [12] := 12, [13] := 13, [14] := 14, [15] := 15, [16] := 7, 
+          [17] := 4, [18] := 13, [19] := 1, [20] := 10, [21] := 6, [22] := 15, [
+          23] := 3, [24] := 12, [25] := 0, [26] := 9, [27] := 5, [28] := 2, [29]
+           := 14, [30] := 11, [31] := 8, [32] := 3, [33] := 10, [34] := 14, [35]
+           := 4, [36] := 9, [37] := 15, [38] := 8, [39] := 1, [40] := 2, [41] 
+          := 7, [42] := 0, [43] := 6, [44] := 13, [45] := 11, [46] := 5, [47] 
+          := 12, [48] := 1, [49] := 9, [50] := 11, [51] := 10, [52] := 0, [53] 
+          := 8, [54] := 12, [55] := 4, [56] := 13, [57] := 3, [58] := 7, [59] 
+          := 15, [60] := 14, [61] := 5, [62] := 6, [63] := 2, [64] := 4, [65] 
+          := 0, [66] := 5, [67] := 9, [68] := 7, [69] := 12, [70] := 2, [71] := 
+          10, [72] := 14, [73] := 1, [74] := 3, [75] := 8, [76] := 11, [77] := 
+          6, [78] := 15, [79] := 13), [j]) >= 0 .
+C3:    element(mk__block_permutation([0] := 0, [1] := 1, [2] := 2, [3] := 3, [4]
+           := 4, [5] := 5, [6] := 6, [7] := 7, [8] := 8, [9] := 9, [10] := 10, [
+          11] := 11, [12] := 12, [13] := 13, [14] := 14, [15] := 15, [16] := 7, 
+          [17] := 4, [18] := 13, [19] := 1, [20] := 10, [21] := 6, [22] := 15, [
+          23] := 3, [24] := 12, [25] := 0, [26] := 9, [27] := 5, [28] := 2, [29]
+           := 14, [30] := 11, [31] := 8, [32] := 3, [33] := 10, [34] := 14, [35]
+           := 4, [36] := 9, [37] := 15, [38] := 8, [39] := 1, [40] := 2, [41] 
+          := 7, [42] := 0, [43] := 6, [44] := 13, [45] := 11, [46] := 5, [47] 
+          := 12, [48] := 1, [49] := 9, [50] := 11, [51] := 10, [52] := 0, [53] 
+          := 8, [54] := 12, [55] := 4, [56] := 13, [57] := 3, [58] := 7, [59] 
+          := 15, [60] := 14, [61] := 5, [62] := 6, [63] := 2, [64] := 4, [65] 
+          := 0, [66] := 5, [67] := 9, [68] := 7, [69] := 12, [70] := 2, [71] := 
+          10, [72] := 14, [73] := 1, [74] := 3, [75] := 8, [76] := 11, [77] := 
+          6, [78] := 15, [79] := 13), [j]) <= 15 .
+
+