fact: Fixpoint o_pred (x: test): expr3 n n := match x with | e_bot => 0 | e_top => 1 | e_cup x y => o_pred x + o_pred y | e_cap x y => o_pred x ⋅ o_pred y | e_neg x => o_npred x | e_var a => syntax.e_var (l_pos n a) end with o_npred (x: test): expr3 n n := match x with | e_bot => 1 | e_top => 0 | e_cup x y => o_npred x ⋅ o_npred y | e_cap x y => o_npred x + o_npred y | e_neg x => o_pred x | e_var a => syntax.e_var (l_neg n a) end.
imports: Coq.PArith.BinPosDef denum lset sums normalisation kat ka_completeness untyping regex gregex lsyntax syntax lang glang boolean atoms