proposition: Fact ra_recomp_val a b : ⟦ra_recomp⟧ (a##b##vec_nil) (recomp a b).
proof: Proof. unfold recomp. rewrite Nat.add_comm. exists (power a 2 * (S (2*b)) ## vec_nil); split; auto. pos split; simpl. exists (power a 2##S (2*b)##vec_nil); split; auto. pos split; simpl; auto. + exists (a##vec_nil); split; auto. pos split; simpl; auto. + exists (2*b##vec_nil); split; simpl; auto. pos split; simpl; auto. exists (2##b##vec_nil); split. { apply ra_mult_val. } 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 prim_min ra_utils)