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

Induction derivation tree

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.