equal
deleted
inserted
replaced
85 apply (erule (1) flatstream_adm_lemma) |
85 apply (erule (1) flatstream_adm_lemma) |
86 apply (fast) |
86 apply (fast) |
87 done |
87 done |
88 |
88 |
89 |
89 |
90 (* context (theory "Nat_InFinity");*) |
90 (* context (theory "Extended_Nat");*) |
91 lemma ile_lemma: "Fin (i + j) <= x ==> Fin i <= x" |
91 lemma ile_lemma: "Fin (i + j) <= x ==> Fin i <= x" |
92 by (rule order_trans) auto |
92 by (rule order_trans) auto |
93 |
93 |
94 lemma stream_monoP2I: |
94 lemma stream_monoP2I: |
95 "!!X. stream_monoP F ==> !i. ? l. !x y. |
95 "!!X. stream_monoP F ==> !i. ? l. !x y. |