-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.KnuckleDragger.Kleene
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Example use of the KnuckleDragger layer, proving some Kleene algebra theorems.
--
-- Based on <http://www.philipzucker.com/bryzzowski_kat/>
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE TemplateHaskell      #-}
{-# LANGUAGE TypeAbstractions     #-}

{-# OPTIONS_GHC -Wall -Werror -Wno-unused-matches #-}

module Documentation.SBV.Examples.KnuckleDragger.Kleene where

import Prelude hiding((<=))

import Data.SBV
import Data.SBV.Tools.KnuckleDragger

-- | An uninterpreted sort, corresponding to the type of Kleene algebra strings.
data Kleene
mkUninterpretedSort ''Kleene

-- | Star operator over kleene algebras. We're leaving this uninterpreted.
star :: SKleene -> SKleene
star :: SKleene -> SKleene
star = String -> SKleene -> SKleene
forall a. SMTDefinable a => String -> a
uninterpret String
"STAR"

-- | The 'Num' instance for Kleene makes it easy to write regular expressions
-- in the more familiar form.
instance Num SKleene where
  + :: SKleene -> SKleene -> SKleene
(+) = String -> SKleene -> SKleene -> SKleene
forall a. SMTDefinable a => String -> a
uninterpret String
"PAR"
  * :: SKleene -> SKleene -> SKleene
(*) = String -> SKleene -> SKleene -> SKleene
forall a. SMTDefinable a => String -> a
uninterpret String
"SEQ"

  abs :: SKleene -> SKleene
abs    = String -> SKleene -> SKleene
forall a. HasCallStack => String -> a
error String
"SKleene: not defined: abs"
  signum :: SKleene -> SKleene
signum = String -> SKleene -> SKleene
forall a. HasCallStack => String -> a
error String
"SKleene: not defined: signum"
  negate :: SKleene -> SKleene
negate = String -> SKleene -> SKleene
forall a. HasCallStack => String -> a
error String
"SKleene: not defined: signum"

  fromInteger :: Integer -> SKleene
fromInteger Integer
0 = String -> SKleene
forall a. SMTDefinable a => String -> a
uninterpret String
"zero"
  fromInteger Integer
1 = String -> SKleene
forall a. SMTDefinable a => String -> a
uninterpret String
"one"
  fromInteger Integer
n = String -> SKleene
forall a. HasCallStack => String -> a
error (String -> SKleene) -> String -> SKleene
forall a b. (a -> b) -> a -> b
$ String
"SKleene: not defined: fromInteger " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n

-- | The set of strings matched by one regular expression is a subset of the second,
-- if adding it to the second doesn't change the second set.
(<=) :: SKleene -> SKleene -> SBool
SKleene
x <= :: SKleene -> SKleene -> SBool
<= SKleene
y = SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
y SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
y

-- | A sequence of Kleene algebra proofs. See <http://www.cs.cornell.edu/~kozen/Papers/ka.pdf>
--
-- We have:
--
-- >>> kleeneProofs
-- Axiom: par_assoc
-- Axiom: par_comm
-- Axiom: par_idem
-- Axiom: par_zero
-- Axiom: seq_assoc
-- Axiom: seq_zero
-- Axiom: seq_one
-- Axiom: rdistrib
-- Axiom: ldistrib
-- Axiom: unfold
-- Axiom: least_fix
-- Lemma: par_lzero                        Q.E.D.
-- Lemma: par_monotone                     Q.E.D.
-- Lemma: seq_monotone                     Q.E.D.
-- Lemma: star_star_1
--   Step: 1 (unfold)                      Q.E.D.
--   Step: 2 (factor out x * star x)       Q.E.D.
--   Step: 3 (par_idem)                    Q.E.D.
--   Step: 4 (unfold)                      Q.E.D.
--   Result:                               Q.E.D.
-- Lemma: subset_eq                        Q.E.D.
-- Lemma: star_star_2_2                    Q.E.D.
-- Lemma: star_star_2_3                    Q.E.D.
-- Lemma: star_star_2_1                    Q.E.D.
-- Lemma: star_star_2                      Q.E.D.
kleeneProofs :: IO ()
kleeneProofs :: IO ()
kleeneProofs = KD () -> IO ()
forall a. KD a -> IO a
runKD (KD () -> IO ()) -> KD () -> IO ()
forall a b. (a -> b) -> a -> b
$ do

  -- Kozen axioms
  Proof
par_assoc <- String
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> KD Proof
forall a. Proposition a => String -> a -> KD Proof
axiom String
"par_assoc" ((Forall "x" Kleene
  -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
 -> KD Proof)
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> KD Proof
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" (SKleene
x :: SKleene)) (Forall @"y" SKleene
y) (Forall @"z" SKleene
z) -> SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ (SKleene
y SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
z) SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
y) SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
z
  Proof
