page 2 1 2 3 4

Behavioral Properties of Set
Union

 Associativity of union We want to prove ( S0  S1  S2  : Set  ) (S0 U S1) U S2 = S0 U (S1 U S2) . This goal is proved directly by circular coinductive rewriting. Commutativity of union We want to prove ( S0  S1  : Set  ) S0 U S1 = S1 U S0 . This goal is proved directly by circular coinductive rewriting. Idempotency of union We want to prove ( S  : Set  ) S U S = S . This goal is proved directly by circular coinductive rewriting. The empty set is a unit for union We want to prove ( S  : Set  ) empty U S = S . 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.