proposition: Fact ra_h10c_val c v : ⟦ra_h10c⟧ (c##v##vec_nil) (h10c_test c v).
proof: Proof. simpl. set (i0 := decomp_r c). set (i := decomp_l (decomp_r (decomp_r c))). set (j := decomp_r (decomp_r (decomp_r c))). set (k := decomp_l (decomp_r c)). exists (decomp_l c##nat_test_eq (beta v i0) 1 ##nat_test_eq (beta v i + beta v j) (beta v k) ##nat_test_eq (beta v i * beta v j) (beta v k) ##vec_nil). split. + apply ra_choice3_spec; intros H; unfold h10c_test. * rewrite H; auto. * rewrite H; auto. * destruct (decomp_l c) as [ | [] ]; auto; lia. + pos split; simpl. * exists (c##vec_nil); split; simpl; auto. pos split; simpl; auto. * exists (beta v i0##1##vec_nil); split. - apply ra_eq_val. - pos split; simpl. { apply Hx0. } apply ra_cst_n_val. * exists (beta v i+beta v j##beta v k##vec_nil); split; simpl. - apply ra_eq_val. - pos split; simpl. 2: { apply Hz. } exists (beta v i##beta v j##vec_nil); split; simpl. { apply ra_plus_val. } pos split; simpl. ++ apply Hx. ++ apply Hy. * exists (beta v i*beta v j##beta v k##vec_nil); split; simpl. - apply ra_eq_val. - pos split; simpl. 2: apply Hz. exists (beta v i##beta v j##vec_nil); split; simpl; auto. pos split; simpl. ++ apply Hx. ++ apply Hy. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_nat utils_list) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.MuRec.Util(recalg ra_utils ra_enum recomp ra_recomp beta ra_godel_beta) Undecidability.DiophantineConstraints(H10C Util.h10c_utils)