par_comm  <- String
-> (Forall "x" Kleene -> Forall "y" Kleene -> SBool) -> KD Proof
forall a. Proposition a => String -> a -> KD Proof
axiom String
"par_comm"  ((Forall "x" Kleene -> Forall "y" Kleene -> SBool) -> KD Proof)
-> (Forall "x" Kleene -> Forall "y" Kleene -> SBool) -> KD Proof
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" (SKleene
x :: SKleene)) (Forall @"y" SKleene
y)                 -> SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
y       SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
y SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
x
  Proof
par_idem  <- String -> (Forall "x" Kleene -> SBool) -> KD Proof
forall a. Proposition a => String -> a -> KD Proof
axiom String
"par_idem"  ((Forall "x" Kleene -> SBool) -> KD Proof)
-> (Forall "x" Kleene -> SBool) -> KD Proof
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" (SKleene
x :: SKleene))                                 -> SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
x       SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
x
  Proof
par_zero  <- String -> (Forall "x" Kleene -> SBool) -> KD Proof
forall a. Proposition a => String -> a -> KD Proof
axiom String
"par_zero"  ((Forall "x" Kleene -> SBool) -> KD Proof)
-> (Forall "x" Kleene -> SBool) -> KD Proof
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" (SKleene
x :: SKleene))                                 -> SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
0       SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
x

  Proof
seq_assoc <- String
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> KD Proof
forall a. Proposition a => String -> a -> KD Proof
axiom String
"seq_assoc" ((Forall "x" Kleene
  -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
 -> KD Proof)
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> KD Proof
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" (SKleene
x :: SKleene)) (Forall @"y" SKleene
y) (Forall @"z" SKleene
z) -> SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* (SKleene
y SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene
z) SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene
y) SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene
z
  Proof
seq_zero  <- String -> (Forall "x" Kleene -> SBool) -> KD Proof
forall a. Proposition a => String -> a -> KD Proof
axiom String
"seq_zero"  ((Forall "x" Kleene -> SBool) -> KD Proof)
-> (Forall "x" Kleene -> SBool) -> KD Proof
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" (SKleene
x :: SKleene))                                 -> SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene
0       SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
0
  Proof
seq_one   <- String -> (Forall "x" Kleene -> SBool) -> KD Proof
forall a. Proposition a => String -> a -> KD Proof
axiom String
"seq_one"   ((Forall "x" Kleene -> SBool) -> KD Proof)
-> (Forall "x" Kleene -> SBool) -> KD Proof
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" (SKleene
x :: SKleene))                                 -> SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene
1       SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
x

  Proof
rdistrib  <- String
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> KD Proof
forall a. Proposition a => String -> a -> KD Proof
axiom String
"rdistrib"  ((Forall "x" Kleene
  -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
 -> KD Proof)
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> KD Proof
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" (SKleene
x :: SKleene)) (Forall @"y" SKleene
y) (Forall @"z" SKleene
z) -> SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* (SKleene
y SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
z) SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene
y SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene
z
  Proof
ldistrib  <- String
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> KD Proof
forall a. Proposition a => String -> a -> KD Proof
axiom String
"ldistrib"  ((Forall "x" Kleene
  -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
 -> KD Proof)
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> KD Proof
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" (SKleene
x :: SKleene)) (Forall @"y" SKleene
y) (Forall @"z" SKleene
z) -> (SKleene
y SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
z) SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene
x SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
y SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
z SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene
x

  Proof
