Deduction oveq2i has logical hypothesis named oveq1i.1
34 views
Skip to first unread message
heiph...@wilsonb.com
Oct 25, 2019, 6:03:53 PM10/25/19
to meta...@googlegroups.com
Hello,
The names in the subject line tripped me up. Is this intentional?
In particular, looking at the proof 2p2e4, the first unification is oveq1i.1=df-2, which is followed by it's parent eqtr4i.1=oveq2i. The mismatch between the deduction name and its hypothesis name confused me for a bit. However, since 2p2e4 is exhibited as an example in the MPE, I would be a bit surprised if this just happened to be an unnoticed error.
Just in case, I also confirmed the above against HEAD on the develop branch (commit 2ebe15d3 at the time).
Forgive the spam if I am just missing something obvious.
Cheers,
B. Wilson
The names in the subject line tripped me up. Is this intentional?
In particular, looking at the proof 2p2e4, the first unification is oveq1i.1=df-2, which is followed by it's parent eqtr4i.1=oveq2i. The mismatch between the deduction name and its hypothesis name confused me for a bit. However, since 2p2e4 is exhibited as an example in the MPE, I would be a bit surprised if this just happened to be an unnoticed error.
Just in case, I also confirmed the above against HEAD on the develop branch (commit 2ebe15d3 at the time).
Forgive the spam if I am just missing something obvious.
Cheers,
B. Wilson
heiph...@wilsonb.com
Oct 25, 2019, 7:56:28 PM10/25/19
to meta...@googlegroups.com
heiph...@wilsonb.com
Oct 25, 2019, 7:56:28 PM10/25/19
to meta...@googlegroups.com
0 new messages