-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.KnuckleDragger.ShefferStroke
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Inspired by https://www.philipzucker.com/cody_sheffer/, proving
-- that the axioms of sheffer stroke (i.e., nand in traditional boolean
-- logic), imply it is a boolean algebra.
-----------------------------------------------------------------------------

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.KnuckleDragger.ShefferStroke where

import Prelude hiding ((<))
import Data.List (intercalate)

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

-- * Generalized Boolean Algebras

-- | Capture what it means to be a boolean algebra. We follow Lean's
-- definition, as much as we can: <https://leanprover-community.github.io/mathlib_docs/order/boolean_algebra.html>.
-- Since there's no way in Haskell to capture properties together with a class, we'll represent the properties
-- separately.
class BooleanAlgebra α where
  ﬧ    :: α -> α
  (⨆)  :: α -> α -> α
  (⨅)  :: α -> α -> α
  (≤)  :: α -> α -> SBool
  (<)  :: α -> α -> SBool
  (\\) :: α -> α -> α
  (⇨)  :: α -> α -> α
  ⲳ    :: α
  т    :: α

  infix  4 ≤
  infixl 6 ⨆
  infixl 7 ⨅

-- | Proofs needed for a boolean-algebra. Again, we follow Lean's definition here. Since we cannot
-- put these in the class definition above, we will keep them in a simple data-structure.
data BooleanAlgebraProof = BooleanAlgebraProof {
    BooleanAlgebraProof -> Proof
le_refl          {- ∀ (a : α), a ≤ a                             -} :: Proof
  , BooleanAlgebraProof -> Proof
le_trans         {- ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c         -} :: Proof
  , BooleanAlgebraProof -> Proof
lt_iff_le_not_le {- (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a)        -} :: Proof
  , BooleanAlgebraProof -> Proof
le_antisymm      {- ∀ (a b : α), a ≤ b → b ≤ a → a = b           -} :: Proof
  , BooleanAlgebraProof -> Proof
le_sup_left      {- ∀ (a b : α), a ≤ a ⊔ b                       -} :: Proof
  , BooleanAlgebraProof -> Proof
le_sup_right     {- ∀ (a b : α), b ≤ a ⊔ b                       -} :: Proof
  , BooleanAlgebraProof -> Proof
sup_le           {- ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c     -} :: Proof
  , BooleanAlgebraProof -> Proof
inf_le_left      {- ∀ (a b : α), a ⊓ b ≤ a                       -} :: Proof
  , BooleanAlgebraProof -> Proof
inf_le_right     {- ∀ (a b : α), a ⊓ b ≤ b                       -} :: Proof
  , BooleanAlgebraProof -> Proof
le_inf           {- ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c     -} :: Proof
  , BooleanAlgebraProof -> Proof
le_sup_inf       {- ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z -} :: Proof
  , BooleanAlgebraProof -> Proof
inf_compl_le_bot {- ∀ (x : α), x ⊓ xᶜ ≤ ⊥                        -} :: Proof
  , BooleanAlgebraProof -> Proof
top_le_sup_compl {- ∀ (x : α), ⊤ ≤ x ⊔ xᶜ                        -} :: Proof
  , BooleanAlgebraProof -> Proof
le_top           {- ∀ (a : α), a ≤ ⊤                             -} :: Proof
  , BooleanAlgebraProof -> Proof
bot_le           {- ∀ (a : α), ⊥ ≤ a                             -} :: Proof
  , BooleanAlgebraProof -> Proof
sdiff_eq         {- (∀ (x y : α), x \ y = x ⊓ yᶜ)                -} :: Proof
  , BooleanAlgebraProof -> Proof
himp_eq          {- (∀ (x y : α), x ⇨ y = y ⊔ xᶜ)                -} :: Proof
  }

-- | A somewhat prettier printer for a BooleanAlgebra proof
instance Show BooleanAlgebraProof where
  show :: BooleanAlgebraProof -> String
show BooleanAlgebraProof
p = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [ String
"BooleanAlgebraProof {"
                            , String
"  le_refl         : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
le_refl          BooleanAlgebraProof
p)
                            , String
"  le_trans        : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
le_trans         BooleanAlgebraProof
p)
                            , String
"  lt_iff_le_not_le: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
lt_iff_le_not_le BooleanAlgebraProof
p)
                            , String
"  le_antisymm     : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
le_antisymm      BooleanAlgebraProof
p)
                            , String
"  le_sup_left     : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
le_sup_left      BooleanAlgebraProof
p)
                            , String
"  le_sup_right    : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
le_sup_right     BooleanAlgebraProof
p)
                            , String
"  sup_le          : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
sup_le           BooleanAlgebraProof
p)
                            , String
"  inf_le_left     : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
inf_le_left      BooleanAlgebraProof
p)
                            , String
"  inf_le_right    : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
inf_le_right     BooleanAlgebraProof
p)
                            , String
"  le_inf          : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
le_inf           BooleanAlgebraProof
p)
                            , String
"  le_sup_inf      : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
le_sup_inf       BooleanAlgebraProof
p)
                            , String
"  inf_compl_le_bot: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
inf_compl_le_bot BooleanAlgebraProof
p)
                            , String
"  top_le_sup_compl: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
top_le_sup_compl BooleanAlgebraProof
p)
                            , String
"  le_top          : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
le_top           BooleanAlgebraProof
p)
                            , String
"  bot_le          : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
bot_le           BooleanAlgebraProof
p)
                            , String
