Dear pvs-help: I have a question about a proof with PVS. Reading a paper on PVS proof, I found that using TABLE makes it easy to prove IF-THEN rules. But, I am very interested in proving IF-THEN-ELSE rules themselves. I have tried it, but no TCC's are generated. Do you have any idea for this problem? Please respond to me. Thank you. Best regards, Han Seong.