changeset 56798 | 939e88e79724 |
parent 41561 | d1318f3c86ba |
child 62390 | 842917225d56 |
56797:32963b43a538 | 56798:939e88e79724 |
---|---|
6 |
6 |
7 theory S_R |
7 theory S_R |
8 imports RMD_Specification RMD_Lemmas |
8 imports RMD_Specification RMD_Lemmas |
9 begin |
9 begin |
10 |
10 |
11 spark_open "rmd/s_r.siv" |
11 spark_open "rmd/s_r" |
12 |
12 |
13 spark_vc function_s_r_2 |
13 spark_vc function_s_r_2 |
14 proof - |
14 proof - |
15 from `0 \<le> j` `j \<le> 79` |
15 from `0 \<le> j` `j \<le> 79` |
16 show C: ?C1 |
16 show C: ?C1 |