Re: what's the precise meaning of ...?

[Dave Stringer-Calvert <dave_sc@csl.sri.com>]

> I'm intended to prove the following formula: subset?(g,v) where

What you probably intended is this:

    test: THEORY
    BEGIN
     valve : TYPE = {closed,open}
     va    : TYPE = setof[valve]
     v     : va = fullset[valve]
    

     guan  : TYPE = {i : valve | i = closed}
     gu    : TYPE = setof[guan]
     g     : va = fullset[guan]

     try: formula subset?(g,v)

    END test

The proof of "try" is then simply (grind).

> I'm very confused by the precise meaning of variables defined by
> 'setof[T]'.

setof[T] defines a type, not a variable.

> For instance, 'va: type=setof[valve]'. Since 'v: var va ', so, what's
> the value of 'v'?  v={closed,open} or {open} or {closed} or {closed,
> open, {closed,open}} or all of these are possible?

In your example, v is a variable which can take any possible value of the
type va, including the emptyset, i.e. v={}.

> How to define a set like v={closed, open} which contains 2 elements, one
> is 'closed', the other is 'open'.

Two ways.  The first is how I did it above, to say v is a "fullset" of
valve, ie contains every element of the set.  Another approach would be
to enumerate the elements:

  v : va = {i : valve | i = open OR i = closed}

Hope that helps,
Dave

---
Dr Dave Stringer-Calvert,  Senior Project Manager,  Computer Science Lab
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA
Phone: (650) 859-3291 Fax: (650) 859-2844 David.Stringer-Calvert@sri.com