fact: Definition vgamma2cdata (rpa : nat * Z) : reptype vertex_type := match rpa with | (r, pa) => (Vint (Int.repr pa), Vint (Int.repr (Z.of_nat r))) end.
imports: CertiGraph.msl_application.ArrayGraph VST.veric.SeparationLogic CertiGraph.unionfind.env_unionfind_arr CertiGraph.floyd_ext.share