-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.TP.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 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.TP.ShefferStroke where

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

import Data.SBV
import Data.SBV.TP

-- * 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 (Forall "a" Stroke -> SBool)
le_refl          {- ∀ (a : α), a ≤ a                             -} :: Proof (Forall "a" Stroke -> SBool)
  , BooleanAlgebraProof
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
le_trans         {- ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c         -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
  , BooleanAlgebraProof
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
lt_iff_le_not_le {- (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a)        -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
  , BooleanAlgebraProof
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
le_antisymm      {- ∀ (a b : α), a ≤ b → b ≤ a → a = b           -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
  , BooleanAlgebraProof
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
le_sup_left      {- ∀ (a b : α), a ≤ a ⊔ b                       -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
  , BooleanAlgebraProof
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
le_sup_right     {- ∀ (a b : α), b ≤ a ⊔ b                       -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
  , BooleanAlgebraProof
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
sup_le           {- ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c     -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
  , BooleanAlgebraProof
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
inf_le_left      {- ∀ (a b : α), a ⊓ b ≤ a                       -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
  , BooleanAlgebraProof
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
inf_le_right     {- ∀ (a b : α), a ⊓ b ≤ b                       -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
  , BooleanAlgebraProof
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
le_inf           {- ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c     -} :: Proof (Forall "a" Stroke -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
  , BooleanAlgebraProof
-> Proof
     (Forall "x" Stroke
      -> Forall "y" Stroke -> Forall "z" Stroke -> SBool)
le_sup_inf       {- ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z -} :: Proof (Forall "x" Stroke -> Forall "y" Stroke -> Forall "z" Stroke -> SBool)
  , BooleanAlgebraProof -> Proof (Forall "x" Stroke -> SBool)
inf_compl_le_bot {- ∀ (x : α), x ⊓ xᶜ ≤ ⊥                        -} :: Proof (Forall "x" Stroke -> SBool)
  , BooleanAlgebraProof -> Proof (Forall "x" Stroke -> SBool)
top_le_sup_compl {- ∀ (x : α), ⊤ ≤ x ⊔ xᶜ                        -} :: Proof (Forall "x" Stroke -> SBool)
  , BooleanAlgebraProof -> Proof (Forall "a" Stroke -> SBool)
le_top           {- ∀ (a : α), a ≤ ⊤                             -} :: Proof (Forall "a" Stroke -> SBool)
  , BooleanAlgebraProof -> Proof (Forall "a" Stroke -> SBool)
bot_le           {- ∀ (a : α), ⊥ ≤ a                             -} :: Proof (Forall "a" Stroke -> SBool)
  , BooleanAlgebraProof
-> Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool)
sdiff_eq         {- (∀ (x y : α), x \ y = x ⊓ yᶜ)                -} :: Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool)
  , BooleanAlgebraProof
-> Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool)
himp_eq          {- (∀ (x y : α), x ⇨ y = y ⊔ xᶜ)                -} :: Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool)
  }

-- | 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 (Forall "a" Stroke -> SBool) -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof (Forall "a" Stroke -> SBool)
le_refl          BooleanAlgebraProof
p)
                            , String
"  le_trans        : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> String
forall a. Show a => a -> String
show (BooleanAlgebraProof
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
le_trans         BooleanAlgebraProof
p)
                            , String
"  lt_iff_le_not_le: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
lt_iff_le_not_le BooleanAlgebraProof
p)
                            , String
"  le_antisymm     : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
le_antisymm      BooleanAlgebraProof
p)
                            , String
"  le_sup_left     : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
le_sup_left      BooleanAlgebraProof
p)
                            , String
"  le_sup_right    : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
le_sup_right     BooleanAlgebraProof
p)
                            , String
"  sup_le          : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> String
forall a. Show a => a -> String
show (BooleanAlgebraProof
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
sup_le           BooleanAlgebraProof
p)
                            , String
"  inf_le_left     : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
inf_le_left      BooleanAlgebraProof
p)
                            , String
"  inf_le_right    : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
inf_le_right     BooleanAlgebraProof
p)
                            , String
"  le_inf          : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> String
forall a. Show a => a -> String
show (BooleanAlgebraProof
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
le_inf           BooleanAlgebraProof
p)
                            , String
"  le_sup_inf      : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof
  (Forall "x" Stroke
   -> Forall "y" Stroke -> Forall "z" Stroke -> SBool)
-> String
forall a. Show a => a -> String
show (BooleanAlgebraProof
-> Proof
     (Forall "x" Stroke
      -> Forall "y" Stroke -> Forall "z" Stroke -> SBool)
le_sup_inf       BooleanAlgebraProof
p)
                            , String
"  inf_compl_le_bot: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof (Forall "x" Stroke -> SBool) -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof (Forall "x" Stroke -> SBool)
inf_compl_le_bot BooleanAlgebraProof
p)
                            , String
"  top_le_sup_compl: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof (Forall "x" Stroke -> SBool) -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof (Forall "x" Stroke -> SBool)
top_le_sup_compl BooleanAlgebraProof
p)
                            , String
