equal
deleted
inserted
replaced
821 "(alphalts ===> op =) rfv_lts rfv_lts" |
821 "(alphalts ===> op =) rfv_lts rfv_lts" |
822 "(alphalts ===> op =) rbv5 rbv5" |
822 "(alphalts ===> op =) rbv5 rbv5" |
823 sorry |
823 sorry |
824 |
824 |
825 lemma bv_list_rsp: |
825 lemma bv_list_rsp: |
826 shows "t \<approx>5 s \<Longrightarrow> True" |
826 shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
827 and "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y" |
827 apply(induct rule: alpha5_alphalts.inducts(2)) |
828 apply(induct rule: alpha5_alphalts.inducts) |
|
829 apply(simp_all) |
828 apply(simp_all) |
830 done |
829 done |
831 |
830 |
832 lemma |
831 lemma |
833 shows "(alphalts ===> op =) rbv5 rbv5" |
832 shows "(alphalts ===> op =) rbv5 rbv5" |