Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
7
 Projects Packages Public activity Starred repositories
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-01-30 23:29:34 -05:00
5a7f46a8a1 Finish the enhanced eta postponement
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-01-30 23:10:17 -05:00
51ac5ffbd6 Finish eta postponement
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-01-30 22:36:49 -05:00
9134cfec8a Finish a few cases of eta postponement
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-01-30 20:24:01 -05:00
d925a8bcaa Minor cleanup
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-01-30 20:23:45 -05:00
fc666956e2 Finish off the SN proof
64e558f09e Finish sn unsubst
c83be03230 Finish antirenaming
e4c2bd39db Finish the eta split proof without any admits
20eef78014 Finish one example case of violate sn
Compare 18 commits »
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-30 20:23:36 -05:00
fc666956e2 Finish off the SN proof
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-30 20:17:13 -05:00
64e558f09e Finish sn unsubst
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-30 16:15:02 -05:00
c83be03230 Finish antirenaming
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-29 23:41:50 -05:00
e4c2bd39db Finish the eta split proof without any admits
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-29 23:00:06 -05:00
20eef78014 Finish one example case of violate sn
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-29 22:25:20 -05:00
aa2c2ca151 Add lemmas that bad forms are impossible
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-29 22:19:51 -05:00
a47d69f427 More no forbid
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-29 22:09:13 -05:00
99b5e87ea3 Finish red sn preservation
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-29 21:27:59 -05:00
369bd55932 Add red sn preservation
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-29 15:52:25 -05:00
5f619c0980 Finish the split lemma up to strong normalization
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-29 14:01:45 -05:00
710b59fd8f Prove all application cases
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-29 13:38:05 -05:00
08b9395acb Push some important cases of the split lemma
yiyunliu pushed to tstar at yiyunliu/sp-eta-postpone 2025-01-29 12:19:58 -05:00
a27c41c5d1 Add lemmas that bad forms are impossible
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-28 16:41:24 -05:00
3f3703990d Save progress
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-28 16:08:16 -05:00
24693b8928 Add "beta-free" eta contraction