fact: Definition g_inner_dot n m (x: guard n m): forall p, guard m p -> gregex n p := match x with | g_pred a => fun p y => match y with | g_pred b => 0 | g_elem b e c => if eqb a b ⊓ eqb a c then e else 0 end | g_elem a e b => fun p y => match y with | g_pred c => fun e => if eqb a b ⊓ eqb b c then e else 0 | g_elem c f d => fun e => if eqb b c ⊓ eqb a d then e⋅g_atom _ b⋅f else 0 end e end.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms