We want to prove

.S1,S2,S3:Set (S1 & (S2 & S3) = (S1 & S2) & 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 & (S2 & S3) = N in (S1 & S2) & S3 - Quantifier elimination introduces new
constants *n :Nat*and*s1 s2 s3 :Set*. - Show
( n in s1 & (s2 & s3) = n in (s1 & s2) & s3 )

- Quantifier elimination introduces new

We want to prove

.S1,S2:Set (S1 & S2 = S2 & 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 & S2 = N in S2 & S1 )) - Quantifier elimination introduces new
constants *n :Nat*and*s1 s2 :Set*. - Show
( n in s1 & s2 = n in s2 & s1 )

- Quantifier elimination introduces new

We want to prove

.S1:Set (S1 & 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 & S1 = N in S1 )) - Quantifier elimination introduces new
constants *n :Nat*and*s1 :Set*. - Show
( n in s1 & s1 = n in s1 )

- Quantifier elimination introduces new