@savask thanks a lot for your detailed explanation how reverse engineering
can be performed with mmj2. Following your "tutorial", I was able to create
my first theorem (from No. 6 of your list):
h1::Test.1 |- ( ph -> X e. A )
h2::Test.2 |- ( ph -> th )
h3::Test.3 |- ( ph -> ta )
h4::Test.4 |- ( x = X -> ( ps <-> th ) )
h5::Test.5 |- ( x = X -> ( ch <-> ta ) )
d5:4,5:anbi12d |- ( x = X -> ( ( ps /\ ch ) <-> ( th /\ ta ) ) )
d4:d5:rspcev |- ( ( X e. A /\ ( th /\ ta ) ) -> E. x e. A ( ps /\ ch
) )
qed:1,2,3,d4:syl12anc
|- ( ph -> E. x e. A ( ps /\ ch ) )
with $d A x $. $d X x $. $d ta x $. $d th x $.
But is this a useful theorem? Although it looks inconspicuous, I have run
the minimize script looking for proofs using ~rspcev (there are more than
5000 of them), and stopped the script after more than 100 proofs were found
which could be minimized by using the new theorem. This shows that there is
a high potential that such theorems can be useful for a lot of
minimizations.
--
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/b0759878-65b0-4f8a-ba40-e781baf870e3n%40googlegroups.com.
