Behavioral Properties of Set

page 1

1 2 3 4

Behavioral Properties of Set
LIST is a Behavioral 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 yields 2 subgoals:

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

Quantifier elimination introduces the new constant(s) l : List n : Nat .
We 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 the new constant(s) l : List m, n : Nat .
We show n in cons(m , l) = n == m or (n in l) by reduction.

And thus the main goal is proved.

Explanation

This is a straightforward verification of the two axioms in the specification BASICSET: conjunction elimination turns the goal into the two equations, which are then easily checked by reduction in the theory of lists.

Left Up Down Right

This page was generated by Kumo on Tue Feb 13 11:31:33 PST 2001.