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

Re: Instanciating unboud varaibles




Laurent -

If it is not necessary to instantiate a variable in order to complete the
proof, then you don't have to.

BTW - x is not 'unbound' in:

 {-1}  FORALL (x) : expression(x)

The reference to x in expression(x) is bound to the FORALL (x).  If by
"unbound" you mean that x is not shown as having a specific type at that
point, then this may be a bug.  If you mean that it is not referenced in
the proof, or elsewhere in this sequent, then that's okay, but is not the
right meaning of "unbound".

Dave

---
Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory,
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA.
Phone: (650) 859-3291    Fax: (650) 859-2844   Email: dave_sc@csl.sri.com