A follow up of #4024. The deduction version fndmd was moved to Main on 18-May-2023. Nobody looked through the proofs for possible applications. This is now done by me.
What is different than usual? This all are shortenings, but I neither added a Proof shortened tag, nor provided an OLD version. It is a very mechanical process to open the proofs in Metamath and apply a minimize_with fndmd command. In all instances affected proofs were introduced to Main before May-2023. So there is no learning effect for their authors. That's why I kept it simple.
I only worked on theorems in Main.
Statisics: Each proof roughly became 10 proof bytes shorter. This corresponds to one line in the proof display. Every now and then this small shortening prevented a proof to spill over into a new line. So set.mm is 4 text lines shorter now.
A follow up of #4024. The deduction version fndmd was moved to Main on 18-May-2023. Nobody looked through the proofs for possible applications. This is now done by me.
What is different than usual? This all are shortenings, but I neither added a Proof shortened tag, nor provided an OLD version. It is a very mechanical process to open the proofs in Metamath and apply a minimize_with fndmd command. In all instances affected proofs were introduced to Main before May-2023. So there is no learning effect for their authors. That's why I kept it simple.
I only worked on theorems in Main.
Statisics: Each proof roughly became 10 proof bytes shorter. This corresponds to one line in the proof display. Every now and then this small shortening prevented a proof to spill over into a new line. So set.mm is 4 text lines shorter now.