SSL pairs.pvs

pairs[T: TYPE]: THEORY

BEGIN

   x,y,v,z: VAR T

   pair: TYPE = [T,T]

   mk_pair(x,y): pair = (x,y)

   mk_pair_eq: LEMMA mk_pair(x,y) = mk_pair(v,z) IMPLIES (x = v AND y = z) 

   in?(z:T, p: pair): bool = LET (x,y) = p IN z = x OR z = y

   apair?(x,y): bool = (x /= y)

   apair: TYPE = {p: pair | LET (x,y) = p IN x /= y}

   ap: VAR apair
   apair_irreflexive  : LEMMA LET (x,y) = ap IN x /= y

END pairs