equal
deleted
inserted
replaced
1489 |
1489 |
1490 |
1490 |
1491 lemma seq_closed_form_variant: |
1491 lemma seq_closed_form_variant: |
1492 assumes "s \<noteq> []" |
1492 assumes "s \<noteq> []" |
1493 shows "rders_simp (RSEQ r1 r2) s = |
1493 shows "rders_simp (RSEQ r1 r2) s = |
1494 rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # (map (rders_simp r2) (vsuf s r1))))" |
1494 rsimp (RALTS (RSEQ (rders_simp r1 s) r2 # |
|
1495 (map (rders_simp r2) (vsuf s r1))))" |
1495 using assms q seq_closed_form by force |
1496 using assms q seq_closed_form by force |
1496 |
1497 |
1497 |
1498 |
1498 fun hflat_aux :: "rrexp \<Rightarrow> rrexp list" where |
1499 fun hflat_aux :: "rrexp \<Rightarrow> rrexp list" where |
1499 "hflat_aux (RALT r1 r2) = hflat_aux r1 @ hflat_aux r2" |
1500 "hflat_aux (RALT r1 r2) = hflat_aux r1 @ hflat_aux r2" |