Implementing Sets with Lists

Implementing Sets with Lists
LIST is a refinement of SET.

We want to prove

L:List (N:Nat (N in nil = false)) and
L:List (M,N:Nat ( $ N in cons(M, L) = N == M or N in L $ )) .

Conjunction elimination introduces subgoals as follows:

L:List (N:Nat (N in nil = false))

Quantifier elimination introduces new constants n :Nat and l :List .

Show n in nil = false by reduction.

L:List (M,N:Nat ( $ N in cons(M, L) = N == M or N in L $ ))

Quantifier elimination introduces new constants m n :Nat and l :List .

Show $ n in cons(m, l) = n == m or n in l $ by reduction.

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