unfold    <- String -> (Forall "e" Kleene -> SBool) -> KD Proof
forall a. Proposition a => String -> a -> KD Proof
axiom String
"unfold"    ((Forall "e" Kleene -> SBool) -> KD Proof)
-> (Forall "e" Kleene -> SBool) -> KD Proof
forall a b. (a -> b) -> a -> b
$ \(Forall @"e" SKleene
e) -> SKleene -> SKleene
star SKleene
e SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
1 SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
e SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
e

  Proof
least_fix <- String
-> (Forall "x" Kleene
    -> Forall "e" Kleene -> Forall "f" Kleene -> SBool)
-> KD Proof
forall a. Proposition a => String -> a -> KD Proof
axiom String
"least_fix" ((Forall "x" Kleene
  -> Forall "e" Kleene -> Forall "f" Kleene -> SBool)
 -> KD Proof)
-> (Forall "x" Kleene
    -> Forall "e" Kleene -> Forall "f" Kleene -> SBool)
-> KD Proof
forall a b. (a -> b) -> a -> b
$ \(Forall @"x" SKleene
x) (Forall @"e" SKleene
e) (Forall @"f" SKleene
f) -> ((SKleene
f SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
e SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene
x) SKleene -> SKleene -> SBool
<= SKleene
x) SBool -> SBool -> SBool
.=> ((SKleene -> SKleene
star SKleene
e SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene
f) SKleene -> SKleene -> SBool
<= SKleene
x)

  -- Collect the basic axioms in a list for easy reference
  let kleene :: [Proof]
kleene = [ Proof
par_assoc,  Proof
par_comm, Proof
par_idem, Proof
par_zero
               , Proof
seq_assoc,  Proof
seq_zero, Proof
seq_one
               , Proof
ldistrib,   Proof
rdistrib
               , Proof
unfold
               , Proof
least_fix
               ]

  -- Various proofs:
  Proof
par_lzero    <- String -> (Forall "x" Kleene -> SBool) -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"par_lzero"    (\(Forall @"x" (SKleene
x :: SKleene)) -> SKleene
0 SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
x SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
x) [Proof]
kleene
  Proof
par_monotone <- String
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"par_monotone" (\(Forall @"x" (SKleene
x :: SKleene)) (Forall @"y" SKleene
y) (Forall @"z" SKleene
z) -> SKleene
x SKleene -> SKleene -> SBool
<= SKleene
y SBool -> SBool -> SBool
.=> ((SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
z) SKleene -> SKleene -> SBool
<= (SKleene
y SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
z))) [Proof]
kleene
  Proof
seq_monotone <- String
-> (Forall "x" Kleene
    -> Forall "y" Kleene -> Forall "z" Kleene -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"seq_monotone" (\(Forall @"x" (SKleene
x :: SKleene)) (Forall @"y" SKleene
y) (Forall @"z" SKleene
z) -> SKleene
x SKleene -> SKleene -> SBool
<= SKleene
y SBool -> SBool -> SBool
.=> ((SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene
z) SKleene -> SKleene -> SBool
<= (SKleene
y SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene
z))) [Proof]
kleene

  -- This one requires a chain of reasoning: x* x* == x*
  Proof
star_star_1  <- String
-> (Forall "x" Kleene -> SBool)
-> (SKleene -> (SBool, KDProofRaw SKleene))
-> KD Proof
forall a steps.
(CalcLemma a steps, Proposition a) =>
String -> a -> steps -> KD Proof
calc String
"star_star_1"
                       (\(Forall @"x" (SKleene
x :: SKleene)) -> SKleene -> SKleene
star SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene -> SKleene
star SKleene
x) ((SKleene -> (SBool, KDProofRaw SKleene)) -> KD Proof)
-> (SKleene -> (SBool, KDProofRaw SKleene)) -> KD Proof
forall a b. (a -> b) -> a -> b
$
                       \SKleene
x -> [] [SBool] -> KDProofRaw SKleene -> (SBool, KDProofRaw SKleene)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SKleene -> SKleene
star SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x                     SKleene -> Proof -> Hinted SKleene
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
unfold
                                KDProofRaw SKleene
-> ChainsTo (KDProofRaw SKleene) -> ChainsTo (KDProofRaw SKleene)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SKleene
1 SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x) SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* (SKleene
1 SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x)
                                SKleene -> [Helper] -> Hinted SKleene
