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

Re: Bogus << TCC

The TCC proves with

    (use "exp_well_founded[identifier,nat]")

Check the file "exp_adt.pvs", the prover guide or the datatypes report
(both available from the PVS web page at http://pvs.csl.sri.com) for
details on the datatype mechanism and the subterm ordering <<.


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 David.Stringer-Calvert@sri.com