Implementing Sets with Lists
We prove coherence of the theory SET .
We want to prove
coherence(SET)
.
Attribute coherence requires us to prove the following
subgoals:

S4,S3,S2,S1:Set
((N:Nat ( N in S1 = N in S2 )) and (N:Nat ( N in S3 = N in S4 )) implies
N:Nat ( N in S1 U S3 = N in S2 U S4 ))
.

S4,S3,S2,S1:Set
((N:Nat ( N in S1 = N in S2 )) and (N:Nat ( N in S3 = N in S4 )) implies
N:Nat ( N in S1 & S3 = N in S2 & S4 ))
.

S2,S1:Set
(N:Nat ( N in S1 = N in S2 ) implies
N:Nat ( N in neg(S1) = N in neg(S2) ))
.

S2,S1:Set
M:Nat
(N:Nat ( N in S1 = N in S2 ) implies
N:Nat ( N in add(M,S1) = N in add(M,S2) ))
.
This page was generated
by Kumo on
Mon Jun 15 13:44:12 PDT 1998
from code written by Grigore Rosu,