proposition: Lemma clean_dot' n m p (e: guards n m) (f: guards m p): clean e -> clean f -> clean (g_dot' e f).
proof: Proof. intros He Hf. apply clean_sup. intros x Hx. apply clean_sup. intros y Hy. apply He in Hx. apply Hf in Hy. clear e f He Hf. destruct x as [a|a e b]; destruct y as [c|c f d]; unfold g_dot1; (case eqb_spec; [intros <-|intro E]); try apply clean_bot; apply clean_single; trivial. revert Hx Hy. unfold clean1, geval. rewrite 8G.lang_dot, 3G.lang_atom. simpl o; simpl v. fold_regex. rewrite 8R.lang_dot. repeat change (o_pred ?a (atom ?b)) with (o (g_atom a b)). setoid_rewrite R_lang_atom. intros Hx Hy. rewrite 4dotA, <-dotA, <-(dotA _ _ (latom _ _)). apply gl_dot. assumption. rewrite 2dotA. assumption. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms