1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
\DOC CONJUNCTS_CONV
\TYPE {CONJUNCTS_CONV : ((term # term) -> thm)}
\SYNOPSIS
Prove equivalence under idempotence, symmetry and associativity of conjunction.
\KEYWORDS
conversion, conjunction.
\DESCRIBE
{CONJUNCTS_CONV} takes a pair of terms {"t1"} and {"t2"}, and proves
{|- t1 = t2} if {t1} and {t2} are equivalent up to idempotence, symmetry and
associativity of conjunction. That is, if {t1} and {t2} are two (different)
arbitrarily-nested conjunctions of the same set of terms, then {CONJUNCTS_CONV
(t1,t2)} returns {|- t1 = t2}. Otherwise, it fails.
\FAILURE
Fails if {t1} and {t2} are not equivalent, as described above.
\EXAMPLE
{
#CONJUNCTS_CONV ("(P /\ Q) /\ R", "R /\ (Q /\ R) /\ P");;
|- (P /\ Q) /\ R = R /\ (Q /\ R) /\ P
}
\USES
Used to reorder a conjunction. First sort the conjuncts in a term {t1} into
the desired order (e.g. lexicographic order, for normalization) to get a new
term {t2}, then call {CONJUNCTS_CONV(t1,t2)}.
\COMMENTS
This is not a true conversion, so perhaps it ought to be called something else.
\SEEALSO
CONJ_SET_CONV.
\ENDDOC
|
