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

obsolete;

*****************************************************************************
                       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 .