{-# 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
    prpStructureN, prpStructureZ, prpStructureQ
  , prpStructureOS
  )

  where

import OAlg.Prelude


import OAlg.Structure.Oriented
import OAlg.Structure.Multiplicative
import OAlg.Structure.Fibred
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 [ forall q. Oriented q => XOrt q -> Statement
prpOrt (forall x. XStandard x => X x
xStandard :: XOrt N)
      , forall c. Multiplicative c => XMlt c -> Statement
prpMlt (forall c. XStandardMlt c => XMlt c
xStandardMlt :: XMlt N)
      , forall f. Fibred f => XFbr f -> Statement
prpFbr (forall x. XStandard x => X x
xStandard :: XFbr N)
      , forall f. FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt (forall x. XStandard x => X x
xStandard :: XFbrOrt N)
      , forall a. Additive a => XAdd a -> Statement
prpAdd (forall a. XStandardAdd a => XAdd a
xStandardAdd :: XAdd N)
      , forall d. Distributive d => XDst d -> Statement
prpDst (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 [ forall q. Oriented q => XOrt q -> Statement
prpOrt (forall x. XStandard x => X x
xStandard :: XOrt Z)
      , forall c. Multiplicative c => XMlt c -> Statement
prpMlt (forall c. XStandardMlt c => XMlt c
xStandardMlt :: XMlt Z)
      , forall f. Fibred f => XFbr f -> Statement
prpFbr (forall x. XStandard x => X x
xStandard :: XFbr Z)
      , forall f. FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt (forall x. XStandard x => X x
xStandard :: XFbrOrt Z)
      , forall a. Additive a => XAdd a -> Statement
prpAdd (forall a. XStandardAdd a => XAdd a
xStandardAdd :: XAdd Z)
      , forall d. Distributive d => XDst d -> Statement
prpDst (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 [ forall q. Oriented q => XOrt q -> Statement
prpOrt (forall x. XStandard x => X x
xStandard :: XOrt Q)
      , forall c. Multiplicative c => XMlt c -> Statement
prpMlt (forall c. XStandardMlt c => XMlt c
xStandardMlt :: XMlt Q)
      , forall f. Fibred f => XFbr f -> Statement
prpFbr (forall x. XStandard x => X x
xStandard :: XFbr Q)
      , forall f. FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt (forall x. XStandard x => X x
xStandard :: XFbrOrt Q)
      , forall a. Additive a => XAdd a -> Statement
prpAdd (forall a. XStandardAdd a => XAdd a
xStandardAdd :: XAdd Q)
      , forall d. Distributive d => XDst d -> Statement
prpDst (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 [ forall q. Oriented q => XOrt q -> Statement
prpOrt (forall x. XStandard x => X x
xStandard :: XOrt OS)
      , forall c. Multiplicative c => XMlt c -> Statement
prpMlt (forall c. XStandardMlt c => XMlt c
xStandardMlt :: XMlt OS)
      , forall f. Fibred f => XFbr f -> Statement
prpFbr (forall x. XStandard x => X x
xStandard :: XFbr OS)
      , forall f. FibredOriented f => XFbrOrt f -> Statement
prpFbrOrt (forall x. XStandard x => X x
xStandard :: XFbrOrt OS)
      , forall a. Additive a => XAdd a -> Statement
prpAdd (forall a. XStandardAdd a => XAdd a
xStandardAdd :: XAdd OS)
      , forall d. Distributive d => XDst d -> Statement
prpDst (forall d. XStandardDst d => XDst d
xStandardDst :: XDst OS)
      ]