helphome pageduck scriptspecificationfirst proof pagepage 1 1 2 3 4 page 2

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:
  1. ( L  : List  N  : Nat  ) N in nil = false
  2. ( L  : List  M  N  : Nat  ) N in cons(M , L) = N == M or (N in L)

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.


BOBJ proof scoreLeft    Up    Down    Right   
 

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