Yiyun Liu
|
4599c1d65d
|
Finish commutativity proof
|
2024-12-22 15:22:41 -05:00 |
|
Yiyun Liu
|
fbe0bc4acc
|
Finish Pair EPar
|
2024-12-22 15:08:01 -05:00 |
|
|
|
086e68f43e
|
Prove one Pair EPar case
|
2024-12-22 12:40:20 -05:00 |
|
|
|
ecee278d04
|
Write down the statement of pair_epar
|
2024-12-22 12:12:34 -05:00 |
|
|
|
ccbb9a1395
|
Simplify the syntax by combining proj1 and proj2
|
2024-12-22 10:38:58 -05:00 |
|
|
|
e8ec23a3e7
|
Add the substitution lemmas for RPars
|
2024-12-21 22:36:14 -05:00 |
|
|
|
2bffbcaf0c
|
Work on RPar morphing
|
2024-12-21 00:57:00 -05:00 |
|
|
|
7e4b0f3e81
|
Minor
|
2024-12-21 00:05:42 -05:00 |
|
|
|
ec19e91a47
|
Finish Abs_EPar
|
2024-12-20 23:58:44 -05:00 |
|
|
|
393a022f04
|
Fix Abs_EPar
|
2024-12-20 22:56:08 -05:00 |
|
|
|
67bcc69de7
|
par eta is too complex
|
2024-12-20 16:19:35 -05:00 |
|
Yiyun Liu
|
9dda22dae2
|
Work on Abs_EPar
|
2024-12-17 01:55:28 -05:00 |
|
Yiyun Liu
|
a285b44a46
|
Add more cases
|
2024-12-17 00:41:32 -05:00 |
|
|
|
45bc061b4d
|
Change the definition of commutativity
|
2024-12-16 21:41:29 -05:00 |
|
|
|
b0dbcba2d0
|
Add dependent inversion principle
|
2024-12-16 19:56:27 -05:00 |
|
|
|
d723ee4675
|
Revise reduction rules
|
2024-12-16 18:00:08 -05:00 |
|
|
|
ace1325da8
|
Add rules
|
2024-12-13 11:09:00 -05:00 |
|
|
|
145e316a4b
|
Initial commit
|
2024-12-11 23:52:57 -05:00 |
|
