{-# LANGUAGE NoImplicitPrelude #-}

{-# LANGUAGE MultiParamTypeClasses #-}

-- |

-- Module      : OAlg.Data.Boolean.Proposition

-- Description : propositions on boolean structures.

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

-- 

-- propositions on boolean structures which must always be true, i.e. tautologies. They

-- serve also to describe the semantic of the boolean operators.

module OAlg.Data.Boolean.Proposition
  ( prpBool, prpBoolTautologies
  
    -- * Tautologies

  , prpTautologies
    
    -- ** Not

  , prpNotNot

    -- ** And

  , prpAndAssoc, prpAndOr, prpAndTrue, prpAnd0, prpAnds

    -- ** Or

  , prpOrAssoc, prpOrAnd, prpOr0, prpOrs

    -- * Impl

  , prpImplRefl, prpImplFalseEverything, prpImplCurry, prpImplTransitive

    -- * Eqvl

  , prpEqvlAnd

    -- * Lazy

  , prpLazy, prpLazyAnd, prpLazyOr, prpLazyImpl
  )
  where

import Prelude(IO,undefined)

import Control.Monad

import Data.List(take,repeat)

import OAlg.Category.Definition

import OAlg.Data.Identity
import OAlg.Data.Logical
import OAlg.Data.Canonical
import OAlg.Data.Number
import OAlg.Data.Boolean.Definition
import OAlg.Data.Statement.Definition
import OAlg.Data.X

--------------------------------------------------------------------------------

-- not -

-- | for all @p@ holds: @'not' ('not' p) '<~>' p@.

prpNotNot :: Boolean b => b -> b
prpNotNot :: forall b. Boolean b => b -> b
prpNotNot b
p = b -> b
forall b. Boolean b => b -> b
not (b -> b
forall b. Boolean b => b -> b
not b
p) b -> b -> b
forall b. Boolean b => b -> b -> b
<~> b
p

--------------------------------------------------------------------------------

-- and -


-- | for all @a@, @b@ and @c@ holds: @(a '&&' b) '&&' c '<~>' a '&&' (b '&&' c)@.

prpAndAssoc :: Boolean b => b -> b -> b -> b
prpAndAssoc :: forall b. Boolean b => b -> b -> b -> b
prpAndAssoc b
a b
b b
c = (b
a b -> b -> b
forall a. Logical a => a -> a -> a
&& b
b) b -> b -> b
forall a. Logical a => a -> a -> a
&& b
c b -> b -> b
forall b. Boolean b => b -> b -> b
<~> b
a b -> b -> b
forall a. Logical a => a -> a -> a
&& (b
b b -> b -> b
forall a. Logical a => a -> a -> a
&& b
c)

-- | for all @a@, @b@ and @c@ holds: @(a '&&' b) '||' c '<~>' (a '||' c) '&&' (b '||' c)@.

prpAndOr :: Boolean b => b -> b -> b -> b
prpAndOr :: forall b. Boolean b => b -> b -> b -> b
prpAndOr b
a b
b b
c = (b
a b -> b -> b
forall a. Logical a => a -> a -> a
&& b
b) b -> b -> b
forall a. Logical a => a -> a -> a
|| b
c b -> b -> b
forall b. Boolean b => b -> b -> b
<~> (b
a b -> b -> b
forall a. Logical a => a -> a -> a
|| b
c) b -> b -> b
forall a. Logical a => a -> a -> a
&& (b
b b -> b -> b
forall a. Logical a => a -> a -> a
|| b
c)

-- | for all @p@ holds: @'true' '&&' p '<~>' p@.

prpAndTrue :: Boolean b => b -> b
prpAndTrue :: forall b. Boolean b => b -> b
prpAndTrue b
p = b
forall b. Boolean b => b
true b -> b -> b
forall a. Logical a => a -> a -> a
&& b
p b -> b -> b
forall b. Boolean b => b -> b -> b
<~> b
p

-- | @'and' [] '<~>' 'true'@.

prpAnd0 :: Boolean b => b
prpAnd0 :: forall b. Boolean b => b
prpAnd0 = [b] -> b
forall b. Boolean b => [b] -> b
and [] b -> b -> b
forall b. Boolean b => b -> b -> b
<~> b
forall b. Boolean b => b
true

-- | for all @a@ and @as@ holds: @'and' (a':'as) '<~>' a '&&' 'and' as@.

prpAnds :: Boolean b => b -> [b] -> b
prpAnds :: forall b. Boolean b => b -> [b] -> b
prpAnds b
a [b]
as = [b] -> b
forall b. Boolean b => [b] -> b
and (b
ab -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
as) b -> b -> b
forall b. Boolean b => b -> b -> b
<~> b
a b -> b -> b
forall a. Logical a => a -> a -> a
&& [b] -> b
forall b. Boolean b => [b] -> b
and [b]
as

-- | substituting equivalent boolenas in '&&' yiels equivalent booleans, i.e.

--   @for all @(a,a')@ and @(b,b')@ holds:

--   (a '<~>' a') '&&' (b '<~>' b') '~>' ((a '&&' b) '<~>' (a' '&&' b'))@.

prpAndSubs :: Boolean b => (b,b) -> (b,b) -> b
prpAndSubs :: forall b. Boolean b => (b, b) -> (b, b) -> b
prpAndSubs (b
a,b
a') (b
b,b
b') = (b
a b -> b -> b
forall b. Boolean b => b -> b -> b
<~> b
a') b -> b -> b
forall a. Logical a => a -> a -> a
&& (b
b b -> b -> b
forall b. Boolean b => b -> b -> b
<~> b
b') b -> b -> b
forall b. Boolean b => b -> b -> b
~> ((b
a b -> b -> b
forall a. Logical a => a -> a -> a
&& b
b) b -> b -> b
forall b. Boolean b => b -> b -> b
<~> (b
a' b -> b -> b
forall a. Logical a => a -> a -> a
&& b
b'))

--------------------------------------------------------------------------------

-- Or -


-- | for all @a@, @b@ and @c@ holds: @(a '||' b) '||' c '<~>' a '||' (b '||' c)@.

prpOrAssoc :: Boolean  b => b -> b -> b -> b
prpOrAssoc :: forall b. Boolean b => b -> b -> b -> b
prpOrAssoc b
a b
b b
c = (b
a b -> b -> b
forall a. Logical a => a -> a -> a
|| b
b) b -> b -> b
forall a. Logical a => a -> a -> a
|| b
c b -> b -> b
forall b. Boolean b => b -> b -> b
<~> b
a b -> b -> b
forall a. Logical a => a -> a -> a
|| (b
b b -> b -> b
forall a. Logical a => a -> a -> a
|| b
c)

-- | for all @a@, @b@ and @c@ holds: @(a '||' b) '&&' c '<~>' (a '&&' c) '||' (b '&&' c)@.

prpOrAnd ::  Boolean b => b -> b -> b -> b
prpOrAnd :: forall b. Boolean b => b -> b -> b -> b
prpOrAnd b
a b
b b
c = (b
a b -> b -> b
forall a. Logical a => a -> a -> a
|| b
b) b -> b -> b
forall a. Logical a => a -> a -> a
&& b
c b -> b -> b
forall b. Boolean b => b -> b -> b
<~> (b
a b -> b -> b
forall a. Logical a => a -> a -> a
&& b
c) b -> b -> b
forall a. Logical a => a -> a -> a
|| (b
b b -> b -> b
forall a. Logical a => a -> a -> a
&& b
c)

-- | for all @p@ holds:  @'false' '||' p '<~>' p@.

prpOrFalse :: Boolean b => b -> b
prpOrFalse :: forall b. Boolean b => b -> b
prpOrFalse b
p = b
forall b. Boolean b => b
false b -> b -> b
forall a. Logical a => a -> a -> a
|| b
p b -> b -> b
forall b. Boolean b => b -> b -> b
<~> b
p

-- | @'or' [] '<~>' 'false'@.

prpOr0 :: Boolean b => b
prpOr0 :: forall b. Boolean b => b
prpOr0 = [b] -> b
forall b. Boolean b => [b] -> b
or [] b -> b -> b
forall b. Boolean b => b -> b -> b
<~> b
forall b. Boolean b => b
false

-- | @for all @a@ and @as@ holds: 'or' (a':'as) '<~>' a '||' 'or' as@.

prpOrs :: Boolean b => b -> [b] -> b
prpOrs :: forall b. Boolean b => b -> [b] -> b
prpOrs b
a [b]
as = [b] -> b
forall b. Boolean b => [b] -> b
or (b
ab -> [b] -> [b]
forall a. a -> [a] -> [a]
:[b]
as) b -> b -> b
forall b. Boolean b => b -> b -> b
<~> b
a b -> b -> b
forall a. Logical a => a -> a -> a
|| [b] -> b
forall b. Boolean b => [b] -> b
or [b]
as

--------------------------------------------------------------------------------

-- Impl -


-- | @for all @p@ holds: p '~>' p@.

prpImplRefl :: Boolean b => b -> b
prpImplRefl :: forall b. Boolean b => b -> b
prpImplRefl b
p = b
p b -> b -> b
forall b. Boolean b => b -> b -> b
~> b
p

-- | for all @p@ holds: @'false' '~>' (p '<~>' 'true')@.

--

--   i.e. a false premisis implies everithing.

prpImplFalseEverything :: Boolean b => b -> b
prpImplFalseEverything :: forall b. Boolean b => b -> b
prpImplFalseEverything b
p = b
forall b. Boolean b => b
false b -> b -> b
forall b. Boolean b => b -> b -> b
~> (b
p b -> b -> b
forall b. Boolean b => b -> b -> b
<~> b
forall b. Boolean b => b
true)

-- | for all @a@, @b@ and @c@ holds: @((a '&&' b) '~>' c) '<~>' (a '~>' b '~>' c)@.

prpImplCurry :: Boolean b => b -> b -> b -> b
prpImplCurry :: forall b. Boolean b => b -> b -> b -> b
prpImplCurry b
a b
b b
c = ((b
a b -> b -> b
forall a. Logical a => a -> a -> a
&& b
b) b -> b -> b
forall b. Boolean b => b -> b -> b
~> b
c) b -> b -> b
forall b. Boolean b => b -> b -> b
<~> (b
a b -> b -> b
forall b. Boolean b => b -> b -> b
~> b
b b -> b -> b
forall b. Boolean b => b -> b -> b
~> b
c)

-- | for all @a@, @b@ and @c@ holds: @(a '~>' b) '&&' (b '~>' c) '~>' (a '~>' c)@. 

prpImplTransitive :: Boolean b => b -> b -> b -> b
prpImplTransitive :: forall b. Boolean b => b -> b -> b -> b
prpImplTransitive b
a b
b b
c = (b
a b -> b -> b
forall b. Boolean b => b -> b -> b
~> b
b) b -> b -> b
forall a. Logical a => a -> a -> a
&& (b
b b -> b -> b
forall b. Boolean b => b -> b -> b
~> b
c) b -> b -> b
forall b. Boolean b => b -> b -> b
~> (b
a b -> b -> b
forall b. Boolean b => b -> b -> b
~> b
c)

--------------------------------------------------------------------------------

-- Eqvl -


-- | for all @a@ and @b@ holds: @(a '<~>' b) '<~>' ((a '~>' b) && (b '~>' a))@.

prpEqvlAnd :: Boolean b => b -> b -> b
prpEqvlAnd :: forall b. Boolean b => b -> b -> b
prpEqvlAnd b
a b
b = (b
a b -> b -> b
forall b. Boolean b => b -> b -> b
<~> b
b) b -> b -> b
forall b. Boolean b => b -> b -> b
<~> ((b
a b -> b -> b
forall b. Boolean b => b -> b -> b
~> b
b) b -> b -> b
forall a. Logical a => a -> a -> a
&& (b
b b -> b -> b
forall b. Boolean b => b -> b -> b
~> b
a))

--------------------------------------------------------------------------------

-- lazy -


-- | lazy evaluation of '&&', i.e. @'false' '&&' 'undefined' '<~>' 'false'@.

--

--  __Note__ @('undefined' '&&' 'false')@ evaluates to an exception!

prpLazyAnd :: Boolean b => b
prpLazyAnd :: forall b. Boolean b => b
prpLazyAnd = b
forall b. Boolean b => b
false b -> b -> b
forall a. Logical a => a -> a -> a
&& b
forall a. HasCallStack => a
undefined b -> b -> b
forall b. Boolean b => b -> b -> b
<~> b
forall b. Boolean b => b
false

-- | lazy evaluationof '||', i.e. @'true' '||' 'undefined'@.

prpLazyOr :: Boolean b => b
prpLazyOr :: forall b. Boolean b => b
prpLazyOr = b
forall b. Boolean b => b
true b -> b -> b
forall a. Logical a => a -> a -> a
|| b
forall a. HasCallStack => a
undefined

-- | lazy evaluation of '~>', i.e. @'false' ':=>' 'undefined'@.

prpLazyImpl :: Boolean b => b
prpLazyImpl :: forall b. Boolean b => b
prpLazyImpl = b
forall b. Boolean b => b
false b -> b -> b
forall b. Boolean b => b -> b -> b
~> b
forall a. HasCallStack => a
undefined

--------------------------------------------------------------------------------

-- prpTautologies -


-- | tautologies on boolean structures.

prpTautologies :: Boolean b => (b -> Statement) -> X b -> X [b] -> Statement
prpTautologies :: forall b.
Boolean b =>
(b -> Statement) -> X b -> X [b] -> Statement
prpTautologies b -> Statement
prp X b
xb X [b]
xbs = String -> Label
Prp String
"Tautologies"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ -- Not

              String -> Label
Prp String
"NotNot" Label -> Statement -> Statement
:<=>: X b -> (b -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X b
xb (b -> Statement
prp (b -> Statement) -> (b -> b) -> b -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. b -> b
forall b. Boolean b => b -> b
prpNotNot)

              -- And

            , String -> Label
Prp String
"AndAssoc" Label -> Statement -> Statement
:<=>: X (b, b, b) -> ((b, b, b) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (b, b, b)
xabc (b -> Statement
prp (b -> Statement) -> ((b, b, b) -> b) -> (b, b, b) -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. ((b -> b -> b -> b) -> (b, b, b) -> b
forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 b -> b -> b -> b
forall b. Boolean b => b -> b -> b -> b
prpAndAssoc))
            , String -> Label
Prp String
"AndOr" Label -> Statement -> Statement
:<=>: X (b, b, b) -> ((b, b, b) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (b, b, b)
xabc (b -> Statement
prp (b -> Statement) -> ((b, b, b) -> b) -> (b, b, b) -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. ((b -> b -> b -> b) -> (b, b, b) -> b
forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 b -> b -> b -> b
forall b. Boolean b => b -> b -> b -> b
prpAndOr))
            , String -> Label
Prp String
"AndTrue" Label -> Statement -> Statement
:<=>: X b -> (b -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X b
xb (b -> Statement
prp (b -> Statement) -> (b -> b) -> b -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. b -> b
forall b. Boolean b => b -> b
prpAndTrue)
            , String -> Label
Prp String
"And0" Label -> Statement -> Statement
:<=>: b -> Statement
prp b
forall b. Boolean b => b
prpAnd0
            , String -> Label
Prp String
"Ands" Label -> Statement -> Statement
:<=>: X (b, [b]) -> ((b, [b]) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (b, [b])
xbbs (b -> Statement
prp (b -> Statement) -> ((b, [b]) -> b) -> (b, [b]) -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. ((b -> [b] -> b) -> (b, [b]) -> b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry b -> [b] -> b
forall b. Boolean b => b -> [b] -> b
prpAnds))

              -- Or

            , String -> Label
Prp String
"OrAssoc" Label -> Statement -> Statement
:<=>: X (b, b, b) -> ((b, b, b) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (b, b, b)
xabc (b -> Statement
prp (b -> Statement) -> ((b, b, b) -> b) -> (b, b, b) -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. ((b -> b -> b -> b) -> (b, b, b) -> b
forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 b -> b -> b -> b
forall b. Boolean b => b -> b -> b -> b
prpOrAssoc))
            , String -> Label
Prp String
"OrAnd" Label -> Statement -> Statement
:<=>: X (b, b, b) -> ((b, b, b) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (b, b, b)
xabc (b -> Statement
prp (b -> Statement) -> ((b, b, b) -> b) -> (b, b, b) -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. ((b -> b -> b -> b) -> (b, b, b) -> b
forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 b -> b -> b -> b
forall b. Boolean b => b -> b -> b -> b
prpOrAnd))
            , String -> Label
Prp String
"OrFalse" Label -> Statement -> Statement
:<=>: X b -> (b -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X b
xb (b -> Statement
prp (b -> Statement) -> (b -> b) -> b -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. b -> b
forall b. Boolean b => b -> b
prpOrFalse)
            , String -> Label
Prp String
"Or0" Label -> Statement -> Statement
:<=>: b -> Statement
prp b
forall b. Boolean b => b
prpOr0
            , String -> Label
Prp String
"Ors" Label -> Statement -> Statement
:<=>: X (b, [b]) -> ((b, [b]) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (b, [b])
xbbs (b -> Statement
prp (b -> Statement) -> ((b, [b]) -> b) -> (b, [b]) -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. ((b -> [b] -> b) -> (b, [b]) -> b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry b -> [b] -> b
forall b. Boolean b => b -> [b] -> b
prpOrs))

              -- Impl

            , String -> Label
Prp String
"ImplRefl" Label -> Statement -> Statement
:<=>: X b -> (b -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X b
xb (b -> Statement
prp (b -> Statement) -> (b -> b) -> b -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. b -> b
forall b. Boolean b => b -> b
prpImplRefl)
            , String -> Label
Prp String
"ImplFalseEverything" Label -> Statement -> Statement
:<=>: X b -> (b -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X b
xb (b -> Statement
prp (b -> Statement) -> (b -> b) -> b -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. b -> b
forall b. Boolean b => b -> b
prpImplFalseEverything)
            , String -> Label
Prp String
"ImplCurry" Label -> Statement -> Statement
:<=>: X (b, b, b) -> ((b, b, b) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (b, b, b)
xabc (b -> Statement
prp (b -> Statement) -> ((b, b, b) -> b) -> (b, b, b) -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. ((b -> b -> b -> b) -> (b, b, b) -> b
forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 b -> b -> b -> b
forall b. Boolean b => b -> b -> b -> b
prpImplCurry))
            , String -> Label
Prp String
"ImplTransitive" Label -> Statement -> Statement
:<=>: X (b, b, b) -> ((b, b, b) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (b, b, b)
xabc (b -> Statement
prp (b -> Statement) -> ((b, b, b) -> b) -> (b, b, b) -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. ((b -> b -> b -> b) -> (b, b, b) -> b
forall a b c d. (a -> b -> c -> d) -> (a, b, c) -> d
uncurry3 b -> b -> b -> b
forall b. Boolean b => b -> b -> b -> b
prpImplTransitive))

              -- Eqvl

            , String -> Label
Prp String
"EqvlAnd" Label -> Statement -> Statement
:<=>: X (b, b) -> ((b, b) -> Statement) -> Statement
forall x. X x -> (x -> Statement) -> Statement
Forall X (b, b)
xab (b -> Statement
prp (b -> Statement) -> ((b, b) -> b) -> (b, b) -> Statement
forall y z x. (y -> z) -> (x -> y) -> x -> z
forall (c :: * -> * -> *) y z x.
Category c =>
c y z -> c x y -> c x z
. ((b -> b -> b) -> (b, b) -> b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry b -> b -> b
forall b. Boolean b => b -> b -> b
prpEqvlAnd))
            ]
  where xab :: X (b, b)
xab  = X b -> X b -> X (b, b)
forall a b. X a -> X b -> X (a, b)
xTupple2 X b
xb X b
xb
        xabc :: X (b, b, b)
xabc = X b -> X b -> X b -> X (b, b, b)
forall a b c. X a -> X b -> X c -> X (a, b, c)
xTupple3 X b
xb X b
xb X b
xb
        xbbs :: X (b, [b])
xbbs = X b -> X [b] -> X (b, [b])
forall a b. X a -> X b -> X (a, b)
xTupple2 X b
xb X [b]
xbs

--------------------------------------------------------------------------------

-- prpBoolTautologies -


-- | tautologies for 'Bool'.

prpBoolTautologies :: Statement
prpBoolTautologies :: Statement
prpBoolTautologies = String -> Label
Prp String
"BoolTautologies"
  Label -> Statement -> Statement
:<=>: (Bool -> Statement) -> X Bool -> X [Bool] -> Statement
forall b.
Boolean b =>
(b -> Statement) -> X b -> X [b] -> Statement
prpTautologies Bool -> Statement
forall a b. Embeddable a b => a -> b
inj X Bool
xBool (N -> N -> X Bool -> X [Bool]
forall x. N -> N -> X x -> X [x]
xTakeB N
0 N
10 X Bool
xBool)
  
--------------------------------------------------------------------------------

-- prpLazy -


-- | laziness of 'and', 'or' and @('~>')@.

prpLazy :: Boolean b => (b -> Statement) -> Statement
prpLazy :: forall b. Boolean b => (b -> Statement) -> Statement
prpLazy b -> Statement
prp = String -> Label
Prp String
"Lazy"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ String -> Label
Prp String
"LazyAnd" Label -> Statement -> Statement
:<=>: b -> Statement
prp b
forall b. Boolean b => b
prpLazyAnd
            , String -> Label
Prp String
"LazyOr" Label -> Statement -> Statement
:<=>: b -> Statement
prp b
forall b. Boolean b => b
prpLazyOr
            , String -> Label
Prp String
"LazyImpl" Label -> Statement -> Statement
:<=>: b -> Statement
prp b
forall b. Boolean b => b
prpLazyImpl
            ]
  
xbDst :: Int -> X Bool -> IO ()
xbDst :: Int -> X Bool -> IO ()
xbDst Int
n X Bool
xb = IO Omega
getOmega IO Omega -> (Omega -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> X Bool -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n X Bool
xb

xabDst :: Int -> X Bool -> IO ()
xabDst :: Int -> X Bool -> IO ()
xabDst Int
n X Bool
xb = IO Omega
getOmega IO Omega -> (Omega -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> X (Bool, Bool) -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n X (Bool, Bool)
xab where
  xab :: X (Bool, Bool)
xab = X Bool -> X Bool -> X (Bool, Bool)
forall a b. X a -> X b -> X (a, b)
xTupple2 X Bool
xb X Bool
xb

xabcDst :: Int -> X Bool -> IO ()
xabcDst :: Int -> X Bool -> IO ()
xabcDst Int
n X Bool
xb = IO Omega
getOmega IO Omega -> (Omega -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> X (Bool, Bool, Bool) -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n X (Bool, Bool, Bool)
xabc where
  xabc :: X (Bool, Bool, Bool)
xabc = X Bool -> X Bool -> X Bool -> X (Bool, Bool, Bool)
forall a b c. X a -> X b -> X c -> X (a, b, c)
xTupple3 X Bool
xb X Bool
xb X Bool
xb

xbbsDst :: Int -> Int -> X Bool -> IO ()
xbbsDst :: Int -> Int -> X Bool -> IO ()
xbbsDst Int
n Int
m X Bool
xb = IO Omega
getOmega IO Omega -> (Omega -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Int -> X (Bool, [Bool]) -> Omega -> IO ()
forall x. (Show x, Ord x) => Int -> X x -> Omega -> IO ()
putDistribution Int
n X (Bool, [Bool])
xbbs where
  xbs :: X [Bool]
xbs  = Int -> Int -> X Int
xIntB Int
0 Int
m X Int -> (Int -> X [Bool]) -> X [Bool]
forall a b. X a -> (a -> X b) -> X b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Int
n' -> [X Bool] -> X [Bool]
forall x. [X x] -> X [x]
xList ([X Bool] -> X [Bool]) -> [X Bool] -> X [Bool]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ Int -> [X Bool] -> [X Bool]
forall a. Int -> [a] -> [a]
take Int
n' ([X Bool] -> [X Bool]) -> [X Bool] -> [X Bool]
forall (h :: * -> * -> *) x y. Applicative h => h x y -> x -> y
$ X Bool -> [X Bool]
forall a. a -> [a]
repeat X Bool
xb
  xbbs :: X (Bool, [Bool])
xbbs = X Bool -> X [Bool] -> X (Bool, [Bool])
forall a b. X a -> X b -> X (a, b)
xTupple2 X Bool
xb X [Bool]
xbs

--------------------------------------------------------------------------------

-- prpBool -


-- | validity of the 'Boolean' structure of 'Bool'.

prpBool :: Statement
prpBool :: Statement
prpBool = String -> Label
Prp String
"Bool"
  Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ Statement
prpBoolTautologies
            , (Bool -> Statement) -> Statement
forall b. Boolean b => (b -> Statement) -> Statement
prpLazy (Bool -> Statement
forall a b. Embeddable a b => a -> b
inj :: Bool -> Statement)
            ]