Theory Base_MEC

theory Base_MEC
  imports "HOL-Library.Omega_Words_Fun"
          "Isabelle_LLVM.IICF_Array_Map" 
          "Isabelle_LLVM.Refine_Monadic_Add" "./VC_Solve"
          "Isabelle_LLVM.IICF_Set"
          "Isabelle_LLVM.Refine_Monadic_Add"
          "Isabelle_LLVM.LLVM_DS_Array_List"
          "Isabelle_LLVM.IICF_List"
begin

hide_const (open ) NEMonad.RETURN

type_synonym size_T = "64"
type_synonym size_t = "size_T word"
abbreviation(input) "len_size_T ≡ (64::nat)"
abbreviation "size_rel ≡ snat_rel' TYPE(size_T)"
abbreviation "size_assn ≡ snat_assn' TYPE(size_T)"

lemma "LENGTH(size_T) = len_size_T"
  by simp

end