Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
4
 Projects Packages Public activity Starred repositories
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
yiyunliu created branch nonessential in yiyunliu/sp-eta-postpone 2025-01-28 15:14:42 -05:00
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-28 15:14:42 -05:00
61e743ee74 Add ne ered
yiyunliu pushed to tstar at yiyunliu/sp-eta-postpone 2025-01-27 22:47:34 -05:00
5ea75052a5 Show that eta expansion can be immediately be removed by beta
yiyunliu pushed to tstar at yiyunliu/sp-eta-postpone 2025-01-27 16:48:50 -05:00
b8d7ebfaa2 Fix the broken pair eta rule