"  le_top          : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof (Forall "a" Stroke -> SBool) -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof (Forall "a" Stroke -> SBool)
le_top           BooleanAlgebraProof
p)
                            , String
"  bot_le          : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof (Forall "a" Stroke -> SBool) -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof -> Proof (Forall "a" Stroke -> SBool)
bot_le           BooleanAlgebraProof
p)
                            , String
"  sdiff_eq        : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool) -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof
-> Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool)
sdiff_eq         BooleanAlgebraProof
p)
                            , String
"  himp_eq         : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool) -> String
forall a. Show a => a -> String
show (BooleanAlgebraProof
-> Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool)
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
⏐ :: SBV Stroke -> SBV Stroke -> SBV Stroke
(⏐) = String -> SBV Stroke -> SBV Stroke -> SBV Stroke
forall a. SMTDefinable a => String -> a
uninterpret String
"⏐"
infixl 7 ⏐

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

-- | First Sheffer axiom: @ﬧﬧa == a@
sheffer1 :: TP (Proof (Forall "a" Stroke -> SBool))
sheffer1 :: TP (Proof (Forall "a" Stroke -> SBool))
sheffer1 = String
-> (Forall "a" Stroke -> SBool)
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
"ﬧﬧa == a" ((Forall "a" Stroke -> SBool)
 -> TP (Proof (Forall "a" Stroke -> SBool)))
-> (Forall "a" Stroke -> SBool)
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$ \(Forall SBV Stroke
a) -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
a

-- | Second Sheffer axiom: @a ⏐ (b ⏐ ﬧb) == ﬧa@
sheffer2 :: TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
sheffer2 :: TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
sheffer2 = String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
"a ⏐ (b ⏐ ﬧb) == ﬧa" ((Forall "a" Stroke -> Forall "b" Stroke -> SBool)
 -> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)))
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$ \(Forall SBV Stroke
a) (Forall SBV Stroke
b) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a

