[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Looking for old finite_set library

I am working on PVS proof reuse.
I need the old pvs finite_set library.

Specially I am interested in the following two LEMMA's
A,B: VAR finite_set

finite_union: LEMMA is_finite(union(A,B))
finite_intersection: LEMMA is_finite(intersection(A,B))

Can somebody suggest me a url, where I can find this proof.


                    A mind all logic is like a knife all blade. 
                       It makes the hand bleed that uses it.