{-# LANGUAGE NoImplicitPrelude #-}

-- |

-- Module      : OAlg.Structure.Vectorial.Definition

-- Description : propositions on basic algebraic structures

-- Copyright   : (c) Erich Gut

-- License     : BSD3

-- Maintainer  : zerich.gut@gmail.com

--

-- propositions on basic algebraic structures.

module OAlg.Structure.Proposition
  ( -- * Proposition

    prpStructure
  , prpStructureN, prpStructureZ, prpStructureQ
  , prpStructureOS
  )

  where

import OAlg.Prelude


import OAlg.Structure.Lattice
import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Fibred
import OAlg.Structure.FibredOriented
import OAlg.Structure.Additive
import OAlg.Structure.Distributive

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

-- prpStructureN -


-- | validity of the algebraic structure of 'N'.

prpStructureN :: Statement
prpStructureN :: Statement
prpStructureN = String -> Label
Prp String
"StructureN" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ XOrt N -> Statement
forall q. Oriented q => XOrt q -> Statement
prpOrt (XOrt N
forall x. XStandard x => X x
xStandard :: XOrt N)
      , XMlt N -> Statement
forall c. Multiplicative c => XMlt c -> Statement
prpMlt (XMlt N
forall c. XStandardMlt c => XMlt c
xStandardMlt :: XMlt N)
      , XOrt N -> Statement
forall f. Fibred f => XFbr f -> Statement
prpFbr (XOrt N
forall x. XStandard x => X x
xStandard :: XFbr N)
      , XOrt N -> Statement
forall f. FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt (XOrt N
forall x. XStandard x => X x
xStandard :: XFbrOrt N)
      , XAdd N -> Statement
forall a. Additive a => XAdd a -> Statement
prpAdd (XAdd N
forall a. XStandardAdd a => XAdd a
xStandardAdd :: XAdd N)
      , XDst N -> Statement
forall d. Distributive d => XDst d -> Statement
prpDst (XDst N
forall d. XStandardDst d => XDst d
xStandardDst :: XDst N)
      ]

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

-- prpStructureZ -


-- | validity of the algebraic structure of 'Z'.

prpStructureZ :: Statement
prpStructureZ :: Statement
prpStructureZ = String -> Label
Prp String
"StructureZ" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ XOrt Z -> Statement
forall q. Oriented q => XOrt q -> Statement
prpOrt (XOrt Z
forall x. XStandard x => X x
xStandard :: XOrt Z)
      , XMlt Z -> Statement
forall c. Multiplicative c => XMlt c -> Statement
prpMlt (XMlt Z
forall c. XStandardMlt c => XMlt c
xStandardMlt :: XMlt Z)
      , XOrt Z -> Statement
forall f. Fibred f => XFbr f -> Statement
prpFbr (XOrt Z
forall x. XStandard x => X x
xStandard :: XFbr Z)
      , XOrt Z -> Statement
forall f. FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt (XOrt Z
forall x. XStandard x => X x
xStandard :: XFbrOrt Z)
      , XAdd Z -> Statement
forall a. Additive a => XAdd a -> Statement
prpAdd (XAdd Z
forall a. XStandardAdd a => XAdd a
xStandardAdd :: XAdd Z)
      , XDst Z -> Statement
forall d. Distributive d => XDst d -> Statement
prpDst (XDst Z
forall d. XStandardDst d => XDst d
xStandardDst :: XDst Z)
      ]

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

-- prpStructureQ -


-- | validity of the algebraic structure of 'Q'.

prpStructureQ :: Statement
prpStructureQ :: Statement
prpStructureQ = String -> Label
Prp String
"StructureQ" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ XOrt Q -> Statement
forall q. Oriented q => XOrt q -> Statement
prpOrt (XOrt Q
forall x. XStandard x => X x
xStandard :: XOrt Q)
      , XMlt Q -> Statement
forall c. Multiplicative c => XMlt c -> Statement
prpMlt (XMlt Q
forall c. XStandardMlt c => XMlt c
xStandardMlt :: XMlt Q)
      , XOrt Q -> Statement
forall f. Fibred f => XFbr f -> Statement
prpFbr (XOrt Q
forall x. XStandard x => X x
xStandard :: XFbr Q)
      , XOrt Q -> Statement
forall f. FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt (XOrt Q
forall x. XStandard x => X x
xStandard :: XFbrOrt Q)
      , XAdd Q -> Statement
forall a. Additive a => XAdd a -> Statement
prpAdd (XAdd Q
forall a. XStandardAdd a => XAdd a
xStandardAdd :: XAdd Q)
      , XDst Q -> Statement
forall d. Distributive d => XDst d -> Statement
prpDst (XDst Q
forall d. XStandardDst d => XDst d
xStandardDst :: XDst Q)
      ]

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

