Comments
-
soupel 1 year ago1 + 1 = 3 -
-
Also out of boredom I might try to split that into sections based on what the theorems are generally about
- Real/complex - 2p2e4 <- 2cn <- 2re <- 1re <- axrrecex
- Signed reals - recexsr <- sqgt0sr <- pn0sr <- distrsr <- dmaddsr <- addclsr <- addsrpr <- enrer
- Positive reals - addcanpr <- ltapr <- ltaprlem <- ltexpri <- ltexprlem7 <- ltaddpr <- addclpr <- addclprlem2 <- addclprlem1
- Positive rationals - ltrnq <- dmrecnq <- recclnq <- recidnq <- recmulnq <- mulassnq <- mulerpq <- nqereq <- nqercl <- nqerf <- nqereu <- enqer
- Positive integers - mulcanpi
- Naturals - nnmcan <- nnmword <- nnmord <- nnmordi <- nnaword1 <- nnaword <- nnaord <- nnaordi <- nnasuc
- Ordinal addition - onasuc
- Recursive definition generator - frsuc <- rdgsucg <- rdgdmlim
- Strong transfinite recursion - tfr1a <- tfrlem16 <- tfrlem15 <- tfrlem13 <- tfrlem12 <- tfrlem11 <- tfrlem10 <- tfrlem7 <- tfrlem5 <- tfrlem2 <- tfrlem1
- Function values - fvreseq <- eqfnfv <- mpteqb <- fvmpt2 <- fvmpt2i <- fvmpti <- fvmptg <- fvopab3ig <- funopfv <- funbrfv
- Functions - funeu <- funmo <- dffun6 <- dffun6f <- dffun3 <- dffun2
- Binary relations - brcnv <- brcnvg <- opelcnvg <- brabg <- brabga
- Ordered pairs - opelopabga <- copsex2g <- copsexg <- eqvinop <- opth2 <- opthg2 <- opthg <- opth <- opeq1d <- opeq1
- Conditional operator - ifbieq1d <- ifeq1d <- ifeq1 <- dfif6
- Union - uneq12i <- uneq12 <- uneq2 <- uncom <- uneqri <- elun
- Implicit substitution - elab2g <- elabg <- elabgf <- vtoclgf
- Non-freeness for classes - issetf <- nfeq2 <- nfeq <- nfcri <- nfcrii
- Substitution - hblem <- clelsb1 <- sbco2 <- sbied <- sbie <- sbbi <- sban <- sbim <- sbi2 <- sbn <- dfsb3 <- dfsb2 <- sb4 <- equs5
- Predicate calculus - axc15 <- ax13a2 <- ax13v2 <- dveeq2 <- ax12lem3 <- 19.36v <- 19.36 <- 19.9 <- 19.9h <- 19.9t <- 19.9ht <- a10e <- axc7 <- sp <- 19.8a <- equcoms <- equcomi <- equid <- eximii <- eximi <- exim <- alnex
- Propositional calculus - con2bii <- con1bii <- xchbinx <- notbii <- notbi <- notbid <- 3bitr3g <- syl5bbr <- syl5bb <- bitrd <- bitri <- sylibr <- biimpri <- bicomi <- bicom1 <- bi2 <- dfbi1 <- impbii <- bi3 <- simprim <- impi <- con1i <- nsyl2 <- mt3d <- con1d <- notnot1 <- con2i <- nsyl3 <- mt2d <- con2d <- notnot2 <- pm2.18d <- pm2.18 <- pm2.21 <- pm2.21d <- a1d <- syl <- mpd <- a2i <- ax-2
Those last three could probably be subdivided further -
Ah I must've misremembered generally talking about it on the TBGs as introducing it to you at some point, but yeah I did (I even downloaded the verifier so I could try making a proof myself (I did not end up making a proof myself))