-- | Third Sheffer axiom: @ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)@
sheffer3 :: TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
sheffer3 :: TP
  (Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
sheffer3 = String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
"ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a)" ((Forall "a" Stroke
  -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
 -> TP
      (Proof
         (Forall "a" Stroke
          -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)))
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$ \(Forall SBV Stroke
a) (Forall SBV Stroke
b) (Forall SBV Stroke
c) -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ(SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
c SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke
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 (ﬧﬧa == a)                                        Q.E.D.
--   Step: 2 (ﬧﬧa == a)                                        Q.E.D.
--   Step: 3                                                   Q.E.D.
--   Step: 4 (ﬧ(a ⏐ (b ⏐ c)) == (ﬧb ⏐ a) ⏐ (ﬧc ⏐ a))           Q.E.D.
--   Step: 5                                                   Q.E.D.
--   Step: 6 (ﬧﬧa == a)                                        Q.E.D.
--   Step: 7 (ﬧﬧa == a)                                        Q.E.D.
--   Result:                                                   Q.E.D.
-- Lemma: a | a′ = b | b′
--   Step: 1 (ﬧﬧa == a)                                        Q.E.D.
--   Step: 2 (a ⏐ (b ⏐ ﬧb) == ﬧa)                              Q.E.D.
--   Step: 3                                                   Q.E.D.
--   Step: 4 (a ⏐ (b ⏐ ﬧb) == ﬧa)                              Q.E.D.
--   Step: 5 (ﬧﬧa == a)                                        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.
--   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.
--   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
--   Step: 1                                                   Q.E.D.
--   Step: 2                                                   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
--   Step: 1                                                   Q.E.D.
--   Step: 2                                                   Q.E.D.
--   Step: 3                                                   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
--   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
--   Step: 1                                                   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 :: Ɐa ∷ Stroke → Bool
--   le_trans        : [Proven] a ≤ b → b ≤ c → a ≤ c :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Ɐc ∷ Stroke → Bool
--   lt_iff_le_not_le: [Proven] a < b ↔ a ≤ b ∧ ¬b ≤ a :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
--   le_antisymm     : [Proven] a ≤ b → b ≤ a → a = b :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
--   le_sup_left     : [Proven] a ≤ a ⊔ b :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
--   le_sup_right    : [Proven] b ≤ a ⊔ b :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
--   sup_le          : [Proven] a ≤ c → b ≤ c → a ⊔ b ≤ c :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Ɐc ∷ Stroke → Bool
--   inf_le_left     : [Proven] a ⊓ b ≤ a :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
--   inf_le_right    : [Proven] a ⊓ b ≤ b :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Bool
--   le_inf          : [Proven] a ≤ b → a ≤ c → a ≤ b ⊓ c :: Ɐa ∷ Stroke → Ɐb ∷ Stroke → Ɐc ∷ Stroke → Bool
--   le_sup_inf      : [Proven] (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z :: Ɐx ∷ Stroke → Ɐy ∷ Stroke → Ɐz ∷ Stroke → Bool
--   inf_compl_le_bot: [Proven] x ⊓ xᶜ ≤ ⊥ :: Ɐx ∷ Stroke → Bool
--   top_le_sup_compl: [Proven] ⊤ ≤ x ⊔ xᶜ :: Ɐx ∷ Stroke → Bool
--   le_top          : [Proven] a ≤ ⊤ :: Ɐa ∷ Stroke → Bool
--   bot_le          : [Proven] ⊥ ≤ a :: Ɐa ∷ Stroke → Bool
--   sdiff_eq        : [Proven] x \ y = x ⊓ yᶜ :: Ɐx ∷ Stroke → Ɐy ∷ Stroke → Bool
--   himp_eq         : [Proven] x ⇨ y = y ⊔ xᶜ :: Ɐx ∷ Stroke → Ɐy ∷ Stroke → Bool
-- }
shefferBooleanAlgebra :: IO BooleanAlgebraProof
shefferBooleanAlgebra :: IO BooleanAlgebraProof
shefferBooleanAlgebra = SMTConfig -> TP BooleanAlgebraProof -> IO BooleanAlgebraProof
forall a. SMTConfig -> TP a -> IO a
runTPWith (Int -> SMTConfig -> SMTConfig
tpRibbon Int
60 SMTConfig
z3) (TP BooleanAlgebraProof -> IO BooleanAlgebraProof)
-> TP BooleanAlgebraProof -> IO BooleanAlgebraProof
forall a b. (a -> b) -> a -> b
$ do

  -- shorthand
  let p :: Proof a -> ProofObj
p = Proof a -> ProofObj
forall a. Proof a -> ProofObj
proofOf

  -- Get the axioms
  Proof (Forall "a" Stroke -> SBool)
sh1 <- TP (Proof (Forall "a" Stroke -> SBool))
sheffer1
  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
sh2 <- TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
sheffer2
  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
sh3 <- TP
  (Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
sheffer3

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall t.
(Proposition (Forall "a" Stroke -> Forall "b" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> Forall "b" Stroke -> SBool) t
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a | b = b | a" (\(Forall @"a" SBV Stroke
a) (Forall @"b" SBV Stroke
b) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke
a) (StepArgs (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
 -> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
                 \SBV Stroke
a SBV Stroke
b -> [] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke
b                       SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
sh1
                            TPProofRaw (SBV Stroke)
-> ChainsTo (TPProofRaw (SBV Stroke))
-> ChainsTo (TPProofRaw (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ(SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke
b)                   SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
sh1
                            TPProofRaw (SBV Stroke)
-> ChainsTo (TPProofRaw (SBV Stroke))
-> ChainsTo (TPProofRaw (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ(SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ SBV Stroke
b)
                            SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ(SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b))         SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
sh3
                            TPProofRaw (SBV Stroke)
-> ChainsTo (TPProofRaw (SBV Stroke))
-> ChainsTo (TPProofRaw (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ ((SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke
a))
                            SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ(SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke
a)                SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
sh1
                            TPProofRaw (SBV Stroke)
-> ChainsTo (TPProofRaw (SBV Stroke))
-> ChainsTo (TPProofRaw (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke
a                    SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
sh1
                            TPProofRaw (SBV Stroke)
-> ChainsTo (TPProofRaw (SBV Stroke))
-> ChainsTo (TPProofRaw (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke
a
                            SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
all_bot <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall t.
(Proposition (Forall "a" Stroke -> Forall "b" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> Forall "b" Stroke -> SBool) t
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a | a′ = b | b′" (\(Forall @"a" SBV Stroke
a) (Forall @"b" SBV Stroke
b) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b) (StepArgs (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
 -> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
                  \SBV Stroke
a SBV Stroke
b -> [] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a                  SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
sh1
                             TPProofRaw (SBV Stroke)
-> ChainsTo (TPProofRaw (SBV Stroke))
-> ChainsTo (TPProofRaw (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ(SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a)              SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
sh2
                             TPProofRaw (SBV Stroke)
-> ChainsTo (TPProofRaw (SBV Stroke))
-> ChainsTo (TPProofRaw (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b)) SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut
                             TPProofRaw (SBV Stroke)
-> ChainsTo (TPProofRaw (SBV Stroke))
-> ChainsTo (TPProofRaw (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a)) SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
sh2
                             TPProofRaw (SBV Stroke)
-> ChainsTo (TPProofRaw (SBV Stroke))
-> ChainsTo (TPProofRaw (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b)             SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
sh1
                             TPProofRaw (SBV Stroke)
-> ChainsTo (TPProofRaw (SBV Stroke))
-> ChainsTo (TPProofRaw (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
⏐ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b
                             SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1  <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"a ⊔ b = b ⊔ a" (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
a) [Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut]
  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2  <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"a ⊓ b = b ⊓ a" (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a) [Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut]

  Proof (Forall "a" Stroke -> SBool)
ident1   <- String
-> (Forall "a" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"a ⊔ ⲳ = a" (\(Forall @"a" (SBV Stroke
a :: SStroke)) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
a) [Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
sh1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
sh2]
  Proof (Forall "a" Stroke -> SBool)
ident2   <- String
-> (Forall "a" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"a ⊓ т = a" (\(Forall @"a" (SBV Stroke
a :: SStroke)) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
т SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
a) [Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
sh1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
sh2]

  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib1 <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"a ⊔ (b ⊓ c) = (a ⊔ b) ⊓ (a ⊔ c)"
                    (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) (Forall @"c" SBV Stroke
c) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c))
                    [Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
sh1, Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
sh3, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut]

  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib2 <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"a ⊓ (b ⊔ c) = (a ⊓ b) ⊔ (a ⊓ c)"
                    (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) (Forall @"c" SBV Stroke
c) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
c))
                    [Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
sh1, Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
sh3, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut]

  Proof (Forall "a" Stroke -> SBool)
compl1 <- String
-> (Forall "a" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"a ⊔ aᶜ = т" (\(Forall @"a" (SBV Stroke
a :: SStroke)) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
т) [Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
sh1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
sh2, Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
sh3, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
all_bot]
  Proof (Forall "a" Stroke -> SBool)
compl2 <- String
-> (Forall "a" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"a ⊓ aᶜ = ⲳ" (\(Forall @"a" (SBV Stroke
a :: SStroke)) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ) [Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
sh1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
all_bot]

  Proof (Forall "a" Stroke -> SBool)
bound1 <- String
-> (Forall "a" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> SBool))
forall t.
(Proposition (Forall "a" Stroke -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> SBool) t
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a ⊔ т = т" (\(Forall @"a"  SBV Stroke
a) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
т SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
т) (StepArgs (Forall "a" Stroke -> SBool) Stroke
 -> TP (Proof (Forall "a" Stroke -> SBool)))
-> StepArgs (Forall "a" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
                 \SBV Stroke
a -> [] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
т               SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident2
                           Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
т) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
т         SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2
                           Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
forall α. BooleanAlgebra α => α
т SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
т)         SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
compl1
                           Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
т) SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib1
                           Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
т)       SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident2
                           Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a             SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
compl1
                           Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
forall α. BooleanAlgebra α => α
т :: SStroke)
                           SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof (Forall "a" Stroke -> SBool)
bound2 <- String
-> (Forall "a" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> SBool))
forall t.
(Proposition (Forall "a" Stroke -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> SBool) t
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a ⊓ ⲳ = ⲳ" (\(Forall @"a" SBV Stroke
a) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ) (StepArgs (Forall "a" Stroke -> SBool) Stroke
 -> TP (Proof (Forall "a" Stroke -> SBool)))
-> StepArgs (Forall "a" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
                 \SBV Stroke
a -> [] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ               SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident1
                           Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ         SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1
                           Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ)         SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
compl2
                           Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ) SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib2
                           Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ)       SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident1
                           Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a             SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
compl2
                           Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ :: SStroke)
                           SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
absorb1 <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall t.
(Proposition (Forall "a" Stroke -> Forall "b" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> Forall "b" Stroke -> SBool) t
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a ⊔ (a ⊓ b) = a" (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
a) (StepArgs (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
 -> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
                  \SBV Stroke
a SBV Stroke
b -> [] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b)       SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident2
                             Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
т) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b) SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib2
                             Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
forall α. BooleanAlgebra α => α
т SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b)       SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1
                             Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
т)       SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
bound1
                             Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
т             SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident2
                             Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a
                             SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
absorb2 <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall t.
(Proposition (Forall "a" Stroke -> Forall "b" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> Forall "b" Stroke -> SBool) t
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a ⊓ (a ⊔ b) = a" (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
a) (StepArgs (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
 -> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
                  \SBV Stroke
a SBV Stroke
b -> [] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b)       SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident1
                             Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib1
                             Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b)       SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2
                             Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ)       SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
bound2
                             Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ             SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident1
                             Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a
                             SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof (Forall "a" Stroke -> SBool)
idemp2 <- String
-> (Forall "a" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> SBool))
forall t.
(Proposition (Forall "a" Stroke -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> SBool) t
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a ⊓ a = a" (\(Forall @"a" (SBV Stroke
a :: SStroke)) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
a) (StepArgs (Forall "a" Stroke -> SBool) Stroke
 -> TP (Proof (Forall "a" Stroke -> SBool)))
-> StepArgs (Forall "a" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
                 \SBV Stroke
a -> [] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a       SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident1
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ) SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
absorb2
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a
                          SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof (Forall "a" Stroke -> Forall "a'" Stroke -> SBool)
inv <- String
-> (Forall "a" Stroke -> Forall "a'" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke -> Forall "a'" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "a'" Stroke -> SBool))
forall t.
(Proposition (Forall "a" Stroke -> Forall "a'" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke -> Forall "a'" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> Forall "a'" Stroke -> SBool) t
-> TP (Proof (Forall "a" Stroke -> Forall "a'" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a ⊔ a' = т → a ⊓ a' = ⲳ → a' = aᶜ"
              (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"a'" SBV Stroke
a') -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
a' SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
т SBool -> SBool -> SBool
.=> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a' SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ SBool -> SBool -> SBool
.=> SBV Stroke
a' SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a) (StepArgs (Forall "a" Stroke -> Forall "a'" Stroke -> SBool) Stroke
 -> TP (Proof (Forall "a" Stroke -> Forall "a'" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke -> Forall "a'" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "a'" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
              \SBV Stroke
a SBV Stroke
a' -> [SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
a' SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
т, SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a' SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a'                     SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident2
                                                    Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a' SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
т                 SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
compl1
                                                    Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a' SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a)         SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib2
                                                    Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a' SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a' SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a)  SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2
                                                    Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a' SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a')  SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2
                                                    Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a') SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a')  SBV Stroke -> SBool -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a' SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ
                                                    Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a')         SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
compl2
                                                    Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a') SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2
                                                    Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a') SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib2
                                                    Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
a')         SBV Stroke -> SBool -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
a' SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
т
                                                    Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
т                SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident2
                                                    Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a
                                                    SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof (Forall "a" Stroke -> SBool)
dne      <- String
-> (Forall "a" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"aᶜᶜ = a"
                    (\(Forall @"a" (SBV Stroke
a :: SStroke)) -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
a)
                    [Proof (Forall "a" Stroke -> Forall "a'" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "a'" Stroke -> SBool)
inv, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
compl1, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
compl2, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2]

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
inv_elim <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"aᶜ = bᶜ → a = b"
                    (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBool -> SBool -> SBool
.=> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
b)
                    [Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
dne]

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
cancel <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"a ⊔ bᶜ = т → a ⊓ bᶜ = ⲳ → a = b"
                  (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
т SBool -> SBool -> SBool
.=> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ SBool -> SBool -> SBool
.=> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
b)
                  [Proof (Forall "a" Stroke -> Forall "a'" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "a'" Stroke -> SBool)
inv, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
inv_elim]

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
a1 <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall t.
(Proposition (Forall "a" Stroke -> Forall "b" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> Forall "b" Stroke -> SBool) t
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a ⊔ (aᶜ ⊔ b) = т" (\(Forall @"a" SBV Stroke
a) (Forall @"b" SBV Stroke
b)  -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
т) (StepArgs (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
 -> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
             \SBV Stroke
a SBV Stroke
b -> [] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b)               SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident2
                        Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
т         SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2
                        Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
forall α. BooleanAlgebra α => α
т SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b))         SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
compl1
                        Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b)) SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib1
                        Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b))       SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
