Yiyun Liu yiyunliu · he/him
0 followers · 0 following
Repositories
4
 Projects Packages Public activity Starred repositories
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
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-22 01:29:31 -05:00
2ab47ac883 Finish eta postponement
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-22 01:20:48 -05:00
f44c8ef425 Only the indsucc case remaining for postponement
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-22 00:10:27 -05:00
d9d0e9cdd4 One remaining case for eta postponement
yiyunliu pushed to nat at yiyunliu/sp-eta-postpone 2025-02-21 23:43:51 -05:00
29d05befe9 Seemingly redundant nonelim cases