equal
deleted
inserted
replaced
1545 then have "created_by_star (rder c r1)" |
1545 then have "created_by_star (rder c r1)" |
1546 using cbs_ders_cbs by blast |
1546 using cbs_ders_cbs by blast |
1547 then have "created_by_star (rder c r2)" |
1547 then have "created_by_star (rder c r2)" |
1548 using "2.hyps"(3) cbs_ders_cbs by auto |
1548 using "2.hyps"(3) cbs_ders_cbs by auto |
1549 then show ?case |
1549 then show ?case |
1550 |
|
1551 by (simp add: "2.hyps"(2) "2.hyps"(4)) |
1550 by (simp add: "2.hyps"(2) "2.hyps"(4)) |
1552 qed |
1551 qed |
1553 |
1552 |
1554 |
1553 (*AALTS [a\x . b.c, b\x .c, c \x]*) |
|
1554 (*AALTS [a\x . b.c, AALTS [b\x .c, c\x]]*) |
1555 |
1555 |
1556 lemma stupdate_induct1: |
1556 lemma stupdate_induct1: |
1557 shows " concat (map (hflat_aux \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) = |
1557 shows " concat (map (hflat_aux \<circ> (rder x \<circ> (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)))) Ss) = |
1558 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)" |
1558 map (\<lambda>s1. RSEQ (rders r0 s1) (RSTAR r0)) (star_update x r0 Ss)" |
1559 apply(induct Ss) |
1559 apply(induct Ss) |