13 notation (latex output) |
13 notation (latex output) |
14 Cons ("_::_" [48,47] 48) and |
14 Cons ("_::_" [48,47] 48) and |
15 Oc ("0") and |
15 Oc ("0") and |
16 Bk ("1") and |
16 Bk ("1") and |
17 exponent ("_\<^bsup>_\<^esup>") and |
17 exponent ("_\<^bsup>_\<^esup>") and |
18 inv_begin0 ("I\<^isub>0") and |
18 inv_begin0 ("I\<^sub>0") and |
19 inv_begin1 ("I\<^isub>1") and |
19 inv_begin1 ("I\<^sub>1") and |
20 inv_begin2 ("I\<^isub>2") and |
20 inv_begin2 ("I\<^sub>2") and |
21 inv_begin3 ("I\<^isub>3") and |
21 inv_begin3 ("I\<^sub>3") and |
22 inv_begin4 ("I\<^isub>4") and |
22 inv_begin4 ("I\<^sub>4") and |
23 inv_begin ("I\<^bsub>cbegin\<^esub>") and |
23 inv_begin ("I\<^bsub>cbegin\<^esub>") and |
24 inv_loop1 ("J\<^isub>1") and |
24 inv_loop1 ("J\<^sub>1") and |
25 inv_loop0 ("J\<^isub>0") and |
25 inv_loop0 ("J\<^sub>0") and |
26 inv_end1 ("K\<^isub>1") and |
26 inv_end1 ("K\<^sub>1") and |
27 inv_end0 ("K\<^isub>0") |
27 inv_end0 ("K\<^sub>0") |
28 |
28 |
29 |
29 |
30 |
30 |
31 lemma inv_begin_print: |
31 lemma inv_begin_print: |
32 shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and |
32 shows "s = 0 \<Longrightarrow> inv_begin n (s, tp) = inv_begin0 n tp" and |