|
|
d2faada90a
|
Add a left and right version of identity
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2025-07-11 15:43:27 +02:00 |
|
|
|
7fdbf0397d
|
Prove idempotence of value combining
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2025-07-05 16:57:24 -07:00 |
|
|
|
fdef8c0a60
|
Prove commutativity and associativity of value joining
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2025-07-05 16:49:38 -07:00 |
|
|
|
c48bd0272e
|
Define "less than or equal" for partial lattices and prove some properties
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2025-07-05 14:53:00 -07:00 |
|
|
|
d251915772
|
Show that lifted equality preserves equivalences
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2025-07-05 14:52:40 -07:00 |
|
|
|
da6e82d04b
|
Add helper definitions for partial commutativity, associativity, reflexivity
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2025-07-02 15:11:12 -05:00 |
|
|
|
dd101c6e9b
|
Start working on a general lattice builder framework
|
2025-06-29 10:35:37 -07:00 |
|
