>That's great, but I do not really know how to get this theorem (including its proof) from the sequence ["fvex","eqeltri"]. How does the reverse-engineering work in mmj2?
The sequence of labels "fvex", "eqeltri" is the sequence of essential steps in the compressed proof of our theorem. For example in metamath.exe: MM>show proof test1/lemmon 6 test1.1 $e |- A = ( F ` B ) 9 fvex $p |- ( F ` B ) e. _V 10 6,9 eqeltri $p |- A e. _V To deduce the theorem from the sequence of labels in mmj2, I do as follows (note that there might be a better way). Start with a clean proof: 10:: qed:: |- ph Then set the theorem in 10 to eqeltri and unify with Ctrl-U: !d1:: |- &C1 = &C2 !d2:: |- &C2 e. &C3 10:d1,d2:eqeltri |- &C1 e. &C3 qed:: |- ph Now set the theorem in !d2 to fvex and unify: !d1:: |- &C1 = ( &C5 ` &C4 ) d2::fvex |- ( &C5 ` &C4 ) e. _V 10:d1,d2:eqeltri |- &C1 e. _V qed:: |- ph Fill in the meta variables: !d1:: |- A = ( F ` B ) d2::fvex |- ( F ` B ) e. _V 10:d1,d2:eqeltri |- A e. _V qed:: |- ph Finally, set step 10 to qed and rename all unproven steps to hypotheses (only !d1 in our case): h1::test1.1 |- A = ( F ` B ) d2::fvex |- ( F ` B ) e. _V qed:1,d2:eqeltri |- A e. _V $= ( test1.1 cfv cvv fvex eqeltri ) ABCEFDBCGH $. For some reason mmj2 puts test1.1 into the label list, so it must be removed. We have a theorem with one essential hypothesis |- A = ( F ` B ) and conclusion |- A e. _V. The proof is $= ( cfv cvv fvex eqeltri ) ABCEFDBCGH $. -- 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/38398358-b9c1-4977-a7d8-acc44a631773n%40googlegroups.com.