absorb2
                        Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a                     SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
compl1
                        Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
forall α. BooleanAlgebra α => α
т :: SStroke)
                        SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
a2 <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall t.
(Proposition (Forall "a" Stroke -> Forall "b" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> Forall "b" Stroke -> SBool) t
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a ⊓ (aᶜ ⊓ b) = ⲳ" (\(Forall @"a" SBV Stroke
a) (Forall @"b" SBV Stroke
b)  -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ) (StepArgs (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
 -> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
             \SBV Stroke
a SBV Stroke
b -> [] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b)               SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident1
                        Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ         SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1
                        Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b))         SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
compl2
                        Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b)) SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib2
                        Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b))       SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
absorb1
                        Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a                     SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
compl2
                        Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ :: SStroke)
                        SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
dm1 <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"(a ⊔ b)ᶜ = aᶜ ⊓ bᶜ"
               (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ(SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b)
               [Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
a1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
a2, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
dne, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
ident1, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
ident2, Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib1, Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib2]

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
dm2 <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"(a ⨅ b)ᶜ = aᶜ ⨆ bᶜ"
               (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ(SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b)
               [Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
a1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
a2, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
dne, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
ident1, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
ident2, Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib1, Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib2]


  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
d1 <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"(a ⊔ (b ⊔ c)) ⊔ aᶜ = т"
              (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) (Forall @"c" SBV Stroke
c) -> (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
т)
              [Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
a1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
a2, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
ident1, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
ident2, Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib1, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
compl1, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
compl2, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
dm1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
dm2, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
idemp2]

  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
e1 <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"b ⊓ (a ⊔ (b ⊔ c)) = b"
              (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) (Forall @"c" SBV Stroke
c) -> SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
b)
              [Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib2, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
absorb1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
absorb2, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1]

  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
e2 <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"b ⊔ (a ⊓ (b ⊓ c)) = b" (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) (Forall @"c" SBV Stroke
c) -> SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
b) [Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
absorb1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
absorb2, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2]

  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
