proposition: Fact ra_godel_beta_val a b n : ⟦ra_godel_beta⟧ (a##b##n##vec_nil) (godel_beta a b n).
proof: Proof. exists (a##S ((S n)*b)##vec_nil); split. + apply ra_rem_val; discriminate. + pos split; simpl; auto. exists (((S n)*b)##vec_nil); split; simpl; auto. pos split; simpl. exists (S n##b##vec_nil); split. * apply ra_mult_val. * pos split; simpl; auto. exists (n##vec_nil); split; simpl; auto. pos split; simpl; auto. Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_nat gcd crt sums) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.MuRec.Util(recalg recomp beta ra_utils ra_recomp)