proposition: Lemma teval_xitr n m (r: guard n m) q: teval (xitr r q) ≡ (geval r ⋅ teval q)^+.
proof: Proof. unfold xitr. rewrite 2teval_dot, sup_app, 2sup_singleton, teval_one. symmetry. rewrite itr_str_l. rewrite (geval_fst r) at 2. rewrite <-(dotA (g_atom _ _)), str_dot. apply dot_weq. 2: reflexivity. rewrite cupC. unfold geval at 3. rewrite dotA. rewrite <-itr_str_l. rewrite itr_aea by now rewrite idem_atom_dot. rewrite <-str_itr. apply str_weq1. induction q as [|e q IH]. ra. simpl (sup _ _). rewrite 2dotxpls, 2dotplsx. rewrite <-(cupI 1), 2cupA, 2comm4. apply cup_weq. 2: assumption. clear IH. rewrite <-dirac_refl. rewrite teval_inner_dot. case eqb_spec; intro E. setoid_rewrite dot1x. rewrite E. now rewrite <-dotA, <-geval_lst. rewrite (geval_lst e), <-2dotA, empty_atom_dot by congruence. ra. Qed.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms