fact: Definition nat_h10luc k := let n := decomp_r k in let a := decomp_l (decomp_l k) in let b := decomp_r (decomp_l k) in map (fun p => idx_h10uc a b (pos2nat p)) (pos_list n).
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list crt pos vec) Undecidability.MuRec.Util(recalg ra_utils ra_enum recomp ra_recomp beta ra_godel_beta) Undecidability.DiophantineConstraints(H10C Util.h10c_utils)