forall a b. HintsTo a b => a -> b -> Hinted a
?? String -> Helper
hcmnt String
"factor out x * star x" Helper -> [Helper] -> [Helper]
forall a. a -> [a] -> [a]
: (Proof -> Helper) -> [Proof] -> [Helper]
forall a b. (a -> b) -> [a] -> [b]
map Proof -> Helper
hprf [Proof]
kleene
                                KDProofRaw SKleene
-> ChainsTo (KDProofRaw SKleene) -> ChainsTo (KDProofRaw SKleene)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: (SKleene
1 SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
1) SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ (SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x) SKleene -> Proof -> Hinted SKleene
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
par_idem
                                KDProofRaw SKleene
-> ChainsTo (KDProofRaw SKleene) -> ChainsTo (KDProofRaw SKleene)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SKleene
1 SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x                      SKleene -> Proof -> Hinted SKleene
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
unfold
                                KDProofRaw SKleene
-> ChainsTo (KDProofRaw SKleene) -> ChainsTo (KDProofRaw SKleene)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SKleene -> SKleene
star SKleene
x
                                SKleene -> ChainsTo SKleene -> ChainsTo SKleene
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SKleene
KDProofRaw SKleene
forall a. KDProofRaw a
qed

  Proof
subset_eq   <- String
-> (Forall "x" Kleene -> Forall "y" Kleene -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"subset_eq" (\(Forall @"x" SKleene
x) (Forall @"y" SKleene
y) -> (SKleene
x SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene
y) SBool -> SBool -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SKleene
x SKleene -> SKleene -> SBool
<= SKleene
y SBool -> SBool -> SBool
.&& SKleene
y SKleene -> SKleene -> SBool
<= SKleene
x)) [Proof]
kleene

  -- Prove: x** = x*
  Proof
star_star_2 <- do Proof
_1 <- String -> (Forall "x" Kleene -> SBool) -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"star_star_2_2" (\(Forall @"x" SKleene
x) -> ((SKleene -> SKleene
star SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
* SKleene -> SKleene
star SKleene
x SKleene -> SKleene -> SKleene
forall a. Num a => a -> a -> a
+ SKleene
1) SKleene -> SKleene -> SBool
<= SKleene -> SKleene
star SKleene
x) SBool -> SBool -> SBool
.=> SKleene -> SKleene
star (SKleene -> SKleene
star SKleene
x) SKleene -> SKleene -> SBool
<= SKleene -> SKleene
star SKleene
x) [Proof]
kleene
                    Proof
_2 <- String -> (Forall "x" Kleene -> SBool) -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"star_star_2_3" (\(Forall @"x" SKleene
x) -> SKleene -> SKleene
star (SKleene -> SKleene
star SKleene
x) SKleene -> SKleene -> SBool
<= SKleene -> SKleene
star SKleene
x)                                       ([Proof]
kleene [Proof] -> [Proof] -> [Proof]
forall a. [a] -> [a] -> [a]
++ [Proof
_1])
                    Proof
_3 <- String -> (Forall "x" Kleene -> SBool) -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"star_star_2_1" (\(Forall @"x" SKleene
x) -> SKleene -> SKleene
star SKleene
x        SKleene -> SKleene -> SBool
<= SKleene -> SKleene
star (SKleene -> SKleene
star SKleene
x))                                [Proof]
kleene

                    String -> (Forall "x" Kleene -> SBool) -> [Proof] -> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"star_star_2" (\(Forall @"x" (SKleene
x :: SKleene)) -> SKleene -> SKleene
star (SKleene -> SKleene
star SKleene
x) SKleene -> SKleene -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SKleene -> SKleene
star SKleene
x) [Proof
subset_eq, Proof
_2, Proof
_3]

  () -> KD ()
forall a. a -> KD a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()