helphome pageduck scriptspecificationfirst proof pagepage 2page 1 1 2 3 4 page 3

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.)


BOBJ proof scoreLeft    Up    Down    Right   
 

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