01f7f678d3
Prove congruence of various operations
...
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-07-22 18:02:45 +02:00
14f1494fc3
Provide a definition of partial congruence
...
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-07-22 18:01:48 +02:00
d3bac2fe60
Switch to representing least/greatest with absorption
...
It's more convenient this way to require non-partiality.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-07-22 17:59:54 +02:00
5705f256fd
Prove some quasi-homomorphism properties
...
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-07-11 15:49:56 +02:00
d59ae90cef
Lock down more equivalence relation proofs
...
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-07-11 15:46:18 +02:00
c1c34c69a5
Strengthen absorption laws
...
If x \/ y is defined, x /\ (x \/ y) has to be defined,
too. Previously, we stated them in terms of
"if x /\ (x \/ y) is defined", which is not right.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-07-11 15:44:29 +02:00
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
