proposition: Fact ra_h10uc_val : ⟦ra_h10uc⟧ (x##y##z##a'##b'##vec_nil) (h10uc_test a' b' x y z).
proof: Proof. exists (1-ite_rel (1+vx+vy*vy-vz) (vz-(1+vx+vy*vy)) 1##vec_nil); split. { generalize (ra_not_val (1-ite_rel (1+vx+vy*vy-vz) (vz-(1+vx+vy*vy)) 1)). intros H; eq goal H; f_equal. unfold ite_rel, h10uc_test. fold vx; fold vy; fold vz. case_eq (1 + vx + vy * vy - vz); destruct (eq_nat_dec (1+vx+vy*vy) vz); intros; lia. } pos split; simpl. exists (ite_rel (1+vx+vy*vy-vz) (vz-(1+vx+vy*vy)) 1##vec_nil); split. { apply ra_not_val. } pos split; simpl. exists (1+vx+vy*vy##vz##vec_nil); split. { apply ra_eq_val. } pos split; simpl; auto. + exists (vx+vy*vy##vec_nil); split; auto. { simpl; auto. } pos split; simpl; auto. exists (vx##vy*vy##vec_nil); split; auto. pos split; simpl; auto. * exists (a'##b'##x##vec_nil); split. { apply ra_godel_beta_val. } pos split; simpl; auto. * exists (vy##vec_nil); split; auto. pos split. exists (a'##b'##y##vec_nil); split. { apply ra_godel_beta_val. } pos split; simpl; auto. + exists (a'##b'##z##vec_nil); split. { apply ra_godel_beta_val. } pos split; simpl; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list crt pos vec) Undecidability.MuRec.Util(recalg ra_utils ra_enum recomp ra_recomp beta ra_godel_beta) Undecidability.DiophantineConstraints(H10C Util.h10c_utils)