equal
deleted
inserted
replaced
54 done |
54 done |
55 |
55 |
56 lemma wir_moel: "YS = YYS" |
56 lemma wir_moel: "YS = YYS" |
57 apply (rule stream.take_lemmas) |
57 apply (rule stream.take_lemmas) |
58 apply (induct_tac n) |
58 apply (induct_tac n) |
59 apply (simp (no_asm) add: stream.rews) |
59 apply (simp (no_asm)) |
60 apply (subst YS_def2) |
60 apply (subst YS_def2) |
61 apply (subst YYS_def2) |
61 apply (subst YYS_def2) |
62 apply (simp add: stream.rews) |
62 apply simp |
63 apply (rule lemma5 [symmetric, THEN subst]) |
63 apply (rule lemma5 [symmetric, THEN subst]) |
64 apply (rule refl) |
64 apply (rule refl) |
65 done |
65 done |
66 |
66 |
67 (* ------------------------------------------------------------------------ *) |
67 (* ------------------------------------------------------------------------ *) |