proposition: Fact ra_iter_h10c_val_1 : (exists p, p < n /\ ~ h10c_sem (nat_h10c (beta lc p)) (beta v)) -> ⟦ra_iter_h10c⟧ (n##lc##v##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 := Hf_pr) (i := n) (v := lc##v##vec_nil) as (k & Hk). { destruct H2 as (p & H2 & H3). rewrite <- h10c_test_spec, h10c_test_stable in H3. case_eq (h10c_test (beta lc p) v). { intros; lia. } intros k Hk. exists p, k; rewrite <- Hk; split; auto. } exists (S k##vec_nil); split. { apply ra_not_val. } pos split; simpl; auto. 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)