Skip to content

Commit

Permalink
Replace syl5reqr with eqtr3di (#4276)
Browse files Browse the repository at this point in the history
This is in set.mm and iset.mm

* Add eqtr3di with the order of the hypotheses switched and the variables renamed.

* edit local copy of scripts/minimize to use "minimize_with eqtr3di/may_grow" in
place of the normal minimize

* Run "show usage syl5reqr" and copy-paste the output to a shell command like
for i in x y z; do scripts/minimize $i set.mm; done

* For theorems which had been marked "Proof modification is discouraged",
add /OVERRIDE on PROVE and SAVE NEW_PROOF in the script and run.
Check that the change to use eqtr3di is the only modification printed in the
output. (This step was needed for sineq0ALT in set.mm and nothing in iset.mm)

* Remove syl5reqr

* Repeat for iset.mm
  • Loading branch information
jkingdon authored Oct 10, 2024
1 parent 72fbdcb commit 60914d5
Show file tree
Hide file tree
Showing 3 changed files with 3,801 additions and 3,802 deletions.
2 changes: 1 addition & 1 deletion changes-set.txt
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,6 @@ proposed syl5ibrcom imbitrridcom
proposed syl5bb bitrid compare to bitri or bitrd
proposed syl5rbb bitr2id compare to bitr2i or bitr2d
proposed syl5eq eqtrid compare to eqtri or eqtrd
proposed syl5reqr eqtr3di hypotheses would be switched
proposed syl6 imtrdi alternate proposal: syldi
proposed syl6com imtrdicom
proposed syl6d imtrdid
Expand All @@ -97,6 +96,7 @@ make a github issue.)

DONE:
Date Old New Notes
10-Oct-24 syl5reqr eqtr3di order of hypotheses is switched
30-Sep-24 syl5req eqtr2id compare to eqtr2i or eqtr2d
27-Sep-24 syldbl2 [same] moved from SP's mathbox to main set.mm
27-Sep-24 fiminre2 [same] moved from GS's mathbox to main set.mm
Expand Down
Loading

0 comments on commit 60914d5

Please sign in to comment.