"  sdiff_eq        : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
sdiff_eq         BooleanAlgebraProof
p)
                            , String
"  himp_eq         : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof
himp_eq          BooleanAlgebraProof
p)
                            , String
"}"
                            ]

-- * The sheffer stroke

-- | The abstract type for the domain.
data Stroke
mkUninterpretedSort ''Stroke

-- | The sheffer stroke operator.
(⏐) :: SStroke -> SStroke -> SStroke
⏐ :: SStroke -> SStroke -> SStroke
(⏐) = String -> SStroke -> SStroke -> SStroke
forall a. SMTDefinable a => String -> a
uninterpret String
"⏐"
infixl 7 ⏐

-- | The boolean algebra of the sheffer stroke.
instance BooleanAlgebra SStroke where
  ﬧ :: SStroke -> SStroke
ﬧ SStroke
x    = SStroke
x SStroke -> SStroke -> SStroke
⏐ SStroke
x
  SStroke
a ⨆ :: SStroke -> SStroke -> SStroke
⨆ SStroke
b  = SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ(SStroke
a SStroke -> SStroke -> SStroke
⏐ SStroke
b)
  SStroke
a ⨅ :: SStroke -> SStroke -> SStroke
⨅ SStroke
b  = SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
⏐ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b
  SStroke
a ≤ :: SStroke -> SStroke -> SBool
≤ SStroke
b  = SStroke
a SStroke -> SStroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a
  SStroke
a < :: SStroke -> SStroke -> SBool
< SStroke
b  = SStroke
a SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
b SBool -> SBool -> SBool
.&& SStroke
a SStroke -> SStroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SStroke
b
  SStroke
a \\ :: SStroke -> SStroke -> SStroke
\\ SStroke
b = SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b
  SStroke
a ⇨ :: SStroke -> SStroke -> SStroke
⇨ SStroke
b  = SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a
  ⲳ :: SStroke
ⲳ      = SStroke
arb SStroke -> SStroke -> SStroke
⏐ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
arb where arb :: SStroke
arb = String -> (SStroke -> SBool) -> SStroke
forall a.
(SymVal a, HasKind a) =>
String -> (SBV a -> SBool) -> SBV a
some String
"ⲳ" (SBool -> SStroke -> SBool
forall a b. a -> b -> a
const SBool
sTrue)
  т :: SStroke
т      = SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
forall α. BooleanAlgebra α => α
ⲳ

-- | Double-negation
ﬧﬧ :: BooleanAlgebra a => a -> a
ﬧﬧ :: forall α. BooleanAlgebra α => α -> α
ﬧﬧ = a -> a
forall α. BooleanAlgebra α => α -> α
ﬧ (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a
forall α. BooleanAlgebra α => α -> α
ﬧ

-- A couple of CPP defines make the code shorter to read
#define A      (Forall @"A"  (a  :: SStroke))
#define AAp A  (Forall @"A'" (a' :: SStroke))
#define AB  A  (Forall @"B"  (b  :: SStroke))
#define ABC AB (Forall @"C"  (c  :: SStroke))
#define X      (Forall @"X"  (x  :: SStroke))
#define XY  X  (Forall @"Y"  (y  :: SStroke))
#define XYZ XY (Forall @"Z"  (z  :: SStroke))

-- | First Sheffer axiom: @ﬧﬧa == a@
sheffer1 :: KD Proof
sheffer1 :: KD Proof
sheffer1 = String -> (Forall "A" Stroke -> SBool) -> KD Proof
forall a. Proposition a => String -> a -> KD Proof
axiom String
"ﬧﬧa == a" ((Forall "A" Stroke -> SBool) -> KD Proof)
-> (Forall "A" Stroke -> SBool) -> KD Proof
forall a b. (a -> b) -> a -> b
$ \A -> ﬧﬧ a .== SStroke
a

-- | Second Sheffer axiom: @a ⏐ (b ⏐ ﬧb) == ﬧa@
sheffer2 :: KD Proof
sheffer2 :: KD Proof
sheffer2 = String
-> (Forall "A" Stroke -> Forall "B" Stroke -> SBool) -> KD Proof
forall a. Proposition a => String -> a -> KD Proof
axiom String
"a ⏐ (b ⏐ ﬧb) == ﬧa" ((Forall "A" Stroke -> Forall "B" Stroke -> SBool) -> KD Proof)
-> (Forall "A" Stroke -> Forall "B" Stroke -> SBool) -> KD Proof
forall a b. (a -> b) -> a -> b
$ \AB -> a ⏐ (b ⏐ ﬧ b) .== ﬧ a

-- | Third Sheffer axiom: @ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)@
sheffer3 :: KD Proof
sheffer3 :: KD Proof
sheffer3 = String
-> (Forall "A" Stroke
    -> Forall "B" Stroke -> Forall "C" Stroke -> SBool)
-> KD Proof
forall a. Proposition a => String -> a -> KD Proof
axiom String
"ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)" ((Forall "A" Stroke
  -> Forall "B" Stroke -> Forall "C" Stroke -> SBool)
 -> KD Proof)
-> (Forall "A" Stroke
    -> Forall "B" Stroke -> Forall "C" Stroke -> SBool)
-> KD Proof
forall a b. (a -> b) -> a -> b
$ \ABC -> ﬧ(a ⏐ (b ⏐ c)) .== (ﬧ b ⏐ a) ⏐ (ﬧ c SStroke
⏐ a)

-- * Sheffer's stroke defines a boolean algebra

