% @(#)$Id: UndirectedGraphTrait.lsl,v 1.4 1997/07/25 05:32:44 leavens Exp $

UndirectedGraphTrait(N,E): trait

  includes GraphTrait(N,E)

  introduces
     includesEdge: Set[E], E -> Bool

  asserts
    \forall e: E, n,m: N, e: E, se: Set[E]
      includesEdge(se, makeEdge(n,m)) == e \in edges;

  implies
    converts
      includesEdge: Set[E], E -> Bool

[Index]

HTML generated using lcpp2html.