f1 <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall t.
(Proposition
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"(a ⊔ (b ⊔ c)) ⊔ bᶜ = т" (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) (Forall @"c" SBV Stroke
c) -> (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
т) (StepArgs
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
   Stroke
 -> TP
      (Proof
         (Forall "a" Stroke
          -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
             \SBV Stroke
a SBV Stroke
b SBV Stroke
c -> [] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b               SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c))               SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident2
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c))) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
т         SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
forall α. BooleanAlgebra α => α
т SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)))         SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
compl1
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c))) SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c))) SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib1
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)))         SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
e1
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b                           SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b                           SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
compl1
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
forall α. BooleanAlgebra α => α
т :: SStroke)
                          SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
g1 <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"(a ⊔ (b ⊔ c)) ⊔ cᶜ = т"
              (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) (Forall @"c" SBV Stroke
c) -> (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
c SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
т)
              [Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1, Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
f1]

  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
h1 <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall t.
(Proposition
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"(a ⊔ b ⊔ c)ᶜ ⊓ a = ⲳ"
             (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) (Forall @"c" SBV Stroke
c) -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ(SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ) (StepArgs
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
   Stroke
 -> TP
      (Proof
         (Forall "a" Stroke
          -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
             \SBV Stroke
a SBV Stroke
b SBV Stroke
c -> [] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ(SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a                    SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)                   SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
dm1
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
c)               SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident1
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅  (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ        SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
c))         SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
compl2
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
c)) SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib2
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
c))       SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
c SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b)))     SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
e2
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a                             SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
compl2
                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ :: SStroke)
                          SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
i1 <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"(a ⊔ b ⊔ c)ᶜ ⊓ b = ⲳ"
              (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) (Forall @"c" SBV Stroke
c) -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ(SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ)
              [Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1, Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
h1]

  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
j1 <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"(a ⊔ b ⊔ c)ᶜ ⊓ c = ⲳ"
              (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) (Forall @"c" SBV Stroke
c) -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ(SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
c SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ)
              [Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
a2, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
dne, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2]


  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
assoc1 <- do
    Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
c1 <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall t.
(Proposition
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"(a ⊔ (b ⊔ c)) ⊔ ((a ⊔ b) ⊔ c)ᶜ = т"
               (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) (Forall @"c" SBV Stroke
c) -> (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
т) (StepArgs
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
   Stroke
 -> TP
      (Proof
         (Forall "a" Stroke
          -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
               \SBV Stroke
a SBV Stroke
b SBV Stroke
c -> [] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)                        SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
dm1
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
c)                     SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib1
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
c) SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
g1
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
т                     SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident2
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b)                           SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib1
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b)         SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
d1
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
forall α. BooleanAlgebra α => α
т SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
b)                             SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
f1
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
forall α. BooleanAlgebra α => α
т SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
т :: SStroke)                                    SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
idemp2
                            TPProofRaw (SBV Stroke)
