{-# LANGUAGE NoImplicitPrelude #-}
module OAlg.Proposition
( prpOAlgBase
) where
import OAlg.Prelude
import OAlg.Structure.Proposition
import OAlg.Hom.Proposition
import OAlg.Limes.Proposition
import OAlg.Entity.Product
import OAlg.Entity.Diagram.Proposition
import OAlg.Entity.Matrix
import OAlg.Entity.Sequence
prpOAlgBase :: Statement
prpOAlgBase :: Statement
prpOAlgBase = String -> Label
Prp String
"OAlgBase"
Label -> Statement -> Statement
:<=>: [Statement] -> Statement
And [ String -> Label
Label String
"logic" Label -> Statement -> Statement
:<=>:
[Statement] -> Statement
And [ Statement
prpBool
, Statement
prpValidTautologies
, Statement
prpStatement
]
, String -> Label
Label String
"Structure" Label -> Statement -> Statement
:<=>:
[Statement] -> Statement
And [ Statement
prpStructureN
, Statement
prpStructureZ
, Statement
prpStructureQ
, Statement
prpStructureOS
]
, String -> Label
Label String
"Hom" Label -> Statement -> Statement
:<=>:
[Statement] -> Statement
And [ Statement
prpIdHom
, Statement
prpHomOp
, Statement
prpIsoOpOrt
]
, String -> Label
Label String
"Product" Label -> Statement -> Statement
:<=>: Statement
prpOrtProductZOrntSymbol
, String -> Label
Label String
"Diagram" Label -> Statement -> Statement
:<=>: Statement
prpDiagramOrntSymbol
, String -> Label
Label String
"Limes" Label -> Statement -> Statement
:<=>: Statement
prpLimitsOrntSymbol
, String -> Label
Label String
"Permutation" Label -> Statement -> Statement
:<=>: Statement
prpPermutation
, String -> Label
Label String
"Matrix" Label -> Statement -> Statement
:<=>: Statement
prpMatrixZ
, String -> Label
Label String
"Vector" Label -> Statement -> Statement
:<=>: N -> N -> Statement
prpRepMatrixZ N
8 N
15
]