fact: Definition nat_h10lc k := let n := decomp_l k in let lc := decomp_r k in map (fun p => nat_h10c (beta lc (pos2nat p))) (pos_list n).
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)