fact: Definition h10c_test c v := match decomp_l c with | 0 => let x := decomp_r c in nat_test_eq (beta v x) 1 | 1 => let x := decomp_l (decomp_r (decomp_r c)) in let y := decomp_r (decomp_r (decomp_r c)) in let z := decomp_l (decomp_r c) in nat_test_eq (beta v x + beta v y) (beta v z) | _ => let x := decomp_l (decomp_r (decomp_r c)) in let y := decomp_r (decomp_r (decomp_r c)) in let z := decomp_l (decomp_r c) in nat_test_eq (beta v x * beta v y) (beta v z) 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)