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

*To*: pvs-help@csl.sri.com*Subject*: Induction derivation tree*From*: hkim15 <hkim15@students.uiuc.edu>*Date*: Sat, 1 Mar 2003 14:13:31 -0600*Sender*: pvs-help-owner@csl.sri.com

Dear PVS helpers, Hello. How can I do a induction on derivation trees? For instance, let's consider that a theory has embedded two axiomizations A and B. Then, what should I do to formally prove that A |- x iff B |- y Thank you very much in advance. Hong-Seok

- Prev by Date:
**existskwantor problem** - Next by Date:
**problem with finite types** - Prev by thread:
**rewrite rule for expressions inside LAMBDA** - Next by thread:
**existskwantor problem** - Index(es):