-- | Prove that Sheffer stroke axioms imply it is a boolean algebra. We have:
--
-- >>> shefferBooleanAlgebra
-- Axiom: ﬧﬧa == a
-- Axiom: a ⏐ (b ⏐ ﬧb) == ﬧa
-- Axiom: ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)
-- Lemma: a | b = b | a
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Step  : 4                                                 Q.E.D.
--   Step  : 5                                                 Q.E.D.
--   Step  : 6                                                 Q.E.D.
--   Step  : 7                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: a | a′ = b | b′
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Step  : 4                                                 Q.E.D.
--   Step  : 5                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: a ⊔ b = b ⊔ a                                        Q.E.D.
-- Lemma: a ⊓ b = b ⊓ a                                        Q.E.D.
-- Lemma: a ⊔ ⲳ = a                                            Q.E.D.
-- Lemma: a ⊓ т = a                                            Q.E.D.
-- Lemma: a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c)                      Q.E.D.
-- Lemma: a ⊓ (b ⊔ c) = (a ⊓ b) ⊔ (a ⊓ c)                      Q.E.D.
-- Lemma: a ⊔ aᶜ = т                                           Q.E.D.
-- Lemma: a ⊓ aᶜ = ⲳ                                           Q.E.D.
-- Lemma: a ⊔ т = т
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Step  : 4                                                 Q.E.D.
--   Step  : 5                                                 Q.E.D.
--   Step  : 6                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: a ⊓ ⲳ = ⲳ
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Step  : 4                                                 Q.E.D.
--   Step  : 5                                                 Q.E.D.
--   Step  : 6                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: a ⊔ (a ⊓ b) = a
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Step  : 4                                                 Q.E.D.
--   Step  : 5                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: a ⊓ (a ⊔ b) = a
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Step  : 4                                                 Q.E.D.
--   Step  : 5                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: a ⊓ a = a
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: a ⊔ a' = т → a ⊓ a' = ⲳ → a' = aᶜ
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Step  : 4                                                 Q.E.D.
--   Step  : 5                                                 Q.E.D.
--   Asms  : 6                                                 Q.E.D.
--   Step  : 6                                                 Q.E.D.
--   Step  : 7                                                 Q.E.D.
--   Step  : 8                                                 Q.E.D.
--   Step  : 9                                                 Q.E.D.
--   Asms  : 10                                                Q.E.D.
--   Step  : 10                                                Q.E.D.
--   Step  : 11                                                Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: aᶜᶜ = a                                              Q.E.D.
-- Lemma: aᶜ = bᶜ → a = b                                      Q.E.D.
-- Lemma: a ⊔ bᶜ = т → a ⊓ bᶜ = ⲳ → a = b                      Q.E.D.
-- Lemma: a ⊔ (aᶜ ⊔ b) = т
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Step  : 4                                                 Q.E.D.
--   Step  : 5                                                 Q.E.D.
--   Step  : 6                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: a ⊓ (aᶜ ⊓ b) = ⲳ
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Step  : 4                                                 Q.E.D.
--   Step  : 5                                                 Q.E.D.
--   Step  : 6                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: (a ⊔ b)ᶜ = aᶜ ⊓ bᶜ                                   Q.E.D.
-- Lemma: (a ⨅ b)ᶜ = aᶜ ⨆ bᶜ                                   Q.E.D.
-- Lemma: (a ⊔ (b ⊔ c)) ⊔ aᶜ = т                               Q.E.D.
-- Lemma: b ⊓ (a ⊔ (b ⊔ c)) = b                                Q.E.D.
-- Lemma: b ⊔ (a ⊓ (b ⊓ c)) = b                                Q.E.D.
-- Lemma: (a ⊔ (b ⊔ c)) ⊔ bᶜ = т
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Step  : 4                                                 Q.E.D.
--   Step  : 5                                                 Q.E.D.
--   Step  : 6                                                 Q.E.D.
--   Step  : 7                                                 Q.E.D.
--   Step  : 8                                                 Q.E.D.
--   Step  : 9                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: (a ⊔ (b ⊔ c)) ⊔ cᶜ = т                               Q.E.D.
-- Lemma: (a ⊔ b ⊔ c)ᶜ ⊓ a = ⲳ
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Step  : 4                                                 Q.E.D.
--   Step  : 5                                                 Q.E.D.
--   Step  : 6                                                 Q.E.D.
--   Step  : 7                                                 Q.E.D.
--   Step  : 8                                                 Q.E.D.
--   Step  : 9                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: (a ⊔ b ⊔ c)ᶜ ⊓ b = ⲳ                                 Q.E.D.
-- Lemma: (a ⊔ b ⊔ c)ᶜ ⊓ c = ⲳ                                 Q.E.D.
-- Lemma: (a ⊔ (b ⊔ c)) ⊔ ((a ⊔ b) ⊔ c)ᶜ = т
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Step  : 4                                                 Q.E.D.
--   Step  : 5                                                 Q.E.D.
--   Step  : 6                                                 Q.E.D.
--   Step  : 7                                                 Q.E.D.
--   Step  : 8                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: (a ⊔ (b ⊔ c)) ⊓ ((a ⊔ b) ⊔ c)ᶜ = ⲳ
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Step  : 4                                                 Q.E.D.
--   Step  : 5                                                 Q.E.D.
--   Step  : 6                                                 Q.E.D.
--   Step  : 7                                                 Q.E.D.
--   Step  : 8                                                 Q.E.D.
--   Step  : 9                                                 Q.E.D.
--   Step  : 10                                                Q.E.D.
--   Step  : 11                                                Q.E.D.
--   Step  : 12                                                Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ c                            Q.E.D.
-- Lemma: a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ c
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: a ≤ b → b ≤ a → a = b
--   Asms  : 1                                                 Q.E.D.
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Asms  : 3                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: a ≤ a                                                Q.E.D.
-- Lemma: a ≤ b → b ≤ c → a ≤ c
--   Asms  : 1                                                 Q.E.D.
--   Step  : 1                                                 Q.E.D.
--   Asms  : 2                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Asms  : 4                                                 Q.E.D.
--   Step  : 4                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: a < b ↔ a ≤ b ∧ ¬b ≤ a                               Q.E.D.
-- Lemma: a ≤ a ⊔ b                                            Q.E.D.
-- Lemma: b ≤ a ⊔ b                                            Q.E.D.
-- Lemma: a ≤ c → b ≤ c → a ⊔ b ≤ c
--   Asms  : 1                                                 Q.E.D.
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: a ⊓ b ≤ a                                            Q.E.D.
-- Lemma: a ⊓ b ≤ b                                            Q.E.D.
-- Lemma: a ≤ b → a ≤ c → a ≤ b ⊓ c
--   Asms  : 1                                                 Q.E.D.
--   Step  : 1                                                 Q.E.D.
--   Asms  : 2                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z                        Q.E.D.
-- Lemma: x ⊓ xᶜ ≤ ⊥                                           Q.E.D.
-- Lemma: ⊤ ≤ x ⊔ xᶜ                                           Q.E.D.
-- Lemma: a ≤ ⊤
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Step  : 3                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: ⊥ ≤ a
--   Step  : 1                                                 Q.E.D.
--   Step  : 2                                                 Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: x \ y = x ⊓ yᶜ                                       Q.E.D.
-- Lemma: x ⇨ y = y ⊔ xᶜ                                       Q.E.D.
-- BooleanAlgebraProof {
--   le_refl         : [Proven] a ≤ a
--   le_trans        : [Proven] a ≤ b → b ≤ c → a ≤ c
--   lt_iff_le_not_le: [Proven] a < b ↔ a ≤ b ∧ ¬b ≤ a
--   le_antisymm     : [Proven] a ≤ b → b ≤ a → a = b
--   le_sup_left     : [Proven] a ≤ a ⊔ b
--   le_sup_right    : [Proven] b ≤ a ⊔ b
--   sup_le          : [Proven] a ≤ c → b ≤ c → a ⊔ b ≤ c
--   inf_le_left     : [Proven] a ⊓ b ≤ a
--   inf_le_right    : [Proven] a ⊓ b ≤ b
--   le_inf          : [Proven] a ≤ b → a ≤ c → a ≤ b ⊓ c
--   le_sup_inf      : [Proven] (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
--   inf_compl_le_bot: [Proven] x ⊓ xᶜ ≤ ⊥
--   top_le_sup_compl: [Proven] ⊤ ≤ x ⊔ xᶜ
--   le_top          : [Proven] a ≤ ⊤
--   bot_le          : [Proven] ⊥ ≤ a
--   sdiff_eq        : [Proven] x \ y = x ⊓ yᶜ
--   himp_eq         : [Proven] x ⇨ y = y ⊔ xᶜ
-- }
shefferBooleanAlgebra :: IO BooleanAlgebraProof
shefferBooleanAlgebra :: IO BooleanAlgebraProof
shefferBooleanAlgebra = SMTConfig -> KD BooleanAlgebraProof -> IO BooleanAlgebraProof
forall a. SMTConfig -> KD a -> IO a
runKDWith SMTConfig
z3{kdOptions = (kdOptions z3) {ribbonLength = 60}} (KD BooleanAlgebraProof -> IO BooleanAlgebraProof)
-> KD BooleanAlgebraProof -> IO BooleanAlgebraProof
forall a b. (a -> b) -> a -> b
$ do

  -- Get the axioms
  sh1 <- KD Proof
sheffer1
  sh2 <- sheffer2
  sh3 <- sheffer3

  commut <- calc "a | b = b | a" (\AB -> a ⏐ b .== b ⏐ a) $
                 \SStroke
a SStroke
b -> [] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a SStroke -> SStroke -> SStroke
⏐ SStroke
b                       SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
sh1
                            ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ(SStroke
a SStroke -> SStroke -> SStroke
⏐ SStroke
b)                   SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
sh1
                            ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ(SStroke
a SStroke -> SStroke -> SStroke
⏐ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ SStroke
b)
                            SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ(SStroke
a SStroke -> SStroke -> SStroke
⏐ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b SStroke -> SStroke -> SStroke
⏐ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b))         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
sh3
                            ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ ((SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ SStroke
b SStroke -> SStroke -> SStroke
⏐ SStroke
a) SStroke -> SStroke -> SStroke
⏐ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ SStroke
b SStroke -> SStroke -> SStroke
⏐ SStroke
a))
                            SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ(SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ SStroke
b SStroke -> SStroke -> SStroke
⏐ SStroke
a)                SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
sh1
                            ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ SStroke
