fact: Fixpoint poly_of_formula f := match f with | formula_var x => Poly (Cst false) x (Cst true) | formula_btm => Cst false | formula_top => Cst true | formula_cnj fl fr => let pl := poly_of_formula fl in let pr := poly_of_formula fr in poly_mul pl pr | formula_dsj fl fr => let pl := poly_of_formula fl in let pr := poly_of_formula fr in poly_add (poly_add pl pr) (poly_mul pl pr) | formula_neg f => poly_add (Cst true) (poly_of_formula f) | formula_xor fl fr => poly_add (poly_of_formula fl) (poly_of_formula fr) | formula_ifb fc fl fr => let pc := poly_of_formula fc in let pl := poly_of_formula fl in let pr := poly_of_formula fr in poly_add pr (poly_add (poly_mul pc pl) (poly_mul pc pr)) end.
imports: Bool DecidableClass Algebra Ring PArith Lia