theory CryptHOL imports GPV_Bisim GPV_Applicative Computational_Model Negligible Cyclic_Group_SPMF List_Bits Environment_Functor begin end