pair-eta

yiyunliu/pair-eta

Fork 0

Commit graph

7b86311260 Prove diamond for EPar Yiyun Liu 2024-12-24 00:12:42 -05:00
233f229b3f Add Abs_EPar' Yiyun Liu 2024-12-23 23:44:57 -05:00
86dab74384 Add outermost expansion and some related lemmas Yiyun Liu 2024-12-23 01:13:55 -05:00
a38a6eb8e8 Stuck at diamodn property Yiyun Liu 2024-12-22 23:51:01 -05:00
df9c91dad5 Start EPar_diamond Yiyun Liu 2024-12-22 16:06:36 -05:00
6daef9c807 Finish full commutativity Yiyun Liu 2024-12-22 15:44:48 -05:00
4599c1d65d Finish commutativity proof Yiyun Liu 2024-12-22 15:22:41 -05:00
fbe0bc4acc Finish Pair EPar Yiyun Liu 2024-12-22 15:08:01 -05:00
086e68f43e Prove one Pair EPar case Yiyun Liu 2024-12-22 12:40:20 -05:00
ecee278d04 Write down the statement of pair_epar Yiyun Liu 2024-12-22 12:12:25 -05:00
ccbb9a1395 Simplify the syntax by combining proj1 and proj2 Yiyun Liu 2024-12-22 10:38:58 -05:00
e8ec23a3e7 Add the substitution lemmas for RPars Yiyun Liu 2024-12-21 22:36:14 -05:00
2bffbcaf0c Work on RPar morphing Yiyun Liu 2024-12-21 00:57:00 -05:00
7e4b0f3e81 Minor Yiyun Liu 2024-12-21 00:05:42 -05:00
ec19e91a47 Finish Abs_EPar Yiyun Liu 2024-12-20 23:58:44 -05:00
393a022f04 Fix Abs_EPar Yiyun Liu 2024-12-20 22:56:08 -05:00
a9de3013c9 Revise the par reduction relation master Yiyun Liu 2024-12-20 16:26:32 -05:00
67bcc69de7 par eta is too complex Yiyun Liu 2024-12-20 16:19:35 -05:00
9dda22dae2 Work on Abs_EPar Yiyun Liu 2024-12-17 01:55:28 -05:00
a285b44a46 Add more cases Yiyun Liu 2024-12-17 00:41:32 -05:00
45bc061b4d Change the definition of commutativity Yiyun Liu 2024-12-16 21:41:29 -05:00
b0dbcba2d0 Add dependent inversion principle Yiyun Liu 2024-12-16 19:56:27 -05:00
d723ee4675 Revise reduction rules Yiyun Liu 2024-12-16 18:00:08 -05:00
ace1325da8 Add rules Yiyun Liu 2024-12-13 11:09:00 -05:00
145e316a4b Initial commit Yiyun Liu 2024-12-11 23:52:57 -05:00