(* this file was automatically generated; do not edit *)

(* zone variables *)
type global
(* logic types *)
(* heap variables *)
(* functions specifications *)
parameter addElemList_parameter :
 val:int -> l:global pointer -> { } unit { true }

parameter addElemSet_parameter :
 s:global pointer -> { } global pointer { true }

parameter addNodeList_parameter :
 lnode:global pointer -> l:global pointer -> { } unit { true }

parameter assignSet_parameter :
 s_orig:global pointer -> s_dest:global pointer -> { } unit { true }

parameter calcBoolSet_parameter :
 val1:int -> op:global pointer -> val2:int -> { } int { true }

parameter cleanList_parameter : nd:global pointer -> { } unit { true }

parameter cleanSet_parameter : s:global pointer -> { } unit { true }

parameter copyList_parameter :
 l_orig:global pointer -> l_dest:global pointer -> { } unit { true }

parameter duplicateSet_parameter :
 s:global pointer -> { } global pointer { true }

parameter getElemList_parameter :
 pos:int -> l:global pointer -> { } int { true }

parameter getHeadList_parameter : l:global pointer -> { } int { true }

parameter getSizeList_parameter : l:global pointer -> { } int { true }

parameter getTailList_parameter :
 l:global pointer -> { } global pointer { true }

parameter interceptionSet_parameter :
 s1:global pointer -> s2:global pointer -> { } global pointer { true }

parameter isEmptyList_parameter : l:global pointer -> { } int { true }

parameter isInSet_parameter : val:int -> s:global pointer -> { } int { true }

parameter isMemberList_parameter :
 val:int -> l:global pointer -> { } int { true }

parameter isOperator_parameter : op:global pointer -> { } int { true }

parameter main_parameter : tt:unit -> { } unit { true }

parameter max_parameter :
 x:int ->
  y:int ->
   { } int
   { ("File \"max.c\", line 8, characters 4-86":
     ((ge_int(result, x) and ge_int(result, y))
     and (forall z:int.
          ((ge_int(z, x) and ge_int(z, y)) -> ge_int(z, result))))) }

parameter newInitList_parameter :
 array_0:global pointer -> dim:int -> { } global pointer { true }

parameter newList_parameter : tt:unit -> { } global pointer { true }

parameter newNodeList_parameter : val:int -> { } global pointer { true }

parameter newNodeSet_parameter :
 val:global pointer -> { } global pointer { true }

parameter newSet_parameter :
 array_0:global pointer -> dim:int -> { } global pointer { true }

parameter remElemList_parameter :
 val:int -> l:global pointer -> { } unit { true }

parameter unionSet_parameter :
 s1:global pointer -> s2:global pointer -> { } global pointer { true }