b SStroke -> SStroke -> SStroke
⏐ SStroke
a                    SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
sh1
                            ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
b SStroke -> SStroke -> SStroke
⏐ SStroke
a
                            SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  all_bot <- calc "a | a′ = b | b′" (\AB -> a ⏐ ﬧ a .== b ⏐ ﬧ b) $
                  \SStroke
a SStroke
b -> [] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a SStroke -> SStroke -> SStroke
⏐ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a                  SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
sh1
                             ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ(SStroke
a SStroke -> SStroke -> SStroke
⏐ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a)              SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
sh2
                             ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
⏐ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a) SStroke -> SStroke -> SStroke
⏐ (SStroke
b SStroke -> SStroke -> SStroke
⏐ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b)) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut
                             ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
b SStroke -> SStroke -> SStroke
⏐ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b) SStroke -> SStroke -> SStroke
⏐ (SStroke
a SStroke -> SStroke -> SStroke
⏐ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a)) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
sh2
                             ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ (SStroke
b SStroke -> SStroke -> SStroke
⏐ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b)             SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
sh1
                             ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
b SStroke -> SStroke -> SStroke
⏐ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b
                             SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  commut1  <- lemma "a ⊔ b = b ⊔ a" (\AB -> a ⨆ b .== b ⨆ a) [commut]
  commut2  <- lemma "a ⊓ b = b ⊓ a" (\AB -> a ⨅ b .== b ⨅ a) [commut]

  ident1   <- lemma "a ⊔ ⲳ = a" (\A  -> a ⨆ ⲳ .== a) [sh1, sh2]
  ident2   <- lemma "a ⊓ т = a" (\A  -> a ⨅ т .== a) [sh1, sh2]

  distrib1 <- lemma "a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c)" (\ABC -> a ⨆ (b ⨅ c) .== (a ⨆ b) ⨅ (a ⨆ c)) [sh1, sh3, commut]
  distrib2 <- lemma "a ⊓ (b ⊔ c) = (a ⊓ b) ⊔ (a ⊓ c)" (\ABC -> a ⨅ (b ⨆ c) .== (a ⨅ b) ⨆ (a ⨅ c)) [sh1, sh3, commut]

  compl1 <- lemma "a ⊔ aᶜ = т" (\A -> a ⨆ ﬧ a .== т) [sh1, sh2, sh3, all_bot]
  compl2 <- lemma "a ⊓ aᶜ = ⲳ" (\A -> a ⨅ ﬧ a .== ⲳ) [sh1, commut, all_bot]

  bound1 <- calc "a ⊔ т = т" (\A -> a ⨆ т .== т) $
                 \(SStroke
a :: SStroke) -> [] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
forall α. BooleanAlgebra α => α
т               SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident2
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
forall α. BooleanAlgebra α => α
т) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
т         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut2
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
forall α. BooleanAlgebra α => α
т SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
forall α. BooleanAlgebra α => α
т)         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
compl1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
forall α. BooleanAlgebra α => α
т) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
distrib1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
т)       SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident2
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a             SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
compl1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
forall α. BooleanAlgebra α => α
т :: SStroke)
                                       SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  bound2 <- calc "a ⊓ ⲳ = ⲳ" (\A -> a ⨅ ⲳ .== ⲳ) $
                 \(SStroke
a :: SStroke) -> [] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
ⲳ               SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
ⲳ) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
forall α. BooleanAlgebra α => α
ⲳ         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
forall α. BooleanAlgebra α => α
ⲳ SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
ⲳ)         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
compl2
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
ⲳ) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
distrib2
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
forall α. BooleanAlgebra α => α
ⲳ)       SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a             SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
compl2
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
forall α. BooleanAlgebra α => α
ⲳ :: SStroke)
                                       SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  absorb1 <- calc "a ⊔ (a ⊓ b) = a" (\AB -> a ⨆ (a ⨅ b) .== a) $
                  \(SStroke
a :: SStroke) SStroke
b -> [] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
b)       SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident2
                                          ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
т) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
b) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
distrib2
                                          ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
forall α. BooleanAlgebra α => α
т SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b)       SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut1
                                          ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
forall α. BooleanAlgebra α => α
т)       SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
bound1
                                          ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
т             SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident2
                                          ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a
                                          SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  absorb2 <- calc "a ⊓ (a ⊔ b) = a" (\AB -> a ⨅ (a ⨆ b) .== a) $
                  \(SStroke
a :: SStroke) SStroke
b -> [] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b)       SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident1
                                          ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
forall α. BooleanAlgebra α => α
ⲳ) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
distrib1
                                          ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
forall α. BooleanAlgebra α => α
ⲳ SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
b)       SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut2
                                          ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
ⲳ)       SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
bound2
                                          ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
forall α. BooleanAlgebra α => α
ⲳ             SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident1
                                          ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a
                                          SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  idemp2 <- calc "a ⊓ a = a" (\A -> a ⨅ a .== a) $
                 \(SStroke
a :: SStroke) -> [] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a       SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
forall α. BooleanAlgebra α => α
ⲳ) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
absorb2
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a
                                       SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  inv <- calc "a ⊔ a' = т → a ⊓ a' = ⲳ → a' = aᶜ"
              (\AAp  -> a ⨆ a' .== т .=> a ⨅ a' .== ⲳ .=> a' .== ﬧ a) $
              \(SStroke
a :: SStroke) SStroke
a' -> [SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
a' SStroke -> SStroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SStroke
forall α. BooleanAlgebra α => α
т, SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a' SStroke -> SStroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SStroke
forall α. BooleanAlgebra α => α
ⲳ] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a'                     SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident2
                                                                 ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a' SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
т                 SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
compl1
                                                                 ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a' SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a)         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
distrib2
                                                                 ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a' SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
a' SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a)  SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut2
                                                                 ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a' SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a')  SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut2
                                                                 ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a') SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a')  SStroke -> SBool -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a' SStroke -> SStroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SStroke
forall α. BooleanAlgebra α => α
ⲳ
                                                                 ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
forall α. BooleanAlgebra α => α
ⲳ SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a')         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
compl2
                                                                 ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a') SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut2
                                                                 ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a') SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
distrib2
                                                                 ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
a')         SStroke -> SBool -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
a' SStroke -> SStroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SStroke
forall α. BooleanAlgebra α => α
т
                                                                 ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
т                SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident2
                                                                 ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a
                                                                 SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  dne      <- lemma "aᶜᶜ = a"         (\A -> ﬧﬧ a .== SStroke
a)               [inv, compl1, compl2, commut1, commut2]
  inv_elim <- lemma "aᶜ = bᶜ → a = b" (\AB -> ﬧ a .== ﬧ b .=> a .== b) [dne]

  cancel <- lemma "a ⊔ bᶜ = т → a ⊓ bᶜ = ⲳ → a = b" (\AB -> a ⨆ ﬧ b .== т .=> a ⨅ ﬧ b .== ⲳ .=> a .== b) [inv, inv_elim]

  a1 <- calc "a ⊔ (aᶜ ⊔ b) = т" (\AB  -> a ⨆ (ﬧ a ⨆ b) .== т) $
             \(SStroke
a :: SStroke) SStroke
b -> [] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b)               SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident2
                                     ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
т         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut2
                                     ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
forall α. BooleanAlgebra α => α
т SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b))         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
compl1
                                     ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b)) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
distrib1
                                     ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b))       SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
absorb2
                                     ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a                     SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
compl1
                                     ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
forall α. BooleanAlgebra α => α
т :: SStroke)
                                     SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  a2 <- calc "a ⊓ (aᶜ ⊓ b) = ⲳ" (\AB  -> a ⨅ (ﬧ a ⨅ b) .== ⲳ) $
             \(SStroke
a :: SStroke) SStroke
b -> [] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
b)               SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident1
                                     ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
b)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
forall α. BooleanAlgebra α => α
ⲳ         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut1
                                     ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
forall α. BooleanAlgebra α => α
ⲳ SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
b))         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
compl2
                                     ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
b)) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
distrib2
                                     ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
b))       SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
absorb1
                                     ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a                     SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
compl2
                                     ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
forall α. BooleanAlgebra α => α
ⲳ :: SStroke)
                                     SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  dm1 <- lemma "(a ⊔ b)ᶜ = aᶜ ⊓ bᶜ" (\AB -> ﬧ(a ⨆ b) .== ﬧ a ⨅ ﬧ b)
               [a1, a2, dne, commut1, commut2, ident1, ident2, distrib1, distrib2]

  dm2 <- lemma "(a ⨅ b)ᶜ = aᶜ ⨆ bᶜ" (\AB -> ﬧ(a ⨅ b) .== ﬧ a ⨆ ﬧ b)
               [a1, a2, dne, commut1, commut2, ident1, ident2, distrib1, distrib2]


  d1 <- lemma "(a ⊔ (b ⊔ c)) ⊔ aᶜ = т" (\ABC -> (a ⨆ (b ⨆ c)) ⨆ ﬧ a .== т)
              [a1, a2, commut1, ident1, ident2, distrib1, compl1, compl2, dm1, dm2, idemp2]

  e1 <- lemma "b ⊓ (a ⊔ (b ⊔ c)) = b" (\ABC -> b ⨅ (a ⨆ (b ⨆ c)) .== b) [distrib2, absorb1, absorb2, commut1]

  e2 <- lemma "b ⊔ (a ⊓ (b ⊓ c)) = b" (\ABC -> b ⨆ (a ⨅ (b ⨅ c)) .== b) [distrib1, absorb1, absorb2, commut2]

  f1 <- calc "(a ⊔ (b ⊔ c)) ⊔ bᶜ = т" (\ABC -> (a ⨆ (b ⨆ c)) ⨆ ﬧ b .== т) $
             \(SStroke
a :: SStroke) SStroke
b SStroke
c -> [] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b               SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c))               SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident2
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c))) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
т         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut2
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
forall α. BooleanAlgebra α => α
т SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)))         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
compl1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c))) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c))) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
distrib1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)))         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
e1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b                           SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b                           SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
compl1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
forall α. BooleanAlgebra α => α
т :: SStroke)
                                       SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  g1 <- lemma "(a ⊔ (b ⊔ c)) ⊔ cᶜ = т" (\ABC -> (a ⨆ (b ⨆ c)) ⨆ ﬧ c .== т) [commut1, f1]

  h1 <- calc "(a ⊔ b ⊔ c)ᶜ ⊓ a = ⲳ" (\ABC -> ﬧ(a ⨆ b ⨆ c) ⨅ a .== ⲳ) $
             \(SStroke
a :: SStroke) SStroke
b SStroke
c -> [] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ(SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a                    SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut2
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)                   SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
dm1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
c)               SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅  (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
c)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
forall α. BooleanAlgebra α => α
ⲳ        SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut1
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
forall α. BooleanAlgebra α => α
ⲳ SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
c))         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
compl2
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
c)) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
distrib2
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
c))       SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut2
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
c SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b)))     SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
e2
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a                             SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
compl2
                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
