I think that the inference version is not worth keeping: the deduction
version is enough, and easily implies the inference form. For the sake of
illustration, here is a proof of itexp from itgexp (current labeling),
using "trud" at its last step, as hinted above:
---------Clip out the proof below this line to put it in the source file:
( cicc co cv cexp citg c1 caddc cmin wtru cr wcel a1i cdiv cle wbr cn
cn0
wceq nnnn0 syl itgexp trud )
ABCIJAKDLJMCDNOJZLJBUKLJPJUKUAJUFQABCDBRSQET
CRSQFTBCUBUCQGTQDUDSZDUESULQHTDUGUHUIUJ $.
---------The proof of "itexp" (186 bytes) ends above this line.
You can paste it to see how it looks in uncompressed format.
Since only the deduction form will remain, is the suffixed "d" still
necessary? Depending on Thierry's (or someone else's) answer, I suggest
you (Jon) relabel it either itgpow or itgpowd, and remove the inference
version (if you want: this is your mathbox, after all!).
I just did some minimization and rewrapping of some of your proofs (it's
one the later commits of the pending PR #926). May I suggest that in the
future you use
MM-PA> minimize * /no *
when your proofs are done, to minimize them without introducing
dependencies on new axioms or definitions. Also, just before doing a PR,
as indicated in
https://github.com/metamath/set.mm/blob/develop/CONTRIBUTING.md, you can do
a general check and rewrap by typing
$ ./metamath 'read set.mm' 'write source set.mm /rewrap' erase 'read
set.mm' 'save proof */compressed/fast' 'verify markup
*/file_skip/top_date_skip' 'verify proof *' 'write source set.mm' quit
It rewraps everything except for the statements, i.e. in between $p ... $=
(and $a..., $e... ). For these, you have to break lines manually. At
least, do a line break after "$=". Never use tabulations. If the line of
the statement needs to be broken, then break it after operators which are
"high in the parsing tree" (I don't know how to say it precisely and
concisely, but you see what I mean).
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/39b771b9-37ee-424f-83ad-ccc6b02afd90%40googlegroups.com.
