Hi Thierry,
yes, you are right - the second list contains also theorems of the
mathboxes. Here is the list containing only the 23 theorems of the main
part.
On Sunday, November 3, 2019 at 11:44:23 PM UTC+1, Thierry Arnoux wrote:
>
> Hi Alexander,
>
> For the second list, did you also restrict yourself to the main part of
> set.mm ?
> BR,
> _
> Thierry
>
> Le 3 nov. 2019 à 23:38, 'Alexander van der Vekens' via Metamath <
> [email protected] <javascript:>> a écrit :
>
>
>
> On Thursday, October 31, 2019 at 1:55:27 PM UTC+1, Norman Megill wrote:
>
>>
>> We could add ph to every such hypothesis to make it more general-purpose,
>> but 99% of the time it wouldn't be needed and would make all other proofs
>> using it (as well as the theorem itself) slightly longer. Not to mention
>> that it would be a huge retrofit to do this throughout set.mm. I will
>> concede there may be a few cases where it would be advantageous to do
>> things other than prove a simple substitution with the hypothesis, but
>> overall I believe it is rare and does not justify adding ph everywhere.
>>
>> I tried to identify all the theorems in set.mm (excluding the mathboxes)
> which would be concerned - I found about 70 of them (see attachment
> deduct_th_eq_hyp.txt). On the other hand, there are about 50 theorema in
> deduction form having the form $e |- ( ( ph /\ x = ... ) -> ... ) $. (see
> attachment deduct_th_ph_eq_hyp.txt). So there is no big difference.
> Therefore, I still would propose to recommend to use the form $e |- ( ( ph
> /\ x = ... ) -> ... ) $. in deduction style. Already existing theorems need
> not to be rewritten (by the way, many of them have no "d" at the end..).
>
>>
>>
> --
> 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] <javascript:>.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/351cfee0-e03b-4d61-b839-694b61641bb0%40googlegroups.com
>
> <https://groups.google.com/d/msgid/metamath/351cfee0-e03b-4d61-b839-694b61641bb0%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
> <deduct_th_ph_eq_hyp.txt>
> <deduct_th_eq_hyp.txt>
>
>
--
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/3620ab9b-f405-43d2-821f-e15b56977eb0%40googlegroups.com.
Theorems written in deduction form, using hypotheses of the kind
$e |- ( ( ph /\ x = ... ) -> ... ) $.
Line 51536: ralxfrd.3 $e |- ( ( ph /\ x = A ) -> ( ps <-> ch ) ) $.
Line 51558: ralxfr2d.3 $e |- ( ( ph /\ x = A ) -> ( ps <-> ch ) ) $.
Line 59804: iota2df.3 $e |- ( ( ph /\ x = B ) -> ( ps <-> ch ) ) $.
Line 63151: fvmptd.2 $e |- ( ( ph /\ x = A ) -> B = C ) $.
Line 63231: fvmptdf.2 $e |- ( ( ph /\ x = A ) -> B e. V ) $.
Line 63232: fvmptdf.3 $e |- ( ( ph /\ x = A ) -> ( ( F ` A ) = B ->
ps ) ) $.
Line 63257: fvmptdv2.2 $e |- ( ( ph /\ x = A ) -> B e. V ) $.
Line 63258: fvmptdv2.3 $e |- ( ( ph /\ x = A ) -> B = C ) $.
Line 64651: fmptapd.2 $e |- ( ( ph /\ x = A ) -> C = B ) $.
Line 64668: fmptpr.5 $e |- ( ( ph /\ x = A ) -> E = C ) $.
Line 64669: fmptpr.6 $e |- ( ( ph /\ x = B ) -> E = D ) $.
Line 66839: riota2df.5 $e |- ( ( ph /\ x = B ) -> ( ps <-> ch ) ) $.
Line 68467: ovmpt2dx.3 $e |- ( ( ph /\ x = A ) -> D = L ) $.
Line 68548: ovmpt2df.2 $e |- ( ( ph /\ x = A ) -> B e. D ) $.
Line 68581: ovmpt2dv2.2 $e |- ( ( ph /\ x = A ) -> B e. D ) $.
Line 75327: sprmpt2d.2 $e |- ( ( ph /\ v = V /\ e = E ) -> ( ch <->
ps ) ) $.
Line 77808: oe0lem.1 $e |- ( ( ph /\ A = (/) ) -> ps ) $.
Line 216690: gsumsnd.s $e |- ( ( ph /\ k = M ) -> A = C ) $.
Line 216714: gsumzunsnd.s $e |- ( ( ph /\ k = M ) -> X = Y ) $.
Line 216743: gsumunsnd.s $e |- ( ( ph /\ k = M ) -> X = Y ) $.
Line 222411: gsummgp0.e $e |- ( ( ph /\ n = i ) -> A = B ) $.
Line 315067: itgparts.e $e |- ( ( ph /\ x = X ) -> ( A x. C ) = E )
$.
Line 315068: itgparts.f $e |- ( ( ph /\ x = Y ) -> ( A x. C ) = F )
$.
