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