fact: Definition nat_h10c (n : nat) := match decomp_l n with | 0 => h10c_one (decomp_r n) | 1 => h10c_plus (decomp_l (decomp_r (decomp_r n))) (decomp_r (decomp_r (decomp_r n))) (decomp_l (decomp_r n)) | _ => h10c_mult (decomp_l (decomp_r (decomp_r n))) (decomp_r (decomp_r (decomp_r n))) (decomp_l (decomp_r n)) end.
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)