Dear ...: I am a graduate student at KAIST, Korea. I am working with PVS. Actually, I want to know more profoundly how to prove an AXIOM formated as: (IF ---- THEN === ELSIF +++ THEN ... ELSE ,,,) I am using only (prop), (postpone), and (assert), but this seems not to be sufficient to me. Please, let me know as mmuch information as possible. Thank you very much. Best Regards, Han Seong.