On the embedding of multiway decision graphs in HOL