-- prpStructureOS -


-- | validity of the algebraic structure of 'OS'.

prpStructureOS :: Statement
prpStructureOS :: Statement
prpStructureOS = String -> Label
Prp String
"StructureOS" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ XOrt OS -> Statement
forall q. Oriented q => XOrt q -> Statement
prpOrt (XOrt OS
forall x. XStandard x => X x
xStandard :: XOrt OS)
      , XMlt OS -> Statement
forall c. Multiplicative c => XMlt c -> Statement
prpMlt (XMlt OS
forall c. XStandardMlt c => XMlt c
xStandardMlt :: XMlt OS)
      , XOrt OS -> Statement
forall f. Fibred f => XFbr f -> Statement
prpFbr (XOrt OS
forall x. XStandard x => X x
xStandard :: XFbr OS)
      , XOrt OS -> Statement
forall f. FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt (XOrt OS
forall x. XStandard x => X x
xStandard :: XFbrOrt OS)
      , XAdd OS -> Statement
forall a. Additive a => XAdd a -> Statement
prpAdd (XAdd OS
forall a. XStandardAdd a => XAdd a
xStandardAdd :: XAdd OS)
      , XDst OS -> Statement
forall d. Distributive d => XDst d -> Statement
prpDst (XDst OS
forall d. XStandardDst d => XDst d
xStandardDst :: XDst OS)
      ]

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

-- prpStructureOp -


prpStructureOp :: Statement
prpStructureOp :: Statement
prpStructureOp = String -> Label
Prp String
"StructureOp" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ XOrt (Op OS) -> Statement
forall q. Oriented q => XOrt q -> Statement
prpOrt (XOrt (Op OS)
forall x. XStandard x => X x
xStandard :: XOrt (Op OS))
      , XMlt (Op OS) -> Statement
forall c. Multiplicative c => XMlt c -> Statement
prpMlt (XMlt (Op OS)
forall c. XStandardMlt c => XMlt c
xStandardMlt :: XMlt (Op OS))
      , XOrt (Op OS) -> Statement
forall f. Fibred f => XFbr f -> Statement
prpFbr (XOrt (Op OS)
forall x. XStandard x => X x
xStandard :: XFbr (Op OS))
      , XOrt (Op OS) -> Statement
forall f. FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt (XOrt (Op OS)
forall x. XStandard x => X x
xStandard :: XFbrOrt (Op OS))
      , XAdd (Op OS) -> Statement
forall a. Additive a => XAdd a -> Statement
prpAdd (XAdd (Op OS)
forall a. XStandardAdd a => XAdd a
xStandardAdd :: XAdd (Op OS))
      , XDst (Op OS) -> Statement
forall d. Distributive d => XDst d -> Statement
prpDst (XDst (Op OS)
forall d. XStandardDst d => XDst d
xStandardDst :: XDst (Op OS))
      ]

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

-- prpStructureId -


prpStructureId :: Statement
prpStructureId :: Statement
prpStructureId = String -> Label
Prp String
"StructureId" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ XOrt (Id OS) -> Statement
forall q. Oriented q => XOrt q -> Statement
prpOrt (XOrt (Id OS)
forall x. XStandard x => X x
xStandard :: XOrt (Id OS))
      , XMlt (Id OS) -> Statement
forall c. Multiplicative c => XMlt c -> Statement
prpMlt (XMlt (Id OS)
forall c. XStandardMlt c => XMlt c
xStandardMlt :: XMlt (Id OS))
      , XOrt (Id OS) -> Statement
forall f. Fibred f => XFbr f -> Statement
prpFbr (XOrt (Id OS)
forall x. XStandard x => X x
xStandard :: XFbr (Id OS))
      , XOrt (Id OS) -> Statement
forall f. FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt (XOrt (Id OS)
forall x. XStandard x => X x
xStandard :: XFbrOrt (Id OS))
      , XAdd (Id OS) -> Statement
forall a. Additive a => XAdd a -> Statement
prpAdd (XAdd (Id OS)
forall a. XStandardAdd a => XAdd a
xStandardAdd :: XAdd (Id OS))
      , XDst (Id OS) -> Statement
forall d. Distributive d => XDst d -> Statement
prpDst (XDst (Id OS)
forall d. XStandardDst d => XDst d
xStandardDst :: XDst (Id OS))
      ]

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

-- prpStructure -


-- | validity of some structures.

prpStructure :: Statement
prpStructure :: Statement
prpStructure = String -> Label
Prp String
"Structure" Label -> Statement -> Statement
:<=>:
  [Statement] -> Statement
And [ Statement
prpLatticeBool
      , Statement
prpStructureN
      , Statement
prpStructureZ
      , Statement
prpStructureQ
      , Statement
prpStructureOS
      , Statement
prpStructureOp
      , Statement
prpStructureId
      ]