Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
7
 Projects Packages Public activity Starred repositories
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-25 20:18:49 -05:00
96bc223b0a Finish renaming and preservation
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-25 16:50:19 -05:00
cc0e9219c4 Finish two cases of renaming
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-25 16:12:53 -05:00
291d821d94 Add some admits to work on later
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-25 16:06:11 -05:00
b2aec9c6ce Add syntactic typing rules
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-25 15:46:32 -05:00
4dd2cd7cd8 Finish indzero and indsuc rules
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-25 15:29:30 -05:00
890f97365c Finish the indcong rule
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-25 15:05:16 -05:00
e89aaf14a0 Define cleaned up version of gamma eq
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-25 12:48:48 -05:00
133bcd55c2 Need to fix gamma eq
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-24 15:20:38 -05:00
1effbd3d85 Finish morphing_SemWt
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-24 13:51:49 -05:00
9cb7f31cdb Finish ST_Ind
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-24 01:25:16 -05:00
2a24700f9a One case left for nat
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-24 01:06:59 -05:00
5544e401a2 Make some progress on the ST_Ind case
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-23 16:01:59 -05:00
8df64ef989 Write down the statement for ST_Ind
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-23 15:19:07 -05:00
4e9a5582d2 Fix InterpUniv Sub
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-23 14:58:33 -05:00
fabc39b92a Add no confusion lemmas
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-23 14:34:04 -05:00
92e418666f Add the case for SNat
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-23 14:07:24 -05:00
bf6d7db877 Add definition for snat
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-23 13:59:01 -05:00
ffb57a91f4 Update the syntactic reduction lemmas
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-23 01:13:50 -05:00
f8da81ad74 Work on local confluence
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-22 01:33:50 -05:00
6b8120848b Minor