proposition: Lemma dio_repr_at_form n f : dio_repr_at (df_pred f) n (df_weight_1 f) (df_weight_2 f).
proof: Proof. revert n; induction f as [ x i | x y | o x y z | o f IHf g IHg | f IHf ]; intros n; simpl df_pred; simpl df_weight_1; simpl df_weight_2. + apply dio_repr_at_cst; auto. + apply dio_repr_at_eq; auto. + apply dio_repr_at_op; auto. + apply dio_repr_at_bin with (n1 := df_weight_1 f) (a2 := n+df_weight_1 f) (n2 := df_weight_1 g); auto; lia. + apply dio_repr_at_exst with (n := df_weight_1 f); auto; lia. Defined.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_list) Undecidability.H10.Dio(dio_logic)