helphome pageduck scriptspecificationfirst proof pagepage 3page 2 1 2 3 4 page 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.)


BOBJ proof scoreLeft    Up    Down    Right   
 

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