proposition: Fact h10c_test_spec c v : h10c_test (h10c_nat c) v = 0 <-> h10c_sem c (beta v).
proof: Proof. destruct c as [ x | x y z | x y z ]; unfold h10c_test, h10c_nat; repeat (rewrite decomp_l_recomp || rewrite decomp_r_recomp); unfold h10c_sem; apply nat_test_eq_spec. 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)