>
> With putting the theorem in deduction form with "( ph ->" how does making
> that change work? Would I need to replace almost all theorems in the text
> so they begin with "( ph ->" or is there some way of just changing the
> beginning and the end? Sounds like it could be quite a lot of work.
>
I did this a few times, but with smaller proofs. What I did was having the
old proof in mmj2 format in a separate window in a text editor, and proving
the deduction form in mmj2 from scratch, starting from the conclusion, and
at each step, "copying" the old proof but using the "deduction version" of
the theorem used in the old proof. E.g. in the present case, I would open
mmj2, enter "mvllmuld" (instead of mvllmuli) on the "qed" line, then enter
"eqtrd" (instead of eqtri) on the previous line, etc. Sometimes, the
"deduction version" of a theorem does not exist, in particular when the old
proof was already using a deduction version ("double deduction versions"
are very rare), so you need to "export" the antecedent, continue, and then
"import" it back, using ~im and ~exp). Other tweaks might be necessary,
like some extra uses of ~syl. Indeed, this sounds boring indeed :-( Maybe
more experienced practitionners know a faster way? Maybe it would be worth
trying to shorten the proof first? It looks a bit long, given that ftc2
and dvexp should provide most of the work. Again, it would be nice to have
experienced users' opinions.
The slides by Mario on the "deduction method" are interesting (see
http://us.metamath.org/downloads/natded.pdf).
The fact that your current proof already has T. as antecedent in several
steps, and uses ~trud several times, shows that it already uses "deduction
forms" in some parts, and not in others, which gives it an awkward look.
(Roughly, in these steps, the global antecedent ph would replace T.)
Re names I am willing to make the change, I think exp for exponential is a
> bit confusing in this context. Does anyone else have input? One of the
> reviewers suggested using the word monomial so maybe itmon is possible,
> itpow is fine or something else? Using exp does match with itgsinexp
> <http://us.metamath.org/mpegif/itgsinexp.html>, though that is only in
> Glauco's math box. I looked for the theorem of the integral of e^x but
> couldn't find it :(
>
I was the one suggesting "monomial" for the comment (since I see this
theorem as a step towards integrals of polynomials). But as for the label,
I still prefer itpow. Or should it be itgpow? (And similarly, "dvexp"
could be relabeled "dvpow".)
Benoit
--
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/a4761914-607c-4d9f-b17b-4388da0f2661%40googlegroups.com.
