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
|
\DOC FORALL_EQ
\TYPE {FORALL_EQ : (term -> thm -> thm)}
\SYNOPSIS
Universally quantifies both sides of an equational theorem.
\KEYWORDS
rule, quantifier, universal, equality.
\DESCRIBE
When applied to a variable {x} and a theorem {A |- t1 = t2}, whose conclusion
is an equation between boolean terms, {FORALL_EQ} returns the
theorem {A |- (!x. t1) = (!x. t2)}, unless the variable {x} is free in any
of the assumptions.
{
A |- t1 = t2
------------------------ FORALL_EQ "x" [where x is not free in A]
A |- (!x.t1) = (!x.t2)
}
\FAILURE
Fails if the theorem is not an equation between boolean terms, or if the
supplied term is not simply a variable, or if the variable is free in any of
the assumptions.
\SEEALSO
AP_TERM, EXISTS_EQ, SELECT_EQ.
\ENDDOC
|
