1\DOC COND_CONV 2 3\TYPE {COND_CONV : conv} 4 5\SYNOPSIS 6Simplifies conditional terms. 7 8\KEYWORDS 9conversion, conditional. 10 11\DESCRIBE 12The conversion {COND_CONV} simplifies a conditional term {"c => u | v"} if 13the condition {c} is either the constant {T} or the constant {F} or 14if the two terms {u} and {v} are equivalent up to alpha-conversion. 15The theorems returned in these three cases have the forms: 16{ 17 |- (T => u | v) = u 18 19 |- (F => u | v) = u 20 21 |- (c => u | u) = u 22} 23 24 25\FAILURE 26{COND_CONV tm} fails if {tm} is not a conditional {"c => u | v"}, where 27{c} is {T} or {F}, or {u} and {v} are alpha-equivalent. 28 29\ENDDOC 30