forall α. BooleanAlgebra α => α
ⲳ :: SStroke)
                                       SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  i1 <- lemma "(a ⊔ b ⊔ c)ᶜ ⊓ b = ⲳ" (\ABC -> ﬧ(a ⨆ b ⨆ c) ⨅ b .== ⲳ) [commut1, h1]
  j1 <- lemma "(a ⊔ b ⊔ c)ᶜ ⊓ c = ⲳ" (\ABC -> ﬧ(a ⨆ b ⨆ c) ⨅ c .== ⲳ) [a2, dne, commut2]

  assoc1 <- do
    c1 <- calc "(a ⊔ (b ⊔ c)) ⊔ ((a ⊔ b) ⊔ c)ᶜ = т"
               (\ABC -> (a ⨆ (b ⨆ c)) ⨆ ﬧ((a ⨆ b) ⨆ c) .== тSStroke
) $
               \(SStroke
a :: SStroke) SStroke
b SStroke
c -> [] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)                        SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
dm1
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
c)                     SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
distrib1
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
c) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
g1
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
т                     SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident2
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b)                           SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
distrib1
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
a) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b)         SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
d1
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
forall α. BooleanAlgebra α => α
т SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ SStroke
b)                             SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
f1
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
forall α. BooleanAlgebra α => α
т SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
forall α. BooleanAlgebra α => α
т :: SStroke)                                    SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
idemp2
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
forall α. BooleanAlgebra α => α
т :: SStroke)
                                         SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

    c2 <- calc "(a ⊔ (b ⊔ c)) ⊓ ((a ⊔ b) ⊔ c)ᶜ = ⲳ"
               (\ABC -> (a ⨆ (b ⨆ c)) ⨅ ﬧ((a ⨆ b) ⨆ c) .== ⲳSStroke
) $
               \(SStroke
a :: SStroke) SStroke
b SStroke
c -> [] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)                    SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut2
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c))                    SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
distrib2
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut2
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ ((SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut2
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ ((SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
h1
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
forall α. BooleanAlgebra α => α
ⲳ SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ ((SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c))                    SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut1
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ((SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
forall α. BooleanAlgebra α => α
ⲳ                    SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident1
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)                          SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut2
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c)                          SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
distrib2
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
c)       SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
j1
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
c) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
forall α. BooleanAlgebra α => α
ⲳ                          SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
i1
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
forall α. BooleanAlgebra α => α
ⲳ SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
forall α. BooleanAlgebra α => α
ⲳ :: SStroke)                                SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident1
                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
forall α. BooleanAlgebra α => α
ⲳ :: SStroke)
                                         SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

    lemma "a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ c" (\ABC -> a ⨆ (b ⨆ c) .== (a ⨆ b) ⨆ c) [c1, c2, cancel]

  assoc2 <- calc "a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ c" (\ABC -> a ⨅ (b ⨅ c) .== (a ⨅ b) ⨅ c) $
                 \(SStroke
a :: SStroke) SStroke
b SStroke
c -> [] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
c)     SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
dne
                                           ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ(SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
c)) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
assoc1
                                           ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
c) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
dne
                                           ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡   ((SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
c)
                                           SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  le_antisymm <- calc "a ≤ b → b ≤ a → a = b" (\AB -> a ≤ b .=> b ≤ a .=> a .== b) $
                      \(SStroke
a :: SStroke) SStroke
b -> [SStroke
a SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
b, SStroke
b SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
a] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a     SStroke -> SBool -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ SStroke
a SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
b
                                                          ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut2
                                                          ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
b SStroke -> SBool -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ SStroke
b SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
a
                                                          ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
b
                                                          SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  le_refl <- lemma "a ≤ a" (\A -> a ≤ a) [idemp2]

  le_trans <- calc "a ≤ b → b ≤ c → a ≤ c" (\ABC -> a ≤ b .=> b ≤ c .=> a ≤ c) $
                   \(SStroke
a :: SStroke) SStroke
b SStroke
c -> [SStroke
a SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
b, SStroke
b SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
c] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a            SStroke -> SBool -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ SStroke
a SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
b
                                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a        SStroke -> SBool -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ SStroke
b SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
c
                                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
c SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
b) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a  SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
assoc2
                                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
c SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a)  SStroke -> SBool -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ SStroke
a SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
b
                                                         ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
c SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a)
                                                         SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  lt_iff_le_not_le <- lemma "a < b ↔ a ≤ b ∧ ¬b ≤ a" (\AB -> (a < b) .<=> a ≤ b .&& sNot (b ≤ a)) [sh3]

  le_sup_left  <- lemma "a ≤ a ⊔ b" (\AB -> a ≤ a ⨆ b) [commut1, commut2, absorb2]
  le_sup_right <- lemma "b ≤ a ⊔ b" (\AB -> a ≤ a ⨆ b) [commut1, commut2, absorb2]

  sup_le <- calc "a ≤ c → b ≤ c → a ⊔ b ≤ c"
                 (\ABC -> a ≤ c .=> b ≤ c .=> a ⨆ b ≤ c) $
                 \(SStroke
a :: SStroke) SStroke
b SStroke
c -> [SStroke
a SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
c, SStroke
b SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
c] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b             SStroke -> [SBool] -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ [SStroke
a SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
c, SStroke
b SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
c]
                                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
c SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a) SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SStroke
c SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
b) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
distrib2
                                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
c SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SStroke
b)
                                                       SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  inf_le_left  <- lemma "a ⊓ b ≤ a" (\AB -> a ⨅ b ≤ a) [assoc2, idemp2]
  inf_le_right <- lemma "a ⊓ b ≤ b" (\AB -> a ⨅ b ≤ b) [commut2, inf_le_left]

  le_inf <- calc "a ≤ b → a ≤ c → a ≤ b ⊓ c"
                 (\ABC -> a ≤ b .=> a ≤ c .=> a ≤ b ⨅ c) $
                 \(SStroke
a :: SStroke) SStroke
b SStroke
c -> [SStroke
a SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
b, SStroke
a SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
c] [SBool] -> [ProofStep SStroke] -> (SBool, [ProofStep SStroke])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a           SStroke -> SBool -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ SStroke
a SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
b
                                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a       SStroke -> SBool -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ SStroke
a SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
c
                                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SStroke
c SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a) SStroke -> Proof -> ProofStep SStroke
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
assoc2
                                                       ProofStep SStroke
-> ChainsTo (ProofStep SStroke) -> ChainsTo (ProofStep SStroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
b SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
c SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a)
                                                       SStroke -> ChainsTo SStroke -> ChainsTo SStroke
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SStroke]
ChainsTo SStroke
forall a. [ProofStep a]
qed

  le_sup_inf <- lemma "(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z"
                      (\XYZ -> (x ⨆ y) ⨅ (x ⨆ z) ≤ x ⨆ y ⨅ z)
                      [distrib1, le_refl]

  inf_compl_le_bot <- lemma "x ⊓ xᶜ ≤ ⊥" (\X -> x ⨅ ﬧ x ≤ ⲳ) [compl2, le_refl]
  top_le_sup_compl <- lemma "⊤ ≤ x ⊔ xᶜ" (\X -> т ≤ x ⨆ ﬧ x) [compl1, le_refl]

  le_top <- calc "a ≤ ⊤" (\A -> a ≤ т) $
                 \(SStroke
a :: SStroke)-> [] [SBool] -> [ProofStep SBool] -> (SBool, [ProofStep SBool])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
a SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
forall α. BooleanAlgebra α => α
т
                                      SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SStroke
forall α. BooleanAlgebra α => α
т SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
a SBool -> Proof -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
commut2
                                      ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
т SBool -> Proof -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
ident2
                                      ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
a SStroke -> SStroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SStroke
a
                                      SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SBool]
ChainsTo SBool
forall a. [ProofStep a]
qed

  bot_le <- calc "⊥ ≤ a" (\A -> ⲳ ≤ a) $
                 \(SStroke
a :: SStroke) -> [] [SBool] -> [ProofStep SBool] -> (SBool, [ProofStep SBool])
forall a. [SBool] -> [ProofStep a] -> (SBool, [ProofStep a])
⊢ SStroke
forall α. BooleanAlgebra α => α
ⲳ SStroke -> SStroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SStroke
a
                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SStroke
forall α. BooleanAlgebra α => α
ⲳ SStroke -> SStroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SStroke
a SStroke -> SStroke -> SStroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SStroke
forall α. BooleanAlgebra α => α
ⲳ            SBool -> Proof -> ProofStep SBool
forall a b. ProofHint a b => a -> b -> ProofStep a
⁇ Proof
bound2
                                       ProofStep SBool
-> ChainsTo (ProofStep SBool) -> ChainsTo (ProofStep SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SStroke
forall α. BooleanAlgebra α => α
ⲳ SStroke -> SStroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SStroke
forall α. BooleanAlgebra α => α
ⲳ :: SStroke))
                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ [ProofStep SBool]
ChainsTo SBool
forall a. [ProofStep a]
qed

  sdiff_eq <- lemma "x \\ y = x ⊓ yᶜ" (\XY -> x \\ y .== x ⨅ ﬧ y) []
  himp_eq  <- lemma "x ⇨ y = y ⊔ xᶜ"  (\XY -> x ⇨ y .== y ⨆ ﬧ x)  []

  pure BooleanAlgebraProof {
            le_refl          {- ∀ (a : α), a ≤ a                             -} = le_refl
          , le_trans         {- ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c         -} = le_trans
          , lt_iff_le_not_le {- (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a)        -} = lt_iff_le_not_le
          , le_antisymm      {- ∀ (a b : α), a ≤ b → b ≤ a → a = b           -} = le_antisymm
          , le_sup_left      {- ∀ (a b : α), a ≤ a ⊔ b                       -} = le_sup_left
          , le_sup_right     {- ∀ (a b : α), b ≤ a ⊔ b                       -} = le_sup_right
          , sup_le           {- ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c     -} = sup_le
          , inf_le_left      {- ∀ (a b : α), a ⊓ b ≤ a                       -} = inf_le_left
          , inf_le_right     {- ∀ (a b : α), a ⊓ b ≤ b                       -} = inf_le_right
          , le_inf           {- ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c     -} = le_inf
          , le_sup_inf       {- ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z -} = le_sup_inf
          , inf_compl_le_bot {- ∀ (x : α), x ⊓ xᶜ ≤ ⊥                        -} = inf_compl_le_bot
          , top_le_sup_compl {- ∀ (x : α), ⊤ ≤ x ⊔ xᶜ                        -} = top_le_sup_compl
          , le_top           {- ∀ (a : α), a ≤ ⊤                             -} = le_top
          , bot_le           {- ∀ (a : α), ⊥ ≤ a                             -} = bot_le
          , sdiff_eq         {- (∀ (x y : α), x \ y = x ⊓ yᶜ)                -} = sdiff_eq
          , himp_eq          {- (∀ (x y : α), x ⇨ y = y ⊔ xᶜ)                -} = himp_eq
       }