subttle / kleene Goto Github PK

-- https://pdfs.semanticscholar.org/6f33/978012f794cc5fff60506db730e6a15185e7.pdf  -- Introduction to Kleene Algebra Lecture 7, Equational Theory of Kleene Algebra
-- https://pdfs.semanticscholar.org/58e7/4d6c5c462887f7e1ebb9b092554397b89b3b.pdf  -- Kleene Algebra Completeness
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l01-intro.pdf           -- Course Roadmap
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l02-axioms.pdf          -- Introduction to Kleene Algebra Lecture 2, Axioms of Kleene Algebra
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l03-alt.pdf             -- Alternative Axiomatizations
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l04-eqthy.pdf           -- Characterizing the Equational Theory
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l06-adj.pdf             -- Relations Among Algebras
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l07-complete.pdf        -- Equational Theory of Kleene Algebra
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l08-complete.pdf        -- Finite Automata
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l09-complete.pdf        -- Completeness
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l10-complexity.pdf      -- Complexity of the Equational Theory
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l19-kat.pdf             -- Kleene Algebra with Tests
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l20-katmodels.pdf       -- Models of KAT
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l21-katcomplete.pdf     -- Completeness of KAT
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l22-katHoare.pdf        -- KAT and Hoare Logic
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l23-katcomplete.pdf     -- Completeness of KAT for the Hoare Theory of Relational Models
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l24-complexity.pdf      -- Complexity of Kleene Algebra with Tests
-- http://www.cs.cornell.edu/courses/cs786/2004sp/Lectures/l25-phlcomplexity.pdf   -- Complexity of PHL
-- https://www.cs.cornell.edu/~kozen/Papers/ka.pdf                                 -- A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events

bisimulation : ∀ {a b x : A} → a   ∙ x ≡ x ∙ b
                             → a * ∙ x ≡ x ∙ b *
bisimulation {a} {b} {x} ax≡xb = {!   !}

-- sliding rule
sliding : ∀ {a b : A} → (a ∙ b) * ≡ a ∙ (b ∙ a) *
sliding {a} {b} = {!   !}

-- denesting rule
denesting : ∀ {x y z : A} → (x + y) * ≡ x * ∙ (y ∙ x *) *
denesting = {!   !}