Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Shorten well-ordered recursion #4403

Merged
merged 13 commits into from
Nov 18, 2024
Merged

Shorten well-ordered recursion #4403

Show file tree
Hide file tree
Changes from 10 commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
62e9c15
Begin work on transitioning definition of wrecs
sctfn Nov 18, 2024
69c3cde
add some well-founded theorems that avoid ax-rep
sctfn Nov 18, 2024
274eeae
swap definitions of wrecs and obsolete the major lemmas
sctfn Nov 18, 2024
c9ce01c
Paperwork
sctfn Nov 18, 2024
680e4c2
Revise proof of dfrecs3 to use new definition of wrecs
sctfn Nov 18, 2024
fed1b19
Bring csbpredg, csbdif up, prove csbfrecsg
sctfn Nov 18, 2024
f667a02
Prove csbwrecsg with the new definition
sctfn Nov 18, 2024
5fe17aa
regen disc
sctfn Nov 18, 2024
eefc913
rewrap
sctfn Nov 18, 2024
a6debec
add $j for fpr2a
sctfn Nov 18, 2024
66ab190
incorporate benjub's suggestions
sctfn Nov 18, 2024
2c76746
verify cleanup
sctfn Nov 18, 2024
b29b64a
rewrap
sctfn Nov 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions changes-set.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,13 @@ make a github issue.)

DONE:
Date Old New Notes
18-Nov-24 csbcog [same] moved from RP's mathbox to main set.mm
18-Nov-24 csbwrecsg [same] moved from ML's mathbox to main set.mm
18-Nov-24 csbpredg [same] moved from ML's mathbox to main set.mm
18-Nov-24 csbdif [same] moved from ML's mathbox to main set.mm
18-Nov-24 df-wrecs dfwrecsOLD obsoleted
18-Nov-24 dfwrecs2 df-wrecs moved from BJ's mathbox to main set.mm and
made the main definition
16-Nov-24 rspcdvinvd rspcdv2 moved from SP's mathbox to main set.mm
12-Nov-24 sseldi sselid compare to sselii or sseldd
11-Nov-24 mpteq12da [same] moved from GS's mathbox to main set.mm
Expand Down
Loading
Loading