Implementing Sets with Lists
De Morgen laws

We want to prove

S1,S2:Set    (neg (S1 U S2) = neg(S1) & neg (S2)     and
   neg (S1 & S2) = neg(S1) U neg (S2) )
.
We use attribute coinduction to prove this is a behavorial property of the input specification. Implementing Sets with Lists

Distributive law for union and intersection

We want to prove

S1,S2,S3:Set    (S1 U (S2 & S3) = (S1 U S2) & (S1 U S3)     and
   S1 & (S2 U S3) = (S1 & S2) U (S1 & S3) )
.
We use attribute coinduction to prove this is a behavorial property of the input specification.


This page was generated
by Kumo on Mon Jun 15 13:46:12 PDT 1998 from code written by Grigore Rosu,