My quest to understanding the details of metamath continues.
I found a proof step for a result in set.mm where two mandatory variables
are constrained to be disjoint, but mapped to two variables that are *not
*constrained
to be disjoint.
In the context of statement `2alimdv`, variables `x` and `ph` are disjoint.
However, in that statement's proof, `x` and `ph` get substituted for `y`
and `ps` respectively. But there is no disjoint constraint between `y` and
`ps`. This seems to violate disjoint variable restrictions (as per my
reading for the end of Section 4.1.4 in the metamath book).
Is there something about `ps` not being mandatory? Am I misunderstanding
disjoint variable restrictions?
Thank you!
Details below:
MM> show statement alimdv /full
Statement 4613 is located on line 25887 of the file "set.mm". Its statement
number for HTML pages is 1756.
"Deduction form of Theorem 19.20 of [Margaris] p. 90, see ~ alim .
(Contributed by NM, 3-Apr-1994.)"
4613 alimdv $p |- ( ph -> ( A. x ps -> A. x ch ) ) $= ... $.
Its mandatory hypotheses in RPN order are:
wph $f wff ph $.
wps $f wff ps $.
wch $f wff ch $.
vx $f setvar x $.
alimdv.1 $e |- ( ph -> ( ps -> ch ) ) $.
Its mandatory disjoint variable pairs are: <ph,x>
Its optional hypotheses are: wth wta wet wze wsi wrh wmu wla wka vy vz vw
vv
vu vt
The statement and its hypotheses require the variables: ph x ps ch
These additional variables are allowed in its proof: th ta et ze si rh mu
la
ka y z w v u t
The variables it contains are: ph x ps ch
---
MM> show proof 2alimdv /detailed_step 4
Proof step 4: wps=wal $a wff A. y ps
This step assigns source "wal" ($a) to target "wps" ($f). The source
assertion
requires the hypotheses "wph" ($f, step 2) and "vx.wal" ($f, step 3). The
parent assertion of the target hypothesis is "alimdv" ($p, step 15).
The source assertion before substitution was:
wal $a wff A. x ph
The following substitutions were made to the source assertion:
Variable Substituted with
x y
ph ps
The target hypothesis before substitution was:
wps $f wff ps
The following substitution was made to the target hypothesis:
Variable Substituted with
ps A. y ps
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/e7f841ee-5f40-46c3-8606-b00d3767ca6dn%40googlegroups.com.
