proposition: Fact ra_iter_h10uc_val_1 : (exists p, p < n /\ ~ h10uc_eq a' b' (idx_h10uc a b p)) -> ⟦ra_iter_h10uc⟧ (n##a##b##a'##b'##vec_nil) 1.
proof: Proof. intros H2; simpl. exists (0##vec_nil); split. { apply ra_not_val. } pos split; simpl; auto. destruct ra_lsum_S with (1 := f_pr) (i := n) (v := a##b##a'##b'##vec_nil) as (k & Hk). { destruct H2 as (p & H2 & H3). exists p, 0; split; auto. unfold h10uc_eq, idx_h10uc in H3. generalize (f_val p a b a' b'). unfold h10uc_test. match type of H3 with | ?a <> ?b => destruct (eq_nat_dec a b) end; auto; lia. } exists (S k##vec_nil); split. { apply ra_not_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)