Yiyun Liu yiyunliu · he/him
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-02-03 14:55:50 -05:00
84cd0715c7 Prove structural properties of DJoin
3d42581bbe Finish the confluence proof
f3f3991b02 Finish rred standardization
a0c20851fe Prove confluence of beta
cf31e6d285 Finish the confluence proof of ered
Compare 8 commits »
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-03 14:55:40 -05:00
84cd0715c7 Prove structural properties of DJoin
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-03 14:23:19 -05:00
3d42581bbe Finish the confluence proof
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-03 12:17:02 -05:00
f3f3991b02 Finish rred standardization
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-02 21:57:49 -05:00
a0c20851fe Prove confluence of beta
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-02 20:48:54 -05:00
cf31e6d285 Finish the confluence proof of ered
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-02 20:21:14 -05:00
376fce619c Save progress
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-02 20:08:47 -05:00
5624415bc9 Finish antirenaming for injective rens
yiyunliu created branch antirenaming in yiyunliu/sp-eta-postpone 2025-02-02 19:42:59 -05:00
yiyunliu pushed to antirenaming at yiyunliu/sp-eta-postpone 2025-02-02 19:42:59 -05:00
6cc3a65163 Discharge one case of antirenaming using injective renaming
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-01-31 21:57:11 -05:00
ecb50f1ab7 Add comment about the antirenaming proof
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-01-31 21:46:05 -05:00
d2cd3105c7 stuck on antirenaming because of scoped syntax
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-01-31 20:54:43 -05:00
580e3a8251 Prove that ered is strongly normalizing
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-01-31 20:12:39 -05:00
f57e10be93 Finish extracting leftmost-outermost red from sn
yiyunliu pushed to master at yiyunliu/sp-eta-postpone 2025-01-31 17:32:48 -05:00
571779a4dd Fix name change errors for EPar
5dd3428e2b Merge remote-tracking branch 'forgejo/nonessential'
47473fd3cd Minor
Compare 3 commits »
yiyunliu pushed to nonessential at yiyunliu/sp-eta-postpone 2025-01-31 16:30:09 -05:00
47473fd3cd Minor
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