proposition: Lemma eval_inv n min i k (v : vec (recalg i) k) a l : eval n min (rec_erase erase v) a = Some (inr l) -> exists x, vec_list x = l /\ (forall j : pos k, eval (n -S (pos2nat j)) min (erase (vec_pos v j)) a = Some (inl (vec_pos x j))).
proof: Proof. induction v in n,l |- *. - destruct n; cbn. + firstorder congruence. exact vec_nil. + intros [=]; subst. exists vec_nil. split; auto. intro j; invert pos j. - destruct n. 1: inversion 1. intros ?. cbn in H. destruct (eval n) eqn:E1; try congruence. destruct s; try congruence. destruct (eval n min (rec_erase erase v) a) eqn:E2; try congruence. destruct s; try congruence. inv H. edestruct IHv as (? & ? & ?). 1: eauto. exists (n1 ## x). split. 1: cbn; firstorder congruence. intros j; pos_inv j. + rewrite pos2nat_fst in *. assert (S n - 1 = n) by lia. rewrite H1 in *. cbn -[eval]. eassumption. + rewrite pos2nat_nxt. specialize (H0 j). assert (S n - S (S (pos2nat j)) = n - S (pos2nat j)) by lia. rewrite H1 in *. cbn. rewrite H0. reflexivity. Qed.
imports: Undecidability.H10(H10 dio_single dio_logic) Undecidability.L.Datatypes(LNat LOptions LSum) Undecidability.L(Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode) Undecidability.Shared(DLW.Utils.finite DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec(MuRec recalg ra_sem_eq) Undecidability.L.Reductions.MuRec.MuRec_extract