Commit graph

Select branches

Hide pull requests

master

nonessential

tstar

Mono Color

• d925a8bcaa Minor cleanup master Yiyun Liu 2025-01-30 20:23:57 -05:00
• fc666956e2 Finish off the SN proof nonessential Yiyun Liu 2025-01-30 20:23:25 -05:00
• 64e558f09e Finish sn unsubst Yiyun Liu 2025-01-30 20:17:00 -05:00
• c83be03230 Finish antirenaming Yiyun Liu 2025-01-30 16:14:03 -05:00
• e4c2bd39db Finish the eta split proof without any admits Yiyun Liu 2025-01-29 23:41:38 -05:00
• 20eef78014 Finish one example case of violate sn Yiyun Liu 2025-01-29 22:59:57 -05:00
• aa2c2ca151 Add lemmas that bad forms are impossible Yiyun Liu 2025-01-29 22:25:14 -05:00
• a47d69f427 More no forbid Yiyun Liu 2025-01-29 22:14:01 -05:00
• 99b5e87ea3 Finish red sn preservation Yiyun Liu 2025-01-29 22:09:08 -05:00
• 369bd55932 Add red sn preservation Yiyun Liu 2025-01-29 21:27:49 -05:00
• 5f619c0980 Finish the split lemma up to strong normalization Yiyun Liu 2025-01-29 15:52:05 -05:00
• 710b59fd8f Prove all application cases Yiyun Liu 2025-01-29 14:01:35 -05:00
• 08b9395acb Push some important cases of the split lemma Yiyun Liu 2025-01-29 13:37:54 -05:00
• a27c41c5d1 Add lemmas that bad forms are impossible tstar Yiyun Liu 2025-01-29 12:19:45 -05:00
• 3f3703990d Save progress Yiyun Liu 2025-01-28 16:37:23 -05:00
• 24693b8928 Add "beta-free" eta contraction Yiyun Liu 2025-01-28 16:07:52 -05:00
• 61e743ee74 Add ne ered Yiyun Liu 2025-01-28 15:13:41 -05:00
• 5ea75052a5 Show that eta expansion can be immediately be removed by beta Yiyun Liu 2025-01-27 22:47:10 -05:00
• b8d7ebfaa2 Fix the broken pair eta rule Yiyun Liu 2025-01-27 16:48:38 -05:00
• 9f80013df6 Add tstar to preserve eta normal forms Yiyun Liu 2025-01-27 16:44:48 -05:00
• 11d23afa45 Remove the typed postponement theorem Yiyun Liu 2025-01-26 14:51:47 -05:00
• 263fbf7fb6 Finish most of the preservation proof Yiyun Liu 2025-01-25 23:10:29 -05:00
• 8463b4067f Figured out Yiyun Liu 2025-01-25 23:06:38 -05:00
• df62e3691c Need to parallelize eta Yiyun Liu 2025-01-25 16:53:48 -07:00
• 8fcfa5dbf9 "Finish" eta postponement proof Yiyun Liu 2025-01-25 16:26:55 -07:00
• 2f04bcc75c Add a mostly finished eta postponement proof Yiyun Liu 2025-01-25 16:08:21 -07:00