We want to prove

.S1,S2,S3:Set (S1 U (S2 U S3) = (S1 U S2) U S3)

- First, we prove the attribute coherence of the input specification.
- Introduce the
lemma coherence(SET) - This goal is true because
coherence(SET)

- Introduce the
- Then we prove
S1,S2,S3:Set N:Nat N in S1 U (S2 U S3) = N in (S1 U S2) U S3 - Quantifier elimination introduces new
constants *n :Nat*and*s1 s2 s3 :Set*. - Show
( n in s1 U (s2 U s3) = n in (s1 U s2) U s3 )

- Quantifier elimination introduces new

We want to prove

.S1:Set (empty U S1 = S1)

- First, we prove the attribute coherence of the input specification.
- Introduce the
lemma coherence(SET) - This goal is true because
coherence(SET)

- Introduce the
- Then we prove
S1:Set (N:Nat ( N in empty U S1 = N in S1 )) - Quantifier elimination introduces new
constants *n :Nat*and*s1 :Set*. - Show
( n in empty U s1 = n in s1 )

- Quantifier elimination introduces new

We want to prove

.S1:Set (S1 U S1 = S1)

- First, we prove the attribute coherence of the input specification.
- Introduce the
lemma coherence(SET) - This goal is true because
coherence(SET)

- Introduce the
- Then we prove
S1:Set (N:Nat ( N in S1 U S1 = N in S1 )) - Quantifier elimination introduces new
constants *n :Nat*and*s1 :Set*. - Show
( n in s1 U s1 = n in s1 )

- Quantifier elimination introduces new

We want to prove

.S1,S2:Set (S1 U S2 = S2 U S1)

- First, we prove the attribute coherence of the input specification.
- Introduce the
lemma coherence(SET) - This goal is true because
coherence(SET)

- Introduce the
- Then we prove
S1,S2:Set (N:Nat ( N in S1 U S2 = N in S2 U S1 )) - Quantifier elimination introduces new
constants *n :Nat*and*s1 s2 :Set*. - Show
( n in s1 U s2 = n in s2 U s1 )

- Quantifier elimination introduces new