page 3 1 2 3 4

Behavioral Properties of Set
Intersection

 Associativity of intersection We want to prove ( S0  S1  S2  : Set  ) (S0 & S1) & S2 = S0 & (S1 & S2) . This goal is proved directly by circular coinductive rewriting. Commutativity of intersection We want to prove ( S0  S1  : Set  ) S0 & S1 = S1 & S0 . This goal is proved directly by circular coinductive rewriting. Idempotence of intersection We want to prove ( S  : Set  ) S & S = S . This goal is proved directly by circular coinductive rewriting. The empty set is a zero for intersection We want to prove ( S  : Set  ) empty & S = empty . This goal is proved directly by circular coinductive rewriting.

 Explanation Each proof is a straightforward application of circular coinductive rewriting (the special case of attribute coinduction is actually sufficient), using the specification `SET`. (By the way, the buttons labelled Left, Right, Up, Down don't do anything because each proof is complete on its own page.)

 Left    Up    Down    Right

This page was generated by Kumo on Tue Feb 13 11:31:33 PST 2001.