proposition: Theorem dio_formula_elem f : { l | length l <= 1+7*df_size f /\ (forall c x, In c l -> dc_vars c x -> x < 8*df_size f) /\ forall ν, df_pred f ν <-> exists φ, Forall (dc_eval φ ν) l }.
proof: Proof. destruct (dio_repr_at_form 0 f) as [l r H0 H1 H2 H3 H4]. exists ((r,dee_nat 0) :: l); split; [ | split ]; simpl length; try lia. + rewrite H0; apply le_n_S, df_weigth_2_size. + intros c x [ [] | H ]. * simpl dc_vars; intros [ | [] ]; subst. generalize (df_weigth_1_size f); intros; simpl; lia. * intros G; apply H1 in G; auto. generalize (df_weigth_1_size f); intros; simpl; lia. + intros ν; rewrite H4. split; intros (φ & H); exists φ; revert H; rewrite Forall_cons_inv; simpl; tauto. Defined.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_list) Undecidability.H10.Dio(dio_logic)