proposition: Fact ra_choice3_val b x y z : ⟦ra_choice3⟧ (b##x##y##z##vec_nil) (match b with 0 => x | 1 => y | _ => z end).
proof: Proof. exists (nat_test_eq b 0##x##match b with 1 => y | _ => z end##vec_nil). simpl; split. { apply ra_ite_rel; simpl. destruct b as [ | [] ]; simpl; auto. } pos split; simpl; auto. + exists (b##0##vec_nil); split. * apply ra_eq_val. * pos split; simpl; auto. + exists (nat_test_eq b 1##y##z##vec_nil); split; simpl; auto. * apply ra_ite_rel; simpl. destruct b as [ | [] ]; simpl; auto. * pos split; simpl; auto. exists (b##1##vec_nil); split. - apply ra_eq_val. - pos split; simpl; auto. Qed.
imports: Arith List Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list gcd crt sums finite pos vec) Undecidability.MuRec.Util(recalg recomp prim_min)