refactor: review Kleene algebra axioms#35963
refactor: review Kleene algebra axioms#35963Parcly-Taxel wants to merge 10 commits intoleanprover-community:masterfrom
Conversation
PR summary cd57315234Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
vihdzp
left a comment
There was a problem hiding this comment.
This looks reasonable to me, but I'm not an expert in this area, so I won't give explicit approval.
Derive
which is Proposition 2 in Kozen's 1994 paper.
We also remove the
botandbot_lefields inIdemSemiring, since the remaining axioms already show0 ≤ afor alla.