Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
CONJ_CANON_CONV : term -> thm
SYNOPSIS
Puts an iterated conjunction in canonical form.
DESCRIPTION
When applied to a term, CONJ_CANON_CONV splits it into the set of conjuncts
and produces a theorem asserting the equivalence of the term and the new term
with the disjuncts right-associated without repetitions and in a canonical
order.
FAILURE CONDITIONS
Fails if applied to a non-Boolean term. If applied to a term that is not a
conjunction, it will trivially work in the sense of regarding it as a single
conjunct and returning a reflexive theorem.
EXAMPLE
# CONJ_CANON_CONV `(a /\ b) /\ ((b /\ d) /\ a) /\ c`;;
val it : thm = |- (a /\ b) /\ ((b /\ d) /\ a) /\ c <=> a /\ b /\ c /\ d