-> ChainsTo (TPProofRaw (SBV Stroke))
-> ChainsTo (TPProofRaw (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
forall α. BooleanAlgebra α => α
т :: SStroke)
                            SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

    Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
c2 <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall t.
(Proposition
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"(a ⊔ (b ⊔ c)) ⊓ ((a ⊔ b) ⊔ c)ᶜ = ⲳ"
               (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) (Forall @"c" SBV Stroke
c) -> (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ) (StepArgs
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
   Stroke
 -> TP
      (Proof
         (Forall "a" Stroke
          -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
               \SBV Stroke
a SBV Stroke
b SBV Stroke
c -> [] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)                    SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c))                    SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib2
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ ((SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ ((SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
h1
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ ((SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c))                    SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ((SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ                    SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident1
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)                          SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)                          SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib2
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
c)       SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
j1
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ                          SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
i1
                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ :: SStroke)                                SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident1
                            TPProofRaw (SBV Stroke)
-> ChainsTo (TPProofRaw (SBV Stroke))
-> ChainsTo (TPProofRaw (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ :: SStroke)
                            SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

    String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"a ⊔ (b ⊔ c) = (a ⊔ b) ⊔ c"
          (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) (Forall @"c" SBV Stroke
c) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
c)
          [Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
c1, Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
c2, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
cancel]

  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
assoc2 <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall t.
(Proposition
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a ⊓ (b ⊓ c) = (a ⊓ b) ⊓ c"
                 (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) (Forall @"c" SBV Stroke
c) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
c) SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
c) (StepArgs
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
   Stroke
 -> TP
      (Proof
         (Forall "a" Stroke
          -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
                 \SBV Stroke
a SBV Stroke
b SBV Stroke
c -> [] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
c)     SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
dne
                              Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ(SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
c)) SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
assoc1
                              Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧﬧ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
c) SBV Stroke
-> Proof (Forall "a" Stroke -> SBool) -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
dne
                              Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡   ((SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
c)
                              SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
le_antisymm <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall t.
(Proposition (Forall "a" Stroke -> Forall "b" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> Forall "b" Stroke -> SBool) t
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a ≤ b → b ≤ a → a = b"
                      (\(Forall @"a" SBV Stroke
a) (Forall @"b" SBV Stroke
b) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
b SBool -> SBool -> SBool
.=> SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
a SBool -> SBool -> SBool
.=> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
b) (StepArgs (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
 -> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke -> Forall "b" Stroke -> SBool) Stroke
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
                      \SBV Stroke
a SBV Stroke
b -> [SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
b, SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
a] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a     SBV Stroke -> SBool -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
b
                                             Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a SBV Stroke
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2
                                             Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b SBV Stroke -> SBool -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
a
                                             Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
b
                                             SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof (Forall "a" Stroke -> SBool)
le_refl <- String
-> (Forall "a" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"a ≤ a" (\(Forall @"a" SBV Stroke
a) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
a) [Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
idemp2]

  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
le_trans <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall t.
(Proposition
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a ≤ b → b ≤ c → a ≤ c" (\(Forall SBV Stroke
a) (Forall SBV Stroke
b) (Forall SBV Stroke
c) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
b SBool -> SBool -> SBool
.=> SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
c SBool -> SBool -> SBool
.=> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
c) (StepArgs
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
   Stroke
 -> TP
      (Proof
         (Forall "a" Stroke
          -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
                   \SBV Stroke
a SBV Stroke
b SBV Stroke
c -> [SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
b, SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
c] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a            SBV Stroke -> SBool -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
b
                                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a        SBV Stroke -> SBool -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
c
                                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
c SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a  SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
assoc2
                                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
c SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a)  SBV Stroke -> SBool -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
b
                                            Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
c SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a)
                                            SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
lt_iff_le_not_le <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"a < b ↔ a ≤ b ∧ ¬b ≤ a"
                            (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) -> (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
< SBV Stroke
b) SBool -> SBool -> SBool
.<=> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
b SBool -> SBool -> SBool
.&& SBool -> SBool
sNot (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
a))
                            [Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
sh3]

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
le_sup_left  <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"a ≤ a ⊔ b"
                  (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b)
                  [Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
absorb2]

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
le_sup_right <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"b ≤ a ⊔ b"
                  (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b)
                  [Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut1, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
absorb2]

  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
sup_le <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall t.
(Proposition
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a ≤ c → b ≤ c → a ⊔ b ≤ c"
                 (\(Forall SBV Stroke
a) (Forall SBV Stroke
b) (Forall SBV Stroke
c) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
c SBool -> SBool -> SBool
.=> SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
c SBool -> SBool -> SBool
.=> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
c) (StepArgs
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
   Stroke
 -> TP
      (Proof
         (Forall "a" Stroke
          -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
                 \SBV Stroke
a SBV Stroke
b SBV Stroke
c -> [SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
c, SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
c] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b             SBV Stroke -> [SBool] -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ [SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
c, SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
c]
                                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
c SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ (SBV Stroke
c SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b) SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib2
                                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
c SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
b)
                                          SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
inf_le_left  <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"a ⊓ b ≤ a"
                        (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
a)
                        [Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
assoc2,  Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
idemp2]

  Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
inf_le_right <- String
-> (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"a ⊓ b ≤ b"
                        (\(Forall @"a" (SBV Stroke
a :: SStroke)) (Forall @"b" SBV Stroke
b) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
b)
                        [Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2, Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
inf_le_left]

  Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
le_inf <- String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall t.
(Proposition
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool),
 SymVal t, EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     t
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a ≤ b → a ≤ c → a ≤ b ⊓ c"
                 (\(Forall SBV Stroke
a) (Forall SBV Stroke
b) (Forall SBV Stroke
c) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
b SBool -> SBool -> SBool
.=> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
c SBool -> SBool -> SBool
.=> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
c) (StepArgs
   (Forall "a" Stroke
    -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
   Stroke
 -> TP
      (Proof
         (Forall "a" Stroke
          -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)))
-> StepArgs
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
     Stroke
-> TP
     (Proof
        (Forall "a" Stroke
         -> Forall "b" Stroke -> Forall "c" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
                 \SBV Stroke
a SBV Stroke
b SBV Stroke
c -> [SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
b, SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
c] [SBool]
-> TPProofRaw (SBV Stroke) -> (SBool, TPProofRaw (SBV Stroke))
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a           SBV Stroke -> SBool -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
b
                                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a       SBV Stroke -> SBool -> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
c
                                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
c SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a) SBV Stroke
-> Proof
     (Forall "a" Stroke
      -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> Hinted (SBV Stroke)
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
assoc2
                                          Hinted (SBV Stroke)
-> ChainsTo (Hinted (SBV Stroke)) -> ChainsTo (Hinted (SBV Stroke))
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ (SBV Stroke
b SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
c SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a)
                                          SBV Stroke -> ChainsTo (SBV Stroke) -> ChainsTo (SBV Stroke)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo (SBV Stroke)
TPProofRaw (SBV Stroke)
forall a. TPProofRaw a
qed

  Proof
  (Forall "x" Stroke
   -> Forall "y" Stroke -> Forall "z" Stroke -> SBool)
le_sup_inf <- String
-> (Forall "x" Stroke
    -> Forall "y" Stroke -> Forall "z" Stroke -> SBool)
-> [ProofObj]
-> TP
     (Proof
        (Forall "x" Stroke
         -> Forall "y" Stroke -> Forall "z" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z"
                      (\(Forall SBV Stroke
x) (Forall SBV Stroke
y) (Forall SBV Stroke
z) -> (SBV Stroke
x SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
y) SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ (SBV Stroke
x SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
z) SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
x SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke
y SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
z)
                      [Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
-> ProofObj
forall a. Proof a -> ProofObj
p Proof
  (Forall "a" Stroke
   -> Forall "b" Stroke -> Forall "c" Stroke -> SBool)
distrib1, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
le_refl]

  Proof (Forall "x" Stroke -> SBool)
inf_compl_le_bot <- String
-> (Forall "x" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "x" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"x ⊓ xᶜ ≤ ⊥" (\(Forall SBV Stroke
x) -> SBV Stroke
x SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
x SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ) [Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
compl2, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
le_refl]
  Proof (Forall "x" Stroke -> SBool)
top_le_sup_compl <- String
-> (Forall "x" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "x" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"⊤ ≤ x ⊔ xᶜ" (\(Forall SBV Stroke
x) -> SBV Stroke
forall α. BooleanAlgebra α => α
т SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
x SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
x) [Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
compl1, Proof (Forall "a" Stroke -> SBool) -> ProofObj
forall a. Proof a -> ProofObj
p Proof (Forall "a" Stroke -> SBool)
le_refl]

  Proof (Forall "a" Stroke -> SBool)
le_top <- String
-> (Forall "a" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> SBool) Bool
-> TP (Proof (Forall "a" Stroke -> SBool))
forall t.
(Proposition (Forall "a" Stroke -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> SBool) t
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"a ≤ ⊤" (\(Forall @"a" SBV Stroke
a) -> SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
forall α. BooleanAlgebra α => α
т) (StepArgs (Forall "a" Stroke -> SBool) Bool
 -> TP (Proof (Forall "a" Stroke -> SBool)))
-> StepArgs (Forall "a" Stroke -> SBool) Bool
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
                 \SBV Stroke
a -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
forall α. BooleanAlgebra α => α
т
                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
forall α. BooleanAlgebra α => α
т SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
a SBool
-> Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
-> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> Forall "b" Stroke -> SBool)
commut2
                          TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
т SBool -> Proof (Forall "a" Stroke -> SBool) -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
ident2
                          TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
a SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
a
                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed

  Proof (Forall "a" Stroke -> SBool)
bot_le <- String
-> (Forall "a" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> SBool) Bool
-> TP (Proof (Forall "a" Stroke -> SBool))
forall t.
(Proposition (Forall "a" Stroke -> SBool), SymVal t,
 EqSymbolic (SBV t)) =>
String
-> (Forall "a" Stroke -> SBool)
-> StepArgs (Forall "a" Stroke -> SBool) t
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a t.
(Calc a, Proposition a, SymVal t, EqSymbolic (SBV t)) =>
String -> a -> StepArgs a t -> TP (Proof a)
calc String
"⊥ ≤ a" (\(Forall @"a" SBV Stroke
a) -> SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
a) (StepArgs (Forall "a" Stroke -> SBool) Bool
 -> TP (Proof (Forall "a" Stroke -> SBool)))
-> StepArgs (Forall "a" Stroke -> SBool) Bool
-> TP (Proof (Forall "a" Stroke -> SBool))
forall a b. (a -> b) -> a -> b
$
                 \SBV Stroke
a -> [] [SBool] -> TPProofRaw SBool -> (SBool, TPProofRaw SBool)
forall a. [SBool] -> TPProofRaw a -> (SBool, TPProofRaw a)
⊢ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ SBV Stroke -> SBV Stroke -> SBool
forall α. BooleanAlgebra α => α -> α -> SBool
≤ SBV Stroke
a
                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
a SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ            SBool -> Proof (Forall "a" Stroke -> SBool) -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
∵ Proof (Forall "a" Stroke -> SBool)
bound2
                          TPProofRaw SBool
-> ChainsTo (TPProofRaw SBool) -> ChainsTo (TPProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SBV Stroke
forall α. BooleanAlgebra α => α
ⲳ :: SStroke)
                          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
≡ ChainsTo SBool
TPProofRaw SBool
forall a. TPProofRaw a
qed

  Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool)
sdiff_eq <- String
-> (Forall "x" Stroke -> Forall "y" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"x \\ y = x ⊓ yᶜ" (\(Forall SBV Stroke
x) (Forall SBV Stroke
y) -> SBV Stroke
x SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
\\ SBV Stroke
y SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
x SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨅ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
y) []
  Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool)
himp_eq  <- String
-> (Forall "x" Stroke -> Forall "y" Stroke -> SBool)
-> [ProofObj]
-> TP (Proof (Forall "x" Stroke -> Forall "y" Stroke -> SBool))
forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
"x ⇨ y = y ⊔ xᶜ"  (\(Forall SBV Stroke
x) (Forall SBV Stroke
y) -> SBV Stroke
x SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⇨ SBV Stroke
y SBV Stroke -> SBV Stroke -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SBV Stroke
y SBV Stroke -> SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α -> α
⨆ SBV Stroke -> SBV Stroke
forall α. BooleanAlgebra α => α -> α
ﬧ SBV Stroke
x)  []

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