module UVMHS.Lib.MMSP where

import UVMHS.Core

import UVMHS.Lib.Variables
import UVMHS.Lib.Parser
import UVMHS.Lib.Annotated
-- import UVMHS.Lib.Substitution

-- MMSP ≈
-- c ⊔ (c ⊓ (c + c(xᶜ…xᶜ) 
--   ⋮    ⋮    ⋮ 
--   ⋮    ⋮    + c(xᵈ…xᵈ)) 
--   ⋮    ⋮ 
--   ⋮    ⊓ (c + c(xᶜ…xᶜ) 
--   ⋮         ⋮ 
--   ⋮         + c(xᵈ…xᵈ))
--   ⊔ (c ⊓ (c + c(xᶜ…xᶜ) 
--        ⋮    ⋮ 
--        ⋮    + c(xᵈ…xᵈ)) 
--        ⋮ 
--        ⊓ (c + c(xᶜ…xᶜ) 
--             ⋮ 
--             + c(xᵈ…xᵈ))

newtype MMSP = MMSP
  { MMSP -> MMSPMaxs
mmspMaxs ∷ MMSPMaxs
  } 
  deriving (MMSP -> MMSP -> Bool
(MMSP -> MMSP -> Bool) -> (MMSP -> MMSP -> Bool) -> Eq MMSP
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MMSP -> MMSP -> Bool
== :: MMSP -> MMSP -> Bool
$c/= :: MMSP -> MMSP -> Bool
/= :: MMSP -> MMSP -> Bool
Eq,Eq MMSP
Eq MMSP =>
(MMSP -> MMSP -> Ordering)
-> (MMSP -> MMSP -> Bool)
-> (MMSP -> MMSP -> Bool)
-> (MMSP -> MMSP -> Bool)
-> (MMSP -> MMSP -> Bool)
-> (MMSP -> MMSP -> MMSP)
-> (MMSP -> MMSP -> MMSP)
-> Ord MMSP
MMSP -> MMSP -> Bool
MMSP -> MMSP -> Ordering
MMSP -> MMSP -> MMSP
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: MMSP -> MMSP -> Ordering
compare :: MMSP -> MMSP -> Ordering
$c< :: MMSP -> MMSP -> Bool
< :: MMSP -> MMSP -> Bool
$c<= :: MMSP -> MMSP -> Bool
<= :: MMSP -> MMSP -> Bool
$c> :: MMSP -> MMSP -> Bool
> :: MMSP -> MMSP -> Bool
$c>= :: MMSP -> MMSP -> Bool
>= :: MMSP -> MMSP -> Bool
$cmax :: MMSP -> MMSP -> MMSP
max :: MMSP -> MMSP -> MMSP
$cmin :: MMSP -> MMSP -> MMSP
min :: MMSP -> MMSP -> MMSP
Ord,Int -> MMSP -> ShowS
[MMSP] -> ShowS
MMSP -> String
(Int -> MMSP -> ShowS)
-> (MMSP -> String) -> ([MMSP] -> ShowS) -> Show MMSP
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MMSP -> ShowS
showsPrec :: Int -> MMSP -> ShowS
$cshow :: MMSP -> String
show :: MMSP -> String
$cshowList :: [MMSP] -> ShowS
showList :: [MMSP] -> ShowS
Show)

data MMSPMaxs = MMSPMaxs
  { MMSPMaxs -> ℕ
mmspMaxsConstant    ∷ ℕ
  , MMSPMaxs -> 𝑃 MMSPMins
mmspMaxsMins        ∷ 𝑃 MMSPMins
  }
  deriving (MMSPMaxs -> MMSPMaxs -> Bool
(MMSPMaxs -> MMSPMaxs -> Bool)
-> (MMSPMaxs -> MMSPMaxs -> Bool) -> Eq MMSPMaxs
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MMSPMaxs -> MMSPMaxs -> Bool
== :: MMSPMaxs -> MMSPMaxs -> Bool
$c/= :: MMSPMaxs -> MMSPMaxs -> Bool
/= :: MMSPMaxs -> MMSPMaxs -> Bool
Eq,Eq MMSPMaxs
Eq MMSPMaxs =>
(MMSPMaxs -> MMSPMaxs -> Ordering)
-> (MMSPMaxs -> MMSPMaxs -> Bool)
-> (MMSPMaxs -> MMSPMaxs -> Bool)
-> (MMSPMaxs -> MMSPMaxs -> Bool)
-> (MMSPMaxs -> MMSPMaxs -> Bool)
-> (MMSPMaxs -> MMSPMaxs -> MMSPMaxs)
-> (MMSPMaxs -> MMSPMaxs -> MMSPMaxs)
-> Ord MMSPMaxs
MMSPMaxs -> MMSPMaxs -> Bool
MMSPMaxs -> MMSPMaxs -> Ordering
MMSPMaxs -> MMSPMaxs -> MMSPMaxs
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: MMSPMaxs -> MMSPMaxs -> Ordering
compare :: MMSPMaxs -> MMSPMaxs -> Ordering
$c< :: MMSPMaxs -> MMSPMaxs -> Bool
< :: MMSPMaxs -> MMSPMaxs -> Bool
$c<= :: MMSPMaxs -> MMSPMaxs -> Bool
<= :: MMSPMaxs -> MMSPMaxs -> Bool
$c> :: MMSPMaxs -> MMSPMaxs -> Bool
> :: MMSPMaxs -> MMSPMaxs -> Bool
$c>= :: MMSPMaxs -> MMSPMaxs -> Bool
>= :: MMSPMaxs -> MMSPMaxs -> Bool
$cmax :: MMSPMaxs -> MMSPMaxs -> MMSPMaxs
max :: MMSPMaxs -> MMSPMaxs -> MMSPMaxs
$cmin :: MMSPMaxs -> MMSPMaxs -> MMSPMaxs
min :: MMSPMaxs -> MMSPMaxs -> MMSPMaxs
Ord,Int -> MMSPMaxs -> ShowS
[MMSPMaxs] -> ShowS
MMSPMaxs -> String
(Int -> MMSPMaxs -> ShowS)
-> (MMSPMaxs -> String) -> ([MMSPMaxs] -> ShowS) -> Show MMSPMaxs
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MMSPMaxs -> ShowS
showsPrec :: Int -> MMSPMaxs -> ShowS
$cshow :: MMSPMaxs -> String
show :: MMSPMaxs -> String
$cshowList :: [MMSPMaxs] -> ShowS
showList :: [MMSPMaxs] -> ShowS
Show)

data MMSPMins = MMSPMins
  { MMSPMins -> AddTop ℕ
mmspMinsConstant    ∷ AddTop ℕ   -- non-zero
  , MMSPMins -> 𝑃 MMSPSums
mmspMinsSums        ∷ 𝑃 MMSPSums -- at least one
  }
  deriving (MMSPMins -> MMSPMins -> Bool
(MMSPMins -> MMSPMins -> Bool)
-> (MMSPMins -> MMSPMins -> Bool) -> Eq MMSPMins
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MMSPMins -> MMSPMins -> Bool
== :: MMSPMins -> MMSPMins -> Bool
$c/= :: MMSPMins -> MMSPMins -> Bool
/= :: MMSPMins -> MMSPMins -> Bool
Eq,Eq MMSPMins
Eq MMSPMins =>
(MMSPMins -> MMSPMins -> Ordering)
-> (MMSPMins -> MMSPMins -> Bool)
-> (MMSPMins -> MMSPMins -> Bool)
-> (MMSPMins -> MMSPMins -> Bool)
-> (MMSPMins -> MMSPMins -> Bool)
-> (MMSPMins -> MMSPMins -> MMSPMins)
-> (MMSPMins -> MMSPMins -> MMSPMins)
-> Ord MMSPMins
MMSPMins -> MMSPMins -> Bool
MMSPMins -> MMSPMins -> Ordering
MMSPMins -> MMSPMins -> MMSPMins
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: MMSPMins -> MMSPMins -> Ordering
compare :: MMSPMins -> MMSPMins -> Ordering
$c< :: MMSPMins -> MMSPMins -> Bool
< :: MMSPMins -> MMSPMins -> Bool
$c<= :: MMSPMins -> MMSPMins -> Bool
<= :: MMSPMins -> MMSPMins -> Bool
$c> :: MMSPMins -> MMSPMins -> Bool
> :: MMSPMins -> MMSPMins -> Bool
$c>= :: MMSPMins -> MMSPMins -> Bool
>= :: MMSPMins -> MMSPMins -> Bool
$cmax :: MMSPMins -> MMSPMins -> MMSPMins
max :: MMSPMins -> MMSPMins -> MMSPMins
$cmin :: MMSPMins -> MMSPMins -> MMSPMins
min :: MMSPMins -> MMSPMins -> MMSPMins
Ord,Int -> MMSPMins -> ShowS
[MMSPMins] -> ShowS
MMSPMins -> String
(Int -> MMSPMins -> ShowS)
-> (MMSPMins -> String) -> ([MMSPMins] -> ShowS) -> Show MMSPMins
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MMSPMins -> ShowS
showsPrec :: Int -> MMSPMins -> ShowS
$cshow :: MMSPMins -> String
show :: MMSPMins -> String
$cshowList :: [MMSPMins] -> ShowS
showList :: [MMSPMins] -> ShowS
Show)

data MMSPSums = MMSPSums
  { MMSPSums -> ℕ
mmspSumsConstant    ∷ ℕ
  , MMSPSums -> MMSPProds ⇰ ℕ
mmspSumsPRods       ∷ MMSPProds ⇰ ℕ -- at least one
  }
  deriving (MMSPSums -> MMSPSums -> Bool
(MMSPSums -> MMSPSums -> Bool)
-> (MMSPSums -> MMSPSums -> Bool) -> Eq MMSPSums
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MMSPSums -> MMSPSums -> Bool
== :: MMSPSums -> MMSPSums -> Bool
$c/= :: MMSPSums -> MMSPSums -> Bool
/= :: MMSPSums -> MMSPSums -> Bool
Eq,Eq MMSPSums
Eq MMSPSums =>
(MMSPSums -> MMSPSums -> Ordering)
-> (MMSPSums -> MMSPSums -> Bool)
-> (MMSPSums -> MMSPSums -> Bool)
-> (MMSPSums -> MMSPSums -> Bool)
-> (MMSPSums -> MMSPSums -> Bool)
-> (MMSPSums -> MMSPSums -> MMSPSums)
-> (MMSPSums -> MMSPSums -> MMSPSums)
-> Ord MMSPSums
MMSPSums -> MMSPSums -> Bool
MMSPSums -> MMSPSums -> Ordering
MMSPSums -> MMSPSums -> MMSPSums
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: MMSPSums -> MMSPSums -> Ordering
compare :: MMSPSums -> MMSPSums -> Ordering
$c< :: MMSPSums -> MMSPSums -> Bool
< :: MMSPSums -> MMSPSums -> Bool
$c<= :: MMSPSums -> MMSPSums -> Bool
<= :: MMSPSums -> MMSPSums -> Bool
$c> :: MMSPSums -> MMSPSums -> Bool
> :: MMSPSums -> MMSPSums -> Bool
$c>= :: MMSPSums -> MMSPSums -> Bool
>= :: MMSPSums -> MMSPSums -> Bool
$cmax :: MMSPSums -> MMSPSums -> MMSPSums
max :: MMSPSums -> MMSPSums -> MMSPSums
$cmin :: MMSPSums -> MMSPSums -> MMSPSums
min :: MMSPSums -> MMSPSums -> MMSPSums
Ord,Int -> MMSPSums -> ShowS
[MMSPSums] -> ShowS
MMSPSums -> String
(Int -> MMSPSums -> ShowS)
-> (MMSPSums -> String) -> ([MMSPSums] -> ShowS) -> Show MMSPSums
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MMSPSums -> ShowS
showsPrec :: Int -> MMSPSums -> ShowS
$cshow :: MMSPSums -> String
show :: MMSPSums -> String
$cshowList :: [MMSPSums] -> ShowS
showList :: [MMSPSums] -> ShowS
Show)

data MMSPProds = MMSPProds
  { MMSPProds -> MMSPAtom ⇰ ℕ
mmspProdsExps        ∷ MMSPAtom ⇰ ℕ -- at least one
  }
  deriving (MMSPProds -> MMSPProds -> Bool
(MMSPProds -> MMSPProds -> Bool)
-> (MMSPProds -> MMSPProds -> Bool) -> Eq MMSPProds
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MMSPProds -> MMSPProds -> Bool
== :: MMSPProds -> MMSPProds -> Bool
$c/= :: MMSPProds -> MMSPProds -> Bool
/= :: MMSPProds -> MMSPProds -> Bool
Eq,Eq MMSPProds
Eq MMSPProds =>
(MMSPProds -> MMSPProds -> Ordering)
-> (MMSPProds -> MMSPProds -> Bool)
-> (MMSPProds -> MMSPProds -> Bool)
-> (MMSPProds -> MMSPProds -> Bool)
-> (MMSPProds -> MMSPProds -> Bool)
-> (MMSPProds -> MMSPProds -> MMSPProds)
-> (MMSPProds -> MMSPProds -> MMSPProds)
-> Ord MMSPProds
MMSPProds -> MMSPProds -> Bool
MMSPProds -> MMSPProds -> Ordering
MMSPProds -> MMSPProds -> MMSPProds
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: MMSPProds -> MMSPProds -> Ordering
compare :: MMSPProds -> MMSPProds -> Ordering
$c< :: MMSPProds -> MMSPProds -> Bool
< :: MMSPProds -> MMSPProds -> Bool
$c<= :: MMSPProds -> MMSPProds -> Bool
<= :: MMSPProds -> MMSPProds -> Bool
$c> :: MMSPProds -> MMSPProds -> Bool
> :: MMSPProds -> MMSPProds -> Bool
$c>= :: MMSPProds -> MMSPProds -> Bool
>= :: MMSPProds -> MMSPProds -> Bool
$cmax :: MMSPProds -> MMSPProds -> MMSPProds
max :: MMSPProds -> MMSPProds -> MMSPProds
$cmin :: MMSPProds -> MMSPProds -> MMSPProds
min :: MMSPProds -> MMSPProds -> MMSPProds
Ord,Int -> MMSPProds -> ShowS
[MMSPProds] -> ShowS
MMSPProds -> String
(Int -> MMSPProds -> ShowS)
-> (MMSPProds -> String)
-> ([MMSPProds] -> ShowS)
-> Show MMSPProds
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MMSPProds -> ShowS
showsPrec :: Int -> MMSPProds -> ShowS
$cshow :: MMSPProds -> String
show :: MMSPProds -> String
$cshowList :: [MMSPProds] -> ShowS
showList :: [MMSPProds] -> ShowS
Show)

data MMSPAtom = 
    Var_MMSPAtom (𝐴 (𝑃 SrcCxt) 𝕏)
  deriving (MMSPAtom -> MMSPAtom -> Bool
(MMSPAtom -> MMSPAtom -> Bool)
-> (MMSPAtom -> MMSPAtom -> Bool) -> Eq MMSPAtom
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MMSPAtom -> MMSPAtom -> Bool
== :: MMSPAtom -> MMSPAtom -> Bool
$c/= :: MMSPAtom -> MMSPAtom -> Bool
/= :: MMSPAtom -> MMSPAtom -> Bool
Eq,Eq MMSPAtom
Eq MMSPAtom =>
(MMSPAtom -> MMSPAtom -> Ordering)
-> (MMSPAtom -> MMSPAtom -> Bool)
-> (MMSPAtom -> MMSPAtom -> Bool)
-> (MMSPAtom -> MMSPAtom -> Bool)
-> (MMSPAtom -> MMSPAtom -> Bool)
-> (MMSPAtom -> MMSPAtom -> MMSPAtom)
-> (MMSPAtom -> MMSPAtom -> MMSPAtom)
-> Ord MMSPAtom
MMSPAtom -> MMSPAtom -> Bool
MMSPAtom -> MMSPAtom -> Ordering
MMSPAtom -> MMSPAtom -> MMSPAtom
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: MMSPAtom -> MMSPAtom -> Ordering
compare :: MMSPAtom -> MMSPAtom -> Ordering
$c< :: MMSPAtom -> MMSPAtom -> Bool
< :: MMSPAtom -> MMSPAtom -> Bool
$c<= :: MMSPAtom -> MMSPAtom -> Bool
<= :: MMSPAtom -> MMSPAtom -> Bool
$c> :: MMSPAtom -> MMSPAtom -> Bool
> :: MMSPAtom -> MMSPAtom -> Bool
$c>= :: MMSPAtom -> MMSPAtom -> Bool
>= :: MMSPAtom -> MMSPAtom -> Bool
$cmax :: MMSPAtom -> MMSPAtom -> MMSPAtom
max :: MMSPAtom -> MMSPAtom -> MMSPAtom
$cmin :: MMSPAtom -> MMSPAtom -> MMSPAtom
min :: MMSPAtom -> MMSPAtom -> MMSPAtom
Ord,Int -> MMSPAtom -> ShowS
[MMSPAtom] -> ShowS
MMSPAtom -> String
(Int -> MMSPAtom -> ShowS)
-> (MMSPAtom -> String) -> ([MMSPAtom] -> ShowS) -> Show MMSPAtom
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MMSPAtom -> ShowS
showsPrec :: Int -> MMSPAtom -> ShowS
$cshow :: MMSPAtom -> String
show :: MMSPAtom -> String
$cshowList :: [MMSPAtom] -> ShowS
showList :: [MMSPAtom] -> ShowS
Show)
makePrisms ''MMSPAtom

----------
-- MMSP --
----------

----------------
-- OPERATIONS --
----------------

instance Zero  MMSP where zero :: MMSP
zero = ℕ -> MMSP
litMMSP ℕ
forall a. Zero a => a
zero
instance One   MMSP where one :: MMSP
one  = ℕ -> MMSP
litMMSP ℕ
forall a. One a => a
one
instance Plus  MMSP where + :: MMSP -> MMSP -> MMSP
(+)  = MMSP -> MMSP -> MMSP
plusMMSP
instance Times MMSP where × :: MMSP -> MMSP -> MMSP
(×)  = MMSP -> MMSP -> MMSP
timesMMSP
instance Pon   MMSP where ^^ :: MMSP -> ℕ -> MMSP
(^^) = MMSP -> ℕ -> MMSP
ponMMSP
instance Bot   MMSP where bot :: MMSP
bot  = ℕ -> MMSP
litMMSP ℕ
forall a. Zero a => a
zero
instance Join  MMSP where ⊔ :: MMSP -> MMSP -> MMSP
(⊔)  = MMSP -> MMSP -> MMSP
joinMMSP
instance Top   MMSP where top :: MMSP
top  = MMSP
topMMSP
instance Meet  MMSP where ⊓ :: MMSP -> MMSP -> MMSP
(⊓)  = MMSP -> MMSP -> MMSP
meetMMSP

instance Additive       MMSP
instance Multiplicative MMSP
instance JoinLattice    MMSP
instance MeetLattice    MMSP

maxsMMSPL ∷ MMSP ⌲ MMSPMaxs
maxsMMSPL :: MMSP ⌲ MMSPMaxs
maxsMMSPL = (MMSPMaxs -> MMSP) -> (MMSP -> 𝑂 MMSPMaxs) -> MMSP ⌲ MMSPMaxs
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism MMSPMaxs -> MMSP
MMSP ((MMSP -> 𝑂 MMSPMaxs) -> MMSP ⌲ MMSPMaxs)
-> (MMSP -> 𝑂 MMSPMaxs) -> MMSP ⌲ MMSPMaxs
forall a b. (a -> b) -> a -> b
$ MMSPMaxs -> 𝑂 MMSPMaxs
forall a. a -> 𝑂 a
Some (MMSPMaxs -> 𝑂 MMSPMaxs)
-> (MMSP -> MMSPMaxs) -> MMSP -> 𝑂 MMSPMaxs
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ MMSP -> MMSPMaxs
mmspMaxs

minsMMSPL ∷ MMSP ⌲ MMSPMins
minsMMSPL :: MMSP ⌲ MMSPMins
minsMMSPL  = 
  let mk :: MMSPMins -> MMSPMaxs
mk MMSPMins
β̇ = ℕ -> 𝑃 MMSPMins -> MMSPMaxs
MMSPMaxs ℕ
forall a. Zero a => a
zero (𝑃 MMSPMins -> MMSPMaxs) -> 𝑃 MMSPMins -> MMSPMaxs
forall a b. (a -> b) -> a -> b
$ MMSPMins -> 𝑃 MMSPMins
forall a t. Single a t => a -> t
single MMSPMins
β̇
      vw :: MMSPMaxs -> 𝑂 MMSPMins
vw = \case
        MMSPMaxs ℕ
a 𝑃 MMSPMins
α | ℕ
a ℕ -> ℕ -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ
forall a. Zero a => a
zero,Some MMSPMins
β̇ ← (𝑃 MMSPMins ⌲ MMSPMins) -> 𝑃 MMSPMins -> 𝑂 MMSPMins
forall a b. (a ⌲ b) -> a -> 𝑂 b
view 𝑃 MMSPMins ⌲ MMSPMins
forall a. Ord a => 𝑃 a ⌲ a
single𝑃L 𝑃 MMSPMins
α → MMSPMins -> 𝑂 MMSPMins
forall a. a -> 𝑂 a
Some MMSPMins
β̇
        MMSPMaxs
_ → 𝑂 MMSPMins
forall a. 𝑂 a
None
  in (MMSPMins -> MMSPMaxs)
-> (MMSPMaxs -> 𝑂 MMSPMins) -> MMSPMaxs ⌲ MMSPMins
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism MMSPMins -> MMSPMaxs
mk MMSPMaxs -> 𝑂 MMSPMins
vw (MMSPMaxs ⌲ MMSPMins) -> (MMSP ⌲ MMSPMaxs) -> MMSP ⌲ MMSPMins
forall b c a. (b ⌲ c) -> (a ⌲ b) -> a ⌲ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ MMSP ⌲ MMSPMaxs
maxsMMSPL

sumsMMSPL ∷ MMSP ⌲ MMSPSums
sumsMMSPL :: MMSP ⌲ MMSPSums
sumsMMSPL = 
  let mk :: MMSPSums -> MMSPMins
mk MMSPSums
γ̇ = AddTop ℕ -> 𝑃 MMSPSums -> MMSPMins
MMSPMins AddTop ℕ
forall a. AddTop a
Top (𝑃 MMSPSums -> MMSPMins) -> 𝑃 MMSPSums -> MMSPMins
forall a b. (a -> b) -> a -> b
$ MMSPSums -> 𝑃 MMSPSums
forall a t. Single a t => a -> t
single (MMSPSums -> 𝑃 MMSPSums) -> MMSPSums -> 𝑃 MMSPSums
forall a b. (a -> b) -> a -> b
$ MMSPSums
γ̇
      vw :: MMSPMins -> 𝑂 MMSPSums
vw = \case
        MMSPMins AddTop ℕ
b 𝑃 MMSPSums
β | AddTop ℕ
b AddTop ℕ -> AddTop ℕ -> Bool
forall a. Eq a => a -> a -> Bool
≡ AddTop ℕ
forall a. AddTop a
Top,Some MMSPSums
γ̇ ← (𝑃 MMSPSums ⌲ MMSPSums) -> 𝑃 MMSPSums -> 𝑂 MMSPSums
forall a b. (a ⌲ b) -> a -> 𝑂 b
view 𝑃 MMSPSums ⌲ MMSPSums
forall a. Ord a => 𝑃 a ⌲ a
single𝑃L 𝑃 MMSPSums
β → MMSPSums -> 𝑂 MMSPSums
forall a. a -> 𝑂 a
Some MMSPSums
γ̇
        MMSPMins
_ → 𝑂 MMSPSums
forall a. 𝑂 a
None
  in (MMSPSums -> MMSPMins)
-> (MMSPMins -> 𝑂 MMSPSums) -> MMSPMins ⌲ MMSPSums
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism MMSPSums -> MMSPMins
mk MMSPMins -> 𝑂 MMSPSums
vw (MMSPMins ⌲ MMSPSums) -> (MMSP ⌲ MMSPMins) -> MMSP ⌲ MMSPSums
forall b c a. (b ⌲ c) -> (a ⌲ b) -> a ⌲ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ MMSP ⌲ MMSPMins
minsMMSPL

prodsMMSPL ∷ MMSP ⌲ MMSPProds
prodsMMSPL :: MMSP ⌲ MMSPProds
prodsMMSPL = 
  let mk :: MMSPProds -> MMSPSums
mk MMSPProds
δ̇ = ℕ -> (MMSPProds ⇰ ℕ) -> MMSPSums
MMSPSums ℕ
forall a. Zero a => a
zero ((MMSPProds ⇰ ℕ) -> MMSPSums) -> (MMSPProds ⇰ ℕ) -> MMSPSums
forall a b. (a -> b) -> a -> b
$ MMSPProds
δ̇ MMSPProds -> ℕ -> MMSPProds ⇰ ℕ
forall k a. k -> a -> k ⇰ a
↦♭ ℕ
forall a. One a => a
one
      vw :: MMSPSums -> 𝑂 MMSPProds
vw = \case
        MMSPSums ℕ
c MMSPProds ⇰ ℕ
γ | ℕ
c ℕ -> ℕ -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ
forall a. Zero a => a
zero,Some (MMSPProds
δ̇ :* ℕ
d) ← ((MMSPProds ⇰ ℕ) ⌲ (MMSPProds ∧ ℕ))
-> (MMSPProds ⇰ ℕ) -> 𝑂 (MMSPProds ∧ ℕ)
forall a b. (a ⌲ b) -> a -> 𝑂 b
view (MMSPProds ⇰ ℕ) ⌲ (MMSPProds ∧ ℕ)
forall k v. Ord k => (k ⇰ v) ⌲ (k ∧ v)
single𝐷L MMSPProds ⇰ ℕ
γ,ℕ
d ℕ -> ℕ -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ
forall a. One a => a
one → MMSPProds -> 𝑂 MMSPProds
forall a. a -> 𝑂 a
Some MMSPProds
δ̇
        MMSPSums
_ → 𝑂 MMSPProds
forall a. 𝑂 a
None
  in (MMSPProds -> MMSPSums)
-> (MMSPSums -> 𝑂 MMSPProds) -> MMSPSums ⌲ MMSPProds
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism MMSPProds -> MMSPSums
mk MMSPSums -> 𝑂 MMSPProds
vw (MMSPSums ⌲ MMSPProds) -> (MMSP ⌲ MMSPSums) -> MMSP ⌲ MMSPProds
forall b c a. (b ⌲ c) -> (a ⌲ b) -> a ⌲ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ MMSP ⌲ MMSPSums
sumsMMSPL

atomMMSPL ∷ MMSP ⌲ MMSPAtom
atomMMSPL :: MMSP ⌲ MMSPAtom
atomMMSPL =
  let mk :: MMSPAtom -> MMSPProds
mk MMSPAtom
ω = (MMSPAtom ⇰ ℕ) -> MMSPProds
MMSPProds ((MMSPAtom ⇰ ℕ) -> MMSPProds) -> (MMSPAtom ⇰ ℕ) -> MMSPProds
forall a b. (a -> b) -> a -> b
$ MMSPAtom
ω MMSPAtom -> ℕ -> MMSPAtom ⇰ ℕ
forall k a. k -> a -> k ⇰ a
↦♭ ℕ
forall a. One a => a
one
      vw :: MMSPProds -> 𝑂 MMSPAtom
vw = \case
        MMSPProds MMSPAtom ⇰ ℕ
δ | Some (MMSPAtom
ω :* ℕ
e) ← ((MMSPAtom ⇰ ℕ) ⌲ (MMSPAtom ∧ ℕ))
-> (MMSPAtom ⇰ ℕ) -> 𝑂 (MMSPAtom ∧ ℕ)
forall a b. (a ⌲ b) -> a -> 𝑂 b
view (MMSPAtom ⇰ ℕ) ⌲ (MMSPAtom ∧ ℕ)
forall k v. Ord k => (k ⇰ v) ⌲ (k ∧ v)
single𝐷L MMSPAtom ⇰ ℕ
δ,ℕ
e ℕ -> ℕ -> Bool
forall a. Eq a => a -> a -> Bool
≡ ℕ
forall a. One a => a
one → MMSPAtom -> 𝑂 MMSPAtom
forall a. a -> 𝑂 a
Some MMSPAtom
ω
        MMSPProds
_ → 𝑂 MMSPAtom
forall a. 𝑂 a
None
  in (MMSPAtom -> MMSPProds)
-> (MMSPProds -> 𝑂 MMSPAtom) -> MMSPProds ⌲ MMSPAtom
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism MMSPAtom -> MMSPProds
mk MMSPProds -> 𝑂 MMSPAtom
vw (MMSPProds ⌲ MMSPAtom) -> (MMSP ⌲ MMSPProds) -> MMSP ⌲ MMSPAtom
forall b c a. (b ⌲ c) -> (a ⌲ b) -> a ⌲ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ MMSP ⌲ MMSPProds
prodsMMSPL

varMMSPL ∷ MMSP ⌲ 𝐴 (𝑃 SrcCxt) 𝕏
varMMSPL :: MMSP ⌲ 𝐴 (𝑃 SrcCxt) 𝕏
varMMSPL = MMSPAtom ⌲ 𝐴 (𝑃 SrcCxt) 𝕏
var_MMSPAtomL (MMSPAtom ⌲ 𝐴 (𝑃 SrcCxt) 𝕏)
-> (MMSP ⌲ MMSPAtom) -> MMSP ⌲ 𝐴 (𝑃 SrcCxt) 𝕏
forall b c a. (b ⌲ c) -> (a ⌲ b) -> a ⌲ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ MMSP ⌲ MMSPAtom
atomMMSPL

litMMSPL ∷ MMSP ⌲ ℕ
litMMSPL :: MMSP ⌲ ℕ
litMMSPL = 
  let mk :: ℕ -> MMSPMaxs
mk ℕ
n = ℕ -> 𝑃 MMSPMins -> MMSPMaxs
MMSPMaxs ℕ
n 𝑃 MMSPMins
forall a. Null a => a
null
      vw :: MMSPMaxs -> 𝑂 ℕ
vw = \case
        MMSPMaxs ℕ
a 𝑃 MMSPMins
α | 𝑃 MMSPMins -> Bool
forall a t. ToIter a t => t -> Bool
isEmpty 𝑃 MMSPMins
α → ℕ -> 𝑂 ℕ
forall a. a -> 𝑂 a
Some ℕ
a
        MMSPMaxs
_ → 𝑂 ℕ
forall a. 𝑂 a
None
  in (ℕ -> MMSPMaxs) -> (MMSPMaxs -> 𝑂 ℕ) -> MMSPMaxs ⌲ ℕ
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism ℕ -> MMSPMaxs
mk MMSPMaxs -> 𝑂 ℕ
vw (MMSPMaxs ⌲ ℕ) -> (MMSP ⌲ MMSPMaxs) -> MMSP ⌲ ℕ
forall b c a. (b ⌲ c) -> (a ⌲ b) -> a ⌲ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ MMSP ⌲ MMSPMaxs
maxsMMSPL

topMMSPL ∷ MMSP ⌲ ()
topMMSPL :: MMSP ⌲ ()
topMMSPL = 
  let mk :: () -> MMSPMins
mk () = AddTop ℕ -> 𝑃 MMSPSums -> MMSPMins
MMSPMins AddTop ℕ
forall a. AddTop a
Top 𝑃 MMSPSums
forall a. Null a => a
null
      vw :: MMSPMins -> 𝑂 ()
vw = \case
        MMSPMins AddTop ℕ
b 𝑃 MMSPSums
β | AddTop ℕ
b AddTop ℕ -> AddTop ℕ -> Bool
forall a. Eq a => a -> a -> Bool
≡ AddTop ℕ
forall a. AddTop a
Top,𝑃 MMSPSums -> Bool
forall a t. ToIter a t => t -> Bool
isEmpty 𝑃 MMSPSums
β → () -> 𝑂 ()
forall a. a -> 𝑂 a
Some ()
        MMSPMins
_ → 𝑂 ()
forall a. 𝑂 a
None
  in (() -> MMSPMins) -> (MMSPMins -> 𝑂 ()) -> MMSPMins ⌲ ()
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism () -> MMSPMins
mk MMSPMins -> 𝑂 ()
vw (MMSPMins ⌲ ()) -> (MMSP ⌲ MMSPMins) -> MMSP ⌲ ()
forall b c a. (b ⌲ c) -> (a ⌲ b) -> a ⌲ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ MMSP ⌲ MMSPMins
minsMMSPL

littMMSPL ∷ MMSP ⌲ AddTop ℕ
littMMSPL :: MMSP ⌲ AddTop ℕ
littMMSPL =
  let mk :: AddTop ℕ -> MMSP
mk = \case
        AddTop ℕ
n → ℕ -> MMSP
litMMSP ℕ
n
        AddTop ℕ
Top → MMSP
topMMSP
      vw :: MMSP -> 𝑂 (AddTop ℕ)
vw MMSP
η 
        | Some ℕ
n ← (MMSP ⌲ ℕ) -> MMSP -> 𝑂 ℕ
forall a b. (a ⌲ b) -> a -> 𝑂 b
view MMSP ⌲ ℕ
litMMSPL MMSP
η = AddTop ℕ -> 𝑂 (AddTop ℕ)
forall a. a -> 𝑂 a
Some (AddTop ℕ -> 𝑂 (AddTop ℕ)) -> AddTop ℕ -> 𝑂 (AddTop ℕ)
forall a b. (a -> b) -> a -> b
$ ℕ -> AddTop ℕ
forall a. a -> AddTop a
AddTop ℕ
n
        | Some () ← (MMSP ⌲ ()) -> MMSP -> 𝑂 ()
forall a b. (a ⌲ b) -> a -> 𝑂 b
view MMSP ⌲ ()
topMMSPL MMSP
η = AddTop ℕ -> 𝑂 (AddTop ℕ)
forall a. a -> 𝑂 a
Some AddTop ℕ
forall a. AddTop a
Top
        | Bool
otherwise = 𝑂 (AddTop ℕ)
forall a. 𝑂 a
None
  in (AddTop ℕ -> MMSP) -> (MMSP -> 𝑂 (AddTop ℕ)) -> MMSP ⌲ AddTop ℕ
forall b a. (b -> a) -> (a -> 𝑂 b) -> a ⌲ b
prism AddTop ℕ -> MMSP
mk MMSP -> 𝑂 (AddTop ℕ)
vw

maxsMMSP ∷ MMSPMaxs → MMSP
maxsMMSP :: MMSPMaxs -> MMSP
maxsMMSP = (MMSP ⌲ MMSPMaxs) -> MMSPMaxs -> MMSP
forall a b. (a ⌲ b) -> b -> a
construct MMSP ⌲ MMSPMaxs
maxsMMSPL

minsMMSP ∷ MMSPMins → MMSP
minsMMSP :: MMSPMins -> MMSP
minsMMSP = (MMSP ⌲ MMSPMins) -> MMSPMins -> MMSP
forall a b. (a ⌲ b) -> b -> a
construct MMSP ⌲ MMSPMins
minsMMSPL

sumsMMSP ∷ MMSPSums → MMSP
sumsMMSP :: MMSPSums -> MMSP
sumsMMSP = (MMSP ⌲ MMSPSums) -> MMSPSums -> MMSP
forall a b. (a ⌲ b) -> b -> a
construct MMSP ⌲ MMSPSums
sumsMMSPL

prodsMMSP ∷ MMSPProds → MMSP
prodsMMSP :: MMSPProds -> MMSP
prodsMMSP = (MMSP ⌲ MMSPProds) -> MMSPProds -> MMSP
forall a b. (a ⌲ b) -> b -> a
construct MMSP ⌲ MMSPProds
prodsMMSPL

atomMMSP ∷ MMSPAtom → MMSP
atomMMSP :: MMSPAtom -> MMSP
atomMMSP = (MMSP ⌲ MMSPAtom) -> MMSPAtom -> MMSP
forall a b. (a ⌲ b) -> b -> a
construct MMSP ⌲ MMSPAtom
atomMMSPL

varMMSP ∷ 𝐴 (𝑃 SrcCxt) 𝕏 → MMSP
varMMSP :: 𝐴 (𝑃 SrcCxt) 𝕏 -> MMSP
varMMSP = (MMSP ⌲ 𝐴 (𝑃 SrcCxt) 𝕏) -> 𝐴 (𝑃 SrcCxt) 𝕏 -> MMSP
forall a b. (a ⌲ b) -> b -> a
construct MMSP ⌲ 𝐴 (𝑃 SrcCxt) 𝕏
varMMSPL

litMMSP ∷ ℕ → MMSP
litMMSP :: ℕ -> MMSP
litMMSP = (MMSP ⌲ ℕ) -> ℕ -> MMSP
forall a b. (a ⌲ b) -> b -> a
construct MMSP ⌲ ℕ
litMMSPL

topMMSP ∷ MMSP
topMMSP :: MMSP
topMMSP = (MMSP ⌲ ()) -> () -> MMSP
forall a b. (a ⌲ b) -> b -> a
construct MMSP ⌲ ()
topMMSPL ()

joinMMSP ∷ MMSP → MMSP → MMSP
joinMMSP :: MMSP -> MMSP -> MMSP
joinMMSP (MMSP MMSPMaxs
α̇₁) (MMSP MMSPMaxs
α̇₂) = MMSPMaxs -> MMSP
MMSP (MMSPMaxs -> MMSP) -> MMSPMaxs -> MMSP
forall a b. (a -> b) -> a -> b
$ MMSPMaxs -> MMSPMaxs -> MMSPMaxs
joinMaxs MMSPMaxs
α̇₁ MMSPMaxs
α̇₂

meetMMSP ∷ MMSP → MMSP → MMSP
meetMMSP :: MMSP -> MMSP -> MMSP
meetMMSP (MMSP MMSPMaxs
α̇₁) (MMSP MMSPMaxs
α̇₂) = MMSPMaxs -> MMSP
MMSP (MMSPMaxs -> MMSP) -> MMSPMaxs -> MMSP
forall a b. (a -> b) -> a -> b
$ MMSPMaxs -> MMSPMaxs -> MMSPMaxs
meetMaxs MMSPMaxs
α̇₁ MMSPMaxs
α̇₂

plusMMSP ∷ MMSP → MMSP → MMSP
plusMMSP :: MMSP -> MMSP -> MMSP
plusMMSP (MMSP MMSPMaxs
α̇₁) (MMSP MMSPMaxs
α̇₂) = MMSPMaxs -> MMSP
MMSP (MMSPMaxs -> MMSP) -> MMSPMaxs -> MMSP
forall a b. (a -> b) -> a -> b
$ MMSPMaxs -> MMSPMaxs -> MMSPMaxs
plusMaxs MMSPMaxs
α̇₁ MMSPMaxs
α̇₂

timesMMSP ∷ MMSP → MMSP → MMSP
timesMMSP :: MMSP -> MMSP -> MMSP
timesMMSP (MMSP MMSPMaxs
α̇₁) (MMSP MMSPMaxs
α̇₂) = MMSPMaxs -> MMSP
MMSP (MMSPMaxs -> MMSP) -> MMSPMaxs -> MMSP
forall a b. (a -> b) -> a -> b
$ MMSPMaxs -> MMSPMaxs -> MMSPMaxs
timesMaxs MMSPMaxs
α̇₁ MMSPMaxs
α̇₂

ponMMSP ∷ MMSP → ℕ → MMSP
ponMMSP :: MMSP -> ℕ -> MMSP
ponMMSP MMSP
e ℕ
n = 𝐼 MMSP -> MMSP
forall a t. (ToIter a t, Multiplicative a) => t -> a
product (𝐼 MMSP -> MMSP) -> 𝐼 MMSP -> MMSP
forall a b. (a -> b) -> a -> b
$ ℕ -> MMSP -> 𝐼 MMSP
forall n a. (Eq n, Zero n, One n, Plus n) => n -> a -> 𝐼 a
replicate ℕ
n MMSP
e

------------------
-- SUBSTITUTION --
------------------

-- gsubstMMSP ∷ (Substy t,Monad m) ⇒ (a → m MMSP) → t a → MMSP → m MMSP
-- gsubstMMSP 𝓋 𝓈 (MMSP α̇) = gsubstMMSPMaxs 𝓋 𝓈 α̇
-- 
-- gsubstMMSPMaxs ∷ (Substy t,Monad m) ⇒ (a → m MMSP) → t a → MMSPMaxs → m MMSP
-- gsubstMMSPMaxs 𝓋 𝓈 (MMSPMaxs a α) = (litMMSP a ⊔) ^$ gsubstMMSPMaxsMins 𝓋 𝓈 α
-- 
-- gsubstMMSPMaxsMins ∷ (Substy t,Monad m) ⇒ (a → m MMSP) → t a → 𝑃 MMSPMins → m MMSP
-- gsubstMMSPMaxsMins 𝓋 𝓈 α = joins ^$ mapM (gsubstMMSPMins 𝓋 𝓈) $ iter α
-- 
-- gsubstMMSPMins ∷ (Substy t,Monad m) ⇒ (a → m MMSP) → t a → MMSPMins → m MMSP
-- gsubstMMSPMins 𝓋 𝓈 (MMSPMins b β) = (elimAddTop top litMMSP b ⊓) ^$ gsubstMMSPMinsSums 𝓋 𝓈 β
-- 
-- gsubstMMSPMinsSums ∷ (Substy t,Monad m) ⇒ (a → m MMSP) → t a → 𝑃 MMSPSums → m MMSP
-- gsubstMMSPMinsSums 𝓋 𝓈 β = meets ^$ mapM (gsubstMMSPSums 𝓋 𝓈) $ iter β
-- 
-- gsubstMMSPSums ∷ (Substy t,Monad m) ⇒ (a → m MMSP) → t a → MMSPSums → m MMSP
-- gsubstMMSPSums 𝓋 𝓈 (MMSPSums c γ) = (litMMSP c +) ^$ gsubstMMSPSumsProds 𝓋 𝓈 γ
-- 
-- gsubstMMSPSumsProds ∷ (Substy t,Monad m) ⇒ (a → m MMSP) → t a → MMSPProds ⇰ ℕ → m MMSP
-- gsubstMMSPSumsProds 𝓋 𝓈 γ = sum ^$ mapMOn (iter γ) $ \ (δ :* d) → 
--   (litMMSP d ×) ^$ gsubstMMSPProds 𝓋 𝓈 δ
-- 
-- gsubstMMSPProds ∷ (Substy t,Monad m) ⇒ (a → m MMSP) → t a → MMSPProds → m MMSP
-- gsubstMMSPProds 𝓋 𝓈 (MMSPProds δ) = product ^$ mapMOn (iter δ) $ \ (ω :* e) → 
--   (^^ e) ^$ gsubstMMSPAtom 𝓋 𝓈 ω
-- 
-- gsubstMMSPAtom ∷ (Substy t,Monad m) ⇒ (a → m MMSP) → t a → MMSPAtom → m MMSP
-- gsubstMMSPAtom 𝓋 𝓈 = \case
--   Var_MMSPAtom (𝐴 𝒸 𝓎) → case 𝓈var 𝓈 𝓎 of
--     Inl 𝓎' → return $ varMMSP $ 𝐴 𝒸 𝓎'
--     Inr (𝓈O :* e) → elim𝑂 return (gsubstMMSP exfalso) 𝓈O *$ 𝓋 e
-- 
-- instance Substable m () MMSP MMSP where gsubstS 𝓋 𝓈 = gsubstMMSP 𝓋 $ ifNone null $ 𝓈 ⋕? ()

---------------
-- FREE VARS --
---------------

-- fvMMSP ∷ MMSP → 𝑃 𝕐
-- fvMMSP (MMSP α̇) = fvMMSPMaxs α̇
-- 
-- fvMMSPMaxs ∷ MMSPMaxs → 𝑃 𝕐
-- fvMMSPMaxs (MMSPMaxs _ α) = joins $ map fvMMSPMins $ iter α
-- 
-- fvMMSPMins ∷ MMSPMins → 𝑃 𝕐
-- fvMMSPMins (MMSPMins _ β) = joins $ map fvMMSPSums $ iter β
-- 
-- fvMMSPSums ∷ MMSPSums → 𝑃 𝕐
-- fvMMSPSums (MMSPSums _ γ) = joins $ map (fvMMSPProds ∘ fst) $ iter γ
-- 
-- fvMMSPProds ∷ MMSPProds → 𝑃 𝕐
-- fvMMSPProds (MMSPProds δ) = joins $ map (fvMMSPAtom ∘ fst) $ iter δ
-- 
-- fvMMSPAtom ∷ MMSPAtom → 𝑃 𝕐
-- fvMMSPAtom = \case
--   Var_MMSPAtom xA → fv $ aval xA

-- instance HasFBV MMSP where fbv = FBV pø ∘ fvMMSP

----------
-- MAXS --
----------

-- Mins --

-- ┌─────┐
-- │α ≡ 0│
-- └─────┘
zeroMaxsMins ∷ 𝑃 MMSPMins
-- β ≡ 0 ≜ ⨆{}
zeroMaxsMins :: 𝑃 MMSPMins
zeroMaxsMins = 𝑃 MMSPMins
forall a. Null a => a
null

-- ┌─────┐
-- │α ∨̃ α│
-- └─────┘
joinMaxsMins ∷ 𝑃 MMSPMins → 𝑃 MMSPMins → 𝑃 MMSPMins
joinMaxsMins :: 𝑃 MMSPMins -> 𝑃 MMSPMins -> 𝑃 MMSPMins
joinMaxsMins 𝑃 MMSPMins
α₁ 𝑃 MMSPMins
α₂ = 𝑃 MMSPMins
α₁ 𝑃 MMSPMins -> 𝑃 MMSPMins -> 𝑃 MMSPMins
forall e s. Set e s => s -> s -> s
∪ 𝑃 MMSPMins
α₂

-- ┌─────┐
-- │b ∧̃ α│
-- └─────┘
cmeetMaxsMins ∷ AddTop ℕ → 𝑃 MMSPMins → 𝑃 MMSPMins
-- b ∧̃ α = c ⊓ ⨆{ β | β ∈ α} 
--       ≜ ⨆ { b ∧̃ β | β ∈ α}
cmeetMaxsMins :: AddTop ℕ -> 𝑃 MMSPMins -> 𝑃 MMSPMins
cmeetMaxsMins AddTop ℕ
b = 𝐼 MMSPMins -> 𝑃 MMSPMins
forall s t e. (ToIter e t, Set e s) => t -> s
pow (𝐼 MMSPMins -> 𝑃 MMSPMins)
-> (𝐼 MMSPMins -> 𝐼 MMSPMins) -> 𝐼 MMSPMins -> 𝑃 MMSPMins
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (MMSPMins -> MMSPMins) -> 𝐼 MMSPMins -> 𝐼 MMSPMins
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (AddTop ℕ -> MMSPMins -> MMSPMins
cmeetMins AddTop ℕ
b) (𝐼 MMSPMins -> 𝑃 MMSPMins)
-> (𝑃 MMSPMins -> 𝐼 MMSPMins) -> 𝑃 MMSPMins -> 𝑃 MMSPMins
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑃 MMSPMins -> 𝐼 MMSPMins
forall a t. ToIter a t => t -> 𝐼 a
iter

-- ┌─────┐
-- │α ∧̃ α│
-- └─────┘
meetMaxsMins ∷ 𝑃 MMSPMins → 𝑃 MMSPMins → 𝑃 MMSPMins
-- α₁ ∧̃ α₂ = ⨆{ β | β ∈ α₁ } + ⨆{ β | β ∈ α₂ }
--         ≜ ⨆{ β₁ ∧̃ β₂ | β₁ ∈ α₁ , β₂ ∈ α₂}
meetMaxsMins :: 𝑃 MMSPMins -> 𝑃 MMSPMins -> 𝑃 MMSPMins
meetMaxsMins 𝑃 MMSPMins
α₁ 𝑃 MMSPMins
α₂ = 𝐼 MMSPMins -> 𝑃 MMSPMins
forall s t e. (ToIter e t, Set e s) => t -> s
pow (𝐼 MMSPMins -> 𝑃 MMSPMins) -> 𝐼 MMSPMins -> 𝑃 MMSPMins
forall a b. (a -> b) -> a -> b
$ 𝐼 (MMSPMins ∧ MMSPMins)
-> ((MMSPMins ∧ MMSPMins) -> MMSPMins) -> 𝐼 MMSPMins
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝑃 MMSPMins -> 𝐼 MMSPMins
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 MMSPMins
α₁ 𝐼 MMSPMins -> 𝐼 MMSPMins -> 𝐼 (MMSPMins ∧ MMSPMins)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a ∧ b)
⧆ 𝑃 MMSPMins -> 𝐼 MMSPMins
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 MMSPMins
α₂) (((MMSPMins ∧ MMSPMins) -> MMSPMins) -> 𝐼 MMSPMins)
-> ((MMSPMins ∧ MMSPMins) -> MMSPMins) -> 𝐼 MMSPMins
forall a b. (a -> b) -> a -> b
$ \ (MMSPMins
β₁ :* MMSPMins
β₂) → MMSPMins -> MMSPMins -> MMSPMins
meetMins MMSPMins
β₁ MMSPMins
β₂

-- ┌─────┐
-- │c +̃ α│
-- └─────┘
cplusMaxsMins ∷ ℕ → 𝑃 MMSPMins → 𝑃 MMSPMins
-- c +̃ α = c + ⨆{ β | β ∈ α} 
--       ≜ ⨆ { c +̃ β | β ∈ α}
cplusMaxsMins :: ℕ -> 𝑃 MMSPMins -> 𝑃 MMSPMins
cplusMaxsMins ℕ
c = 𝐼 MMSPMins -> 𝑃 MMSPMins
forall s t e. (ToIter e t, Set e s) => t -> s
pow (𝐼 MMSPMins -> 𝑃 MMSPMins)
-> (𝐼 MMSPMins -> 𝐼 MMSPMins) -> 𝐼 MMSPMins -> 𝑃 MMSPMins
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (MMSPMins -> MMSPMins) -> 𝐼 MMSPMins -> 𝐼 MMSPMins
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (ℕ -> MMSPMins -> MMSPMins
cplusMins ℕ
c) (𝐼 MMSPMins -> 𝑃 MMSPMins)
-> (𝑃 MMSPMins -> 𝐼 MMSPMins) -> 𝑃 MMSPMins -> 𝑃 MMSPMins
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑃 MMSPMins -> 𝐼 MMSPMins
forall a t. ToIter a t => t -> 𝐼 a
iter

-- ┌─────┐
-- │α +̃ α│
-- └─────┘
plusMaxsMins ∷ 𝑃 MMSPMins → 𝑃 MMSPMins → 𝑃 MMSPMins
-- α₁ +̃ α₂ = ⨆{ β | β ∈ α₁ } + ⨆{ β | β ∈ α₂ }
--         ≜ ⨆{ β₁ +̃ β₂ | β₁ ∈ α₁ , β₂ ∈ α₂}
plusMaxsMins :: 𝑃 MMSPMins -> 𝑃 MMSPMins -> 𝑃 MMSPMins
plusMaxsMins 𝑃 MMSPMins
α₁ 𝑃 MMSPMins
α₂ = 𝐼 MMSPMins -> 𝑃 MMSPMins
forall s t e. (ToIter e t, Set e s) => t -> s
pow (𝐼 MMSPMins -> 𝑃 MMSPMins) -> 𝐼 MMSPMins -> 𝑃 MMSPMins
forall a b. (a -> b) -> a -> b
$ 𝐼 (MMSPMins ∧ MMSPMins)
-> ((MMSPMins ∧ MMSPMins) -> MMSPMins) -> 𝐼 MMSPMins
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝑃 MMSPMins -> 𝐼 MMSPMins
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 MMSPMins
α₁ 𝐼 MMSPMins -> 𝐼 MMSPMins -> 𝐼 (MMSPMins ∧ MMSPMins)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a ∧ b)
⧆ 𝑃 MMSPMins -> 𝐼 MMSPMins
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 MMSPMins
α₂) (((MMSPMins ∧ MMSPMins) -> MMSPMins) -> 𝐼 MMSPMins)
-> ((MMSPMins ∧ MMSPMins) -> MMSPMins) -> 𝐼 MMSPMins
forall a b. (a -> b) -> a -> b
$ \ (MMSPMins
β₁ :* MMSPMins
β₂) → MMSPMins -> MMSPMins -> MMSPMins
plusMins MMSPMins
β₁ MMSPMins
β₂

-- ┌─────┐
-- │d ×̃ α│
-- └─────┘
ctimesMaxsMins ∷ ℕ → 𝑃 MMSPMins → 𝑃 MMSPMins
-- d ×̃ α = d × ⨆{ β | β ∈ α} 
--       ≜ ⨆ { d ×̃ β | β ∈ α}
ctimesMaxsMins :: ℕ -> 𝑃 MMSPMins -> 𝑃 MMSPMins
ctimesMaxsMins ℕ
d = 𝐼 MMSPMins -> 𝑃 MMSPMins
forall s t e. (ToIter e t, Set e s) => t -> s
pow (𝐼 MMSPMins -> 𝑃 MMSPMins)
-> (𝐼 MMSPMins -> 𝐼 MMSPMins) -> 𝐼 MMSPMins -> 𝑃 MMSPMins
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (MMSPMins -> MMSPMins) -> 𝐼 MMSPMins -> 𝐼 MMSPMins
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (ℕ -> MMSPMins -> MMSPMins
ctimesMins ℕ
d) (𝐼 MMSPMins -> 𝑃 MMSPMins)
-> (𝑃 MMSPMins -> 𝐼 MMSPMins) -> 𝑃 MMSPMins -> 𝑃 MMSPMins
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑃 MMSPMins -> 𝐼 MMSPMins
forall a t. ToIter a t => t -> 𝐼 a
iter

-- ┌─────┐
-- │α ×̃ α│
-- └─────┘
timesMaxsMins ∷ 𝑃 MMSPMins → 𝑃 MMSPMins → 𝑃 MMSPMins
-- α₁ ×̃ α₂ = ⨆{ β | β ∈ α₁ } × ⨆{ β | β ∈ α₂ }
--         ≜ ⨆{ β₁ ×̃ β₂ | β₁ ∈ α₁ , β₂ ∈ α₂}
timesMaxsMins :: 𝑃 MMSPMins -> 𝑃 MMSPMins -> 𝑃 MMSPMins
timesMaxsMins 𝑃 MMSPMins
α₁ 𝑃 MMSPMins
α₂ = 𝐼 MMSPMins -> 𝑃 MMSPMins
forall s t e. (ToIter e t, Set e s) => t -> s
pow (𝐼 MMSPMins -> 𝑃 MMSPMins) -> 𝐼 MMSPMins -> 𝑃 MMSPMins
forall a b. (a -> b) -> a -> b
$ 𝐼 (MMSPMins ∧ MMSPMins)
-> ((MMSPMins ∧ MMSPMins) -> MMSPMins) -> 𝐼 MMSPMins
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝑃 MMSPMins -> 𝐼 MMSPMins
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 MMSPMins
α₁ 𝐼 MMSPMins -> 𝐼 MMSPMins -> 𝐼 (MMSPMins ∧ MMSPMins)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a ∧ b)
⧆ 𝑃 MMSPMins -> 𝐼 MMSPMins
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 MMSPMins
α₂) (((MMSPMins ∧ MMSPMins) -> MMSPMins) -> 𝐼 MMSPMins)
-> ((MMSPMins ∧ MMSPMins) -> MMSPMins) -> 𝐼 MMSPMins
forall a b. (a -> b) -> a -> b
$ \ (MMSPMins
β₁ :* MMSPMins
β₂) → MMSPMins -> MMSPMins -> MMSPMins
timesMins MMSPMins
β₁ MMSPMins
β₂

-- Maxs --

-- ┌─────┐
-- │α̇ ∨̃ α̇│
-- └─────┘
joinMaxs ∷ MMSPMaxs → MMSPMaxs → MMSPMaxs
-- 
joinMaxs :: MMSPMaxs -> MMSPMaxs -> MMSPMaxs
joinMaxs (MMSPMaxs ℕ
a₁ 𝑃 MMSPMins
α₁) (MMSPMaxs ℕ
a₂ 𝑃 MMSPMins
α₂) = ℕ -> 𝑃 MMSPMins -> MMSPMaxs
MMSPMaxs (ℕ
a₁ ℕ -> ℕ -> ℕ
forall a. Join a => a -> a -> a
⊔ ℕ
a₂) (𝑃 MMSPMins -> MMSPMaxs) -> 𝑃 MMSPMins -> MMSPMaxs
forall a b. (a -> b) -> a -> b
$ 𝑃 MMSPMins -> 𝑃 MMSPMins -> 𝑃 MMSPMins
joinMaxsMins 𝑃 MMSPMins
α₁ 𝑃 MMSPMins
α₂

-- ┌─────┐
-- │α̇ ∧̃ α̇│
-- └─────┘
meetMaxs ∷ MMSPMaxs → MMSPMaxs → MMSPMaxs
-- (a₁ ∧̇ α₁) ∧̃ (a₂ ∧̇ α₂) ≜ (a₁ ⊓ a₂) ∨̇ ((a₁ ∧̃ α₂) ∨̃ (a₂ ∧̃ α₁) ∨̃ (α₁ ∧̃ α₂))
meetMaxs :: MMSPMaxs -> MMSPMaxs -> MMSPMaxs
meetMaxs (MMSPMaxs ℕ
a₁ 𝑃 MMSPMins
α₁) (MMSPMaxs ℕ
a₂ 𝑃 MMSPMins
α₂) = 
  ℕ -> 𝑃 MMSPMins -> MMSPMaxs
MMSPMaxs (ℕ
a₁ ℕ -> ℕ -> ℕ
forall a. Plus a => a -> a -> a
+ ℕ
a₂) (𝑃 MMSPMins -> MMSPMaxs) -> 𝑃 MMSPMins -> MMSPMaxs
forall a b. (a -> b) -> a -> b
$ 𝑃 MMSPMins
-> (𝑃 MMSPMins -> 𝑃 MMSPMins -> 𝑃 MMSPMins)
-> [𝑃 MMSPMins]
-> 𝑃 MMSPMins
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold 𝑃 MMSPMins
zeroMaxsMins 𝑃 MMSPMins -> 𝑃 MMSPMins -> 𝑃 MMSPMins
joinMaxsMins
    [ AddTop ℕ -> 𝑃 MMSPMins -> 𝑃 MMSPMins
cmeetMaxsMins (ℕ -> AddTop ℕ
forall a. a -> AddTop a
AddTop ℕ
a₁) 𝑃 MMSPMins
α₂
    , AddTop ℕ -> 𝑃 MMSPMins -> 𝑃 MMSPMins
cmeetMaxsMins (ℕ -> AddTop ℕ
forall a. a -> AddTop a
AddTop ℕ
a₂) 𝑃 MMSPMins
α₂
    , 𝑃 MMSPMins -> 𝑃 MMSPMins -> 𝑃 MMSPMins
meetMaxsMins 𝑃 MMSPMins
α₁ 𝑃 MMSPMins
α₂
    ]

-- ┌─────┐
-- │α̇ +̃ α̇│
-- └─────┘
plusMaxs ∷ MMSPMaxs → MMSPMaxs → MMSPMaxs
-- (a₁ ∧̇ α₁) +̃ (a₂ ∧̇ α₂) ≜ (a₁ + a₂) ∨̇ ((a₁ +̃ α₂) ∨̃ (a₂ +̃ α₁) ∨̃ (α₁ +̃ α₂))
plusMaxs :: MMSPMaxs -> MMSPMaxs -> MMSPMaxs
plusMaxs (MMSPMaxs ℕ
a₁ 𝑃 MMSPMins
α₁) (MMSPMaxs ℕ
a₂ 𝑃 MMSPMins
α₂) = 
  ℕ -> 𝑃 MMSPMins -> MMSPMaxs
MMSPMaxs (ℕ
a₁ ℕ -> ℕ -> ℕ
forall a. Plus a => a -> a -> a
+ ℕ
a₂) (𝑃 MMSPMins -> MMSPMaxs) -> 𝑃 MMSPMins -> MMSPMaxs
forall a b. (a -> b) -> a -> b
$ 𝑃 MMSPMins
-> (𝑃 MMSPMins -> 𝑃 MMSPMins -> 𝑃 MMSPMins)
-> [𝑃 MMSPMins]
-> 𝑃 MMSPMins
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold 𝑃 MMSPMins
zeroMaxsMins 𝑃 MMSPMins -> 𝑃 MMSPMins -> 𝑃 MMSPMins
plusMaxsMins
    [ ℕ -> 𝑃 MMSPMins -> 𝑃 MMSPMins
cplusMaxsMins ℕ
a₁ 𝑃 MMSPMins
α₂
    , ℕ -> 𝑃 MMSPMins -> 𝑃 MMSPMins
cplusMaxsMins ℕ
a₂ 𝑃 MMSPMins
α₂
    , 𝑃 MMSPMins -> 𝑃 MMSPMins -> 𝑃 MMSPMins
plusMaxsMins 𝑃 MMSPMins
α₁ 𝑃 MMSPMins
α₂
    ]

-- ┌─────┐
-- │α̇ ×̃ α̇│
-- └─────┘
timesMaxs ∷ MMSPMaxs → MMSPMaxs → MMSPMaxs
-- (a₁ ∧̇ α₁) ×̃ (a₂ ∧̇ α₂) ≜ (a₁ × a₂) ∨̇ ((a₁ ×̃ α₂) ∨̃ (a₂ ×̃ α₁) ∨̃ (α₁̇ ×̃ α₂))
timesMaxs :: MMSPMaxs -> MMSPMaxs -> MMSPMaxs
timesMaxs (MMSPMaxs ℕ
a₁ 𝑃 MMSPMins
α₁) (MMSPMaxs ℕ
a₂ 𝑃 MMSPMins
α₂) = 
  ℕ -> 𝑃 MMSPMins -> MMSPMaxs
MMSPMaxs (ℕ
a₁ ℕ -> ℕ -> ℕ
forall a. Plus a => a -> a -> a
+ ℕ
a₂) (𝑃 MMSPMins -> MMSPMaxs) -> 𝑃 MMSPMins -> MMSPMaxs
forall a b. (a -> b) -> a -> b
$ 𝑃 MMSPMins
-> (𝑃 MMSPMins -> 𝑃 MMSPMins -> 𝑃 MMSPMins)
-> [𝑃 MMSPMins]
-> 𝑃 MMSPMins
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold 𝑃 MMSPMins
zeroMaxsMins 𝑃 MMSPMins -> 𝑃 MMSPMins -> 𝑃 MMSPMins
timesMaxsMins
    [ ℕ -> 𝑃 MMSPMins -> 𝑃 MMSPMins
ctimesMaxsMins ℕ
a₁ 𝑃 MMSPMins
α₂
    , ℕ -> 𝑃 MMSPMins -> 𝑃 MMSPMins
ctimesMaxsMins ℕ
a₂ 𝑃 MMSPMins
α₂
    , 𝑃 MMSPMins -> 𝑃 MMSPMins -> 𝑃 MMSPMins
timesMaxsMins 𝑃 MMSPMins
α₁ 𝑃 MMSPMins
α₂
    ]

----------
-- MINS --
----------

-- Sums --

-- ┌─────┐
-- │β ≡ ∞│
-- └─────┘
infMinsSums ∷ 𝑃 MMSPSums
-- β ≡ ∞ ≜ ⨅{}
infMinsSums :: 𝑃 MMSPSums
infMinsSums = 𝑃 MMSPSums
forall a. Null a => a
null

-- ┌─────┐
-- │β ∧̃ β│
-- └─────┘
meetMinsSums ∷ 𝑃 MMSPSums → 𝑃 MMSPSums → 𝑃 MMSPSums
-- β₁ ∧̃ β₂ = ⨅{ γ | γ ∈ β₁ } ⊓ ⨅{ γ | γ ∈ β₂ }
--         ≜ ⨅( { γ | γ ∈ β₁ }
--            ∪ { γ | γ ∈ β₂ } )
meetMinsSums :: 𝑃 MMSPSums -> 𝑃 MMSPSums -> 𝑃 MMSPSums
meetMinsSums 𝑃 MMSPSums
xs 𝑃 MMSPSums
ys = 𝑃 MMSPSums
xs 𝑃 MMSPSums -> 𝑃 MMSPSums -> 𝑃 MMSPSums
forall e s. Set e s => s -> s -> s
∪ 𝑃 MMSPSums
ys

-- ┌─────┐
-- │c +̃ β│
-- └─────┘
cplusMinsSums ∷ ℕ → 𝑃 MMSPSums → 𝑃 MMSPSums
-- c +̃ β = c + ⨅{ γ | γ ∈ β} 
--       ≜ ⨅ { c +̃ γ | γ ∈ β}
cplusMinsSums :: ℕ -> 𝑃 MMSPSums -> 𝑃 MMSPSums
cplusMinsSums ℕ
c = 𝐼 MMSPSums -> 𝑃 MMSPSums
forall s t e. (ToIter e t, Set e s) => t -> s
pow (𝐼 MMSPSums -> 𝑃 MMSPSums)
-> (𝐼 MMSPSums -> 𝐼 MMSPSums) -> 𝐼 MMSPSums -> 𝑃 MMSPSums
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (MMSPSums -> MMSPSums) -> 𝐼 MMSPSums -> 𝐼 MMSPSums
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (ℕ -> MMSPSums -> MMSPSums
cplusSums ℕ
c) (𝐼 MMSPSums -> 𝑃 MMSPSums)
-> (𝑃 MMSPSums -> 𝐼 MMSPSums) -> 𝑃 MMSPSums -> 𝑃 MMSPSums
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑃 MMSPSums -> 𝐼 MMSPSums
forall a t. ToIter a t => t -> 𝐼 a
iter

-- ┌─────┐
-- │β +̃ β│
-- └─────┘
plusMinsSums ∷ 𝑃 MMSPSums → 𝑃 MMSPSums → 𝑃 MMSPSums
-- β₁ +̃ β₂ = ⨅{ γ | γ ∈ β₁ } + ⨅{ γ | γ ∈ β₂ }
--         ≜ ⨅{ γ₁ +̃ γ₂ | γ₁ ∈ β₁ , γ₂ ∈ β₂}
plusMinsSums :: 𝑃 MMSPSums -> 𝑃 MMSPSums -> 𝑃 MMSPSums
plusMinsSums 𝑃 MMSPSums
β₁ 𝑃 MMSPSums
β₂ = 𝐼 MMSPSums -> 𝑃 MMSPSums
forall s t e. (ToIter e t, Set e s) => t -> s
pow (𝐼 MMSPSums -> 𝑃 MMSPSums) -> 𝐼 MMSPSums -> 𝑃 MMSPSums
forall a b. (a -> b) -> a -> b
$ 𝐼 (MMSPSums ∧ MMSPSums)
-> ((MMSPSums ∧ MMSPSums) -> MMSPSums) -> 𝐼 MMSPSums
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝑃 MMSPSums -> 𝐼 MMSPSums
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 MMSPSums
β₁ 𝐼 MMSPSums -> 𝐼 MMSPSums -> 𝐼 (MMSPSums ∧ MMSPSums)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a ∧ b)
⧆ 𝑃 MMSPSums -> 𝐼 MMSPSums
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 MMSPSums
β₂) (((MMSPSums ∧ MMSPSums) -> MMSPSums) -> 𝐼 MMSPSums)
-> ((MMSPSums ∧ MMSPSums) -> MMSPSums) -> 𝐼 MMSPSums
forall a b. (a -> b) -> a -> b
$ \ (MMSPSums
γ₁ :* MMSPSums
γ₂) → MMSPSums -> MMSPSums -> MMSPSums
plusSums MMSPSums
γ₁ MMSPSums
γ₂

-- ┌─────┐
-- │d ×̃ β│
-- └─────┘
ctimesMinsSums ∷ ℕ → 𝑃 MMSPSums → 𝑃 MMSPSums
-- d ×̃ β = d × ⨅{ γ | γ ∈ β} 
--       ≜ ⨅ { d ×̃ γ | γ ∈ β}
ctimesMinsSums :: ℕ -> 𝑃 MMSPSums -> 𝑃 MMSPSums
ctimesMinsSums ℕ
c = 𝐼 MMSPSums -> 𝑃 MMSPSums
forall s t e. (ToIter e t, Set e s) => t -> s
pow (𝐼 MMSPSums -> 𝑃 MMSPSums)
-> (𝐼 MMSPSums -> 𝐼 MMSPSums) -> 𝐼 MMSPSums -> 𝑃 MMSPSums
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (MMSPSums -> MMSPSums) -> 𝐼 MMSPSums -> 𝐼 MMSPSums
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (ℕ -> MMSPSums -> MMSPSums
cplusSums ℕ
c) (𝐼 MMSPSums -> 𝑃 MMSPSums)
-> (𝑃 MMSPSums -> 𝐼 MMSPSums) -> 𝑃 MMSPSums -> 𝑃 MMSPSums
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑃 MMSPSums -> 𝐼 MMSPSums
forall a t. ToIter a t => t -> 𝐼 a
iter

-- ┌─────┐
-- │β ×̃ β│
-- └─────┘
timesMinsSums ∷ 𝑃 MMSPSums → 𝑃 MMSPSums → 𝑃 MMSPSums
-- β₁ ×̃ β₂ = ⨅{ γ | γ ∈ β₁ } × ⨅{ γ | γ ∈ β₂ }
--         ≜ ⨅{ γ₁ ×̃ γ₂ | γ₁ ∈ β₁ , γ₂ ∈ β₂}
timesMinsSums :: 𝑃 MMSPSums -> 𝑃 MMSPSums -> 𝑃 MMSPSums
timesMinsSums 𝑃 MMSPSums
β₁ 𝑃 MMSPSums
β₂ = 𝐼 MMSPSums -> 𝑃 MMSPSums
forall s t e. (ToIter e t, Set e s) => t -> s
pow (𝐼 MMSPSums -> 𝑃 MMSPSums) -> 𝐼 MMSPSums -> 𝑃 MMSPSums
forall a b. (a -> b) -> a -> b
$ 𝐼 (MMSPSums ∧ MMSPSums)
-> ((MMSPSums ∧ MMSPSums) -> MMSPSums) -> 𝐼 MMSPSums
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝑃 MMSPSums -> 𝐼 MMSPSums
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 MMSPSums
β₁ 𝐼 MMSPSums -> 𝐼 MMSPSums -> 𝐼 (MMSPSums ∧ MMSPSums)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a ∧ b)
⧆ 𝑃 MMSPSums -> 𝐼 MMSPSums
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑃 MMSPSums
β₂) (((MMSPSums ∧ MMSPSums) -> MMSPSums) -> 𝐼 MMSPSums)
-> ((MMSPSums ∧ MMSPSums) -> MMSPSums) -> 𝐼 MMSPSums
forall a b. (a -> b) -> a -> b
$ \ (MMSPSums
γ₁ :* MMSPSums
γ₂) → MMSPSums -> MMSPSums -> MMSPSums
timesSums MMSPSums
γ₁ MMSPSums
γ₂

-- Mins --

-- ┌─────┐
-- │b ∧̃ β̇│
-- └─────┘
cmeetMins ∷ AddTop ℕ → MMSPMins → MMSPMins
-- b₀ ⊓ (b ∧̇ β) ≜ (b₀ ⊓ b) ∧̇ β
cmeetMins :: AddTop ℕ -> MMSPMins -> MMSPMins
cmeetMins AddTop ℕ
b₀ (MMSPMins AddTop ℕ
b 𝑃 MMSPSums
β) = AddTop ℕ -> 𝑃 MMSPSums -> MMSPMins
MMSPMins (AddTop ℕ
b₀ AddTop ℕ -> AddTop ℕ -> AddTop ℕ
forall a. Meet a => a -> a -> a
⊓ AddTop ℕ
b) 𝑃 MMSPSums
β

-- ┌─────┐
-- │β̇ ∧̃ β̇│
-- └─────┘
meetMins ∷ MMSPMins → MMSPMins → MMSPMins
-- (b₁ ∧̇  β₁) ⊓ (b₂ ∧̇  β₂) ≜ (b₁ ⊓ b₂) ∧̇ (β₁ ∧̃ β₂)
meetMins :: MMSPMins -> MMSPMins -> MMSPMins
meetMins (MMSPMins AddTop ℕ
b₁ 𝑃 MMSPSums
β₁) (MMSPMins AddTop ℕ
b₂ 𝑃 MMSPSums
β₂) = AddTop ℕ -> 𝑃 MMSPSums -> MMSPMins
MMSPMins (AddTop ℕ
b₁ AddTop ℕ -> AddTop ℕ -> AddTop ℕ
forall a. Meet a => a -> a -> a
⊓ AddTop ℕ
b₂) (𝑃 MMSPSums -> MMSPMins) -> 𝑃 MMSPSums -> MMSPMins
forall a b. (a -> b) -> a -> b
$ 𝑃 MMSPSums -> 𝑃 MMSPSums -> 𝑃 MMSPSums
meetMinsSums 𝑃 MMSPSums
β₁ 𝑃 MMSPSums
β₂

-- ┌─────┐
-- │c +̃ β̇│
-- └─────┘
cplusMins ∷ ℕ → MMSPMins → MMSPMins
-- c +̃ (b ∧̇ β) ≜ (c + b) ∧̇ (c +̃ β)
cplusMins :: ℕ -> MMSPMins -> MMSPMins
cplusMins ℕ
c (MMSPMins AddTop ℕ
b 𝑃 MMSPSums
β) = AddTop ℕ -> 𝑃 MMSPSums -> MMSPMins
MMSPMins ((ℕ -> ℕ) -> AddTop ℕ -> AddTop ℕ
forall a b. (a -> b) -> AddTop a -> AddTop b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (ℕ -> ℕ -> ℕ
forall a. Plus a => a -> a -> a
+ ℕ
c) AddTop ℕ
b) (𝑃 MMSPSums -> MMSPMins) -> 𝑃 MMSPSums -> MMSPMins
forall a b. (a -> b) -> a -> b
$ ℕ -> 𝑃 MMSPSums -> 𝑃 MMSPSums
cplusMinsSums ℕ
c 𝑃 MMSPSums
β

-- ┌─────┐
-- │β̇ +̃ β̇│
-- └─────┘
plusMins ∷ MMSPMins → MMSPMins → MMSPMins
-- (b₁ ∧̇ β₁) +̃ (b₂ ∧̇ β₂) ≜ (b₁ + b₂) ∧̇ ((b₁ +̃ β₂) ∧̃ (b₂ +̃ β₁) ∧̃ (β₁̇ +̃ β₂))
plusMins :: MMSPMins -> MMSPMins -> MMSPMins
plusMins (MMSPMins AddTop ℕ
b₁ 𝑃 MMSPSums
β₁) (MMSPMins AddTop ℕ
b₂ 𝑃 MMSPSums
β₂) = 
  AddTop ℕ -> 𝑃 MMSPSums -> MMSPMins
MMSPMins (AddTop ℕ
b₁ AddTop ℕ -> AddTop ℕ -> AddTop ℕ
forall a. Plus a => a -> a -> a
+ AddTop ℕ
b₂) (𝑃 MMSPSums -> MMSPMins) -> 𝑃 MMSPSums -> MMSPMins
forall a b. (a -> b) -> a -> b
$ 𝑃 MMSPSums
-> (𝑃 MMSPSums -> 𝑃 MMSPSums -> 𝑃 MMSPSums)
-> [𝑃 MMSPSums]
-> 𝑃 MMSPSums
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold 𝑃 MMSPSums
infMinsSums 𝑃 MMSPSums -> 𝑃 MMSPSums -> 𝑃 MMSPSums
meetMinsSums
    [ ((ℕ -> 𝑃 MMSPSums) -> AddTop ℕ -> 𝑃 MMSPSums)
-> AddTop ℕ -> (ℕ -> 𝑃 MMSPSums) -> 𝑃 MMSPSums
forall a b c. (a -> b -> c) -> b -> a -> c
flip (𝑃 MMSPSums -> (ℕ -> 𝑃 MMSPSums) -> AddTop ℕ -> 𝑃 MMSPSums
forall b a. b -> (a -> b) -> AddTop a -> b
elimAddTop 𝑃 MMSPSums
forall a. Null a => a
null) AddTop ℕ
b₁ ((ℕ -> 𝑃 MMSPSums) -> 𝑃 MMSPSums)
-> (ℕ -> 𝑃 MMSPSums) -> 𝑃 MMSPSums
forall a b. (a -> b) -> a -> b
$ \ ℕ
b₁' → ℕ -> 𝑃 MMSPSums -> 𝑃 MMSPSums
cplusMinsSums ℕ
b₁' 𝑃 MMSPSums
β₂
    , ((ℕ -> 𝑃 MMSPSums) -> AddTop ℕ -> 𝑃 MMSPSums)
-> AddTop ℕ -> (ℕ -> 𝑃 MMSPSums) -> 𝑃 MMSPSums
forall a b c. (a -> b -> c) -> b -> a -> c
flip (𝑃 MMSPSums -> (ℕ -> 𝑃 MMSPSums) -> AddTop ℕ -> 𝑃 MMSPSums
forall b a. b -> (a -> b) -> AddTop a -> b
elimAddTop 𝑃 MMSPSums
forall a. Null a => a
null) AddTop ℕ
b₂ ((ℕ -> 𝑃 MMSPSums) -> 𝑃 MMSPSums)
-> (ℕ -> 𝑃 MMSPSums) -> 𝑃 MMSPSums
forall a b. (a -> b) -> a -> b
$ \ ℕ
b₂' → ℕ -> 𝑃 MMSPSums -> 𝑃 MMSPSums
cplusMinsSums ℕ
b₂' 𝑃 MMSPSums
β₂
    , 𝑃 MMSPSums -> 𝑃 MMSPSums -> 𝑃 MMSPSums
plusMinsSums 𝑃 MMSPSums
β₁ 𝑃 MMSPSums
β₂
    ]

-- ┌─────┐
-- │c ×̃ β̇│
-- └─────┘
ctimesMins ∷ ℕ → MMSPMins → MMSPMins
-- c ×̃ (b ∧̇ β) ≜ (c × b) ∧̇ (c ×̃ β)
ctimesMins :: ℕ -> MMSPMins -> MMSPMins
ctimesMins ℕ
c (MMSPMins AddTop ℕ
b 𝑃 MMSPSums
β) = AddTop ℕ -> 𝑃 MMSPSums -> MMSPMins
MMSPMins (ℕ -> AddTop ℕ
forall a. a -> AddTop a
AddTop ℕ
c AddTop ℕ -> AddTop ℕ -> AddTop ℕ
forall a. Times a => a -> a -> a
× AddTop ℕ
b) (𝑃 MMSPSums -> MMSPMins) -> 𝑃 MMSPSums -> MMSPMins
forall a b. (a -> b) -> a -> b
$ ℕ -> 𝑃 MMSPSums -> 𝑃 MMSPSums
ctimesMinsSums ℕ
c 𝑃 MMSPSums
β

-- ┌─────┐
-- │β̇ ×̃ β̇│
-- └─────┘
timesMins ∷ MMSPMins → MMSPMins → MMSPMins
-- (b₁ ∧̇ β₁) ×̃ (b₂ ∧̇ β₂) ≜ (b₁ × b₂) ∧̇ ((b₁ ×̃ β₂) ∧̃ (b₂ ×̃ β₁) ∧̃ (β₁̇ ×̃ β₂))
timesMins :: MMSPMins -> MMSPMins -> MMSPMins
timesMins (MMSPMins AddTop ℕ
b₁ 𝑃 MMSPSums
β₁) (MMSPMins AddTop ℕ
b₂ 𝑃 MMSPSums
β₂) = 
  AddTop ℕ -> 𝑃 MMSPSums -> MMSPMins
MMSPMins (AddTop ℕ
b₁ AddTop ℕ -> AddTop ℕ -> AddTop ℕ
forall a. Times a => a -> a -> a
× AddTop ℕ
b₂) (𝑃 MMSPSums -> MMSPMins) -> 𝑃 MMSPSums -> MMSPMins
forall a b. (a -> b) -> a -> b
$ 𝑃 MMSPSums
-> (𝑃 MMSPSums -> 𝑃 MMSPSums -> 𝑃 MMSPSums)
-> [𝑃 MMSPSums]
-> 𝑃 MMSPSums
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold 𝑃 MMSPSums
infMinsSums 𝑃 MMSPSums -> 𝑃 MMSPSums -> 𝑃 MMSPSums
meetMinsSums
    [ ((ℕ -> 𝑃 MMSPSums) -> AddTop ℕ -> 𝑃 MMSPSums)
-> AddTop ℕ -> (ℕ -> 𝑃 MMSPSums) -> 𝑃 MMSPSums
forall a b c. (a -> b -> c) -> b -> a -> c
flip (𝑃 MMSPSums -> (ℕ -> 𝑃 MMSPSums) -> AddTop ℕ -> 𝑃 MMSPSums
forall b a. b -> (a -> b) -> AddTop a -> b
elimAddTop 𝑃 MMSPSums
forall a. Null a => a
null) AddTop ℕ
b₁ ((ℕ -> 𝑃 MMSPSums) -> 𝑃 MMSPSums)
-> (ℕ -> 𝑃 MMSPSums) -> 𝑃 MMSPSums
forall a b. (a -> b) -> a -> b
$ \ ℕ
b₁' → ℕ -> 𝑃 MMSPSums -> 𝑃 MMSPSums
ctimesMinsSums ℕ
b₁' 𝑃 MMSPSums
β₂
    , ((ℕ -> 𝑃 MMSPSums) -> AddTop ℕ -> 𝑃 MMSPSums)
-> AddTop ℕ -> (ℕ -> 𝑃 MMSPSums) -> 𝑃 MMSPSums
forall a b c. (a -> b -> c) -> b -> a -> c
flip (𝑃 MMSPSums -> (ℕ -> 𝑃 MMSPSums) -> AddTop ℕ -> 𝑃 MMSPSums
forall b a. b -> (a -> b) -> AddTop a -> b
elimAddTop 𝑃 MMSPSums
forall a. Null a => a
null) AddTop ℕ
b₂ ((ℕ -> 𝑃 MMSPSums) -> 𝑃 MMSPSums)
-> (ℕ -> 𝑃 MMSPSums) -> 𝑃 MMSPSums
forall a b. (a -> b) -> a -> b
$ \ ℕ
b₂' → ℕ -> 𝑃 MMSPSums -> 𝑃 MMSPSums
ctimesMinsSums ℕ
b₂' 𝑃 MMSPSums
β₂
    , 𝑃 MMSPSums -> 𝑃 MMSPSums -> 𝑃 MMSPSums
timesMinsSums 𝑃 MMSPSums
β₁ 𝑃 MMSPSums
β₂
    ]

----------
-- SUMS --
----------

-- Prods --

-- ┌─────┐
-- │γ ≡ 0│
-- └─────┘
zeroSumsProds ∷ MMSPProds ⇰ ℕ
-- γ ≡ 0 ≜ ∑{}
zeroSumsProds :: MMSPProds ⇰ ℕ
zeroSumsProds = MMSPProds ⇰ ℕ
forall a. Null a => a
null

-- ┌─────┐
-- │γ +̃ γ│
-- └─────┘
plusSumsProds ∷ MMSPProds ⇰ ℕ → MMSPProds ⇰ ℕ → MMSPProds ⇰ ℕ
-- γ₁ +̃ γ₂ = ∑{ d×̇δ | d×̇δ ∈ γ₁} + ∑{ d×̇δ | d×̇δ ∈ γ₂ }
--         ≜ ∑( { d×̇δ | d×̇δ ∈ γ₁ , δ ∉ dom(γ₂) }
--            ∪ { d×̇δ | d×̇δ ∈ γ₂ , δ ∉ dom(γ₁) }
--            ∪ { (d₁+d₂)×̇δ | d₁×̇δ ∈ γ₁ , d₂×̇δ ∈ γ₂ } )
plusSumsProds :: (MMSPProds ⇰ ℕ) -> (MMSPProds ⇰ ℕ) -> MMSPProds ⇰ ℕ
plusSumsProds MMSPProds ⇰ ℕ
γ₁ MMSPProds ⇰ ℕ
γ₂ = MMSPProds ⇰ ℕ
γ₁ (MMSPProds ⇰ ℕ) -> (MMSPProds ⇰ ℕ) -> MMSPProds ⇰ ℕ
forall a. Plus a => a -> a -> a
+ MMSPProds ⇰ ℕ
γ₂

-- ┌─────┐
-- │d ×̃ γ│
-- └─────┘
ctimesSumsProds ∷ ℕ → MMSPProds ⇰ ℕ → MMSPProds ⇰ ℕ
-- d₀ ×̃ γ ≜ d₀ × ∑{ d×̇δ | d×̇δ ∈ γ }
--        ≜ ∑{ d₀d×̇δ | d×̇δ ∈ γ }
ctimesSumsProds :: ℕ -> (MMSPProds ⇰ ℕ) -> MMSPProds ⇰ ℕ
ctimesSumsProds ℕ
d MMSPProds ⇰ ℕ
γ = (ℕ -> ℕ) -> (MMSPProds ⇰ ℕ) -> MMSPProds ⇰ ℕ
forall a b. (a -> b) -> (MMSPProds ⇰ a) -> MMSPProds ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (ℕ -> ℕ -> ℕ
forall a. Times a => a -> a -> a
× ℕ
d) MMSPProds ⇰ ℕ
γ

-- ┌─────┐
-- │γ ×̃ γ│
-- └─────┘
timesSumsProds ∷ MMSPProds ⇰ ℕ → MMSPProds ⇰ ℕ → MMSPProds ⇰ ℕ
-- γ₁ ×̃ γ₂ = ∑{ d×̇δ | d×̇δ ∈ γ₁} × ∑{ d×̇δ | d×̇δ ∈ γ₂ }
--         ≜ ∑{ d₁d₂×̇(δ₁×̃δ₂) | d₁×̇δ₁ ∈ γ₁ , d₂×̇δ₂ ∈ γ₂ }
timesSumsProds :: (MMSPProds ⇰ ℕ) -> (MMSPProds ⇰ ℕ) -> MMSPProds ⇰ ℕ
timesSumsProds MMSPProds ⇰ ℕ
γ₁ MMSPProds ⇰ ℕ
γ₂ = 𝐼 (MMSPProds ∧ ℕ) -> MMSPProds ⇰ ℕ
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 (MMSPProds ∧ ℕ) -> MMSPProds ⇰ ℕ)
-> 𝐼 (MMSPProds ∧ ℕ) -> MMSPProds ⇰ ℕ
forall a b. (a -> b) -> a -> b
$ 𝐼 ((MMSPProds ∧ ℕ) ∧ (MMSPProds ∧ ℕ))
-> (((MMSPProds ∧ ℕ) ∧ (MMSPProds ∧ ℕ)) -> MMSPProds ∧ ℕ)
-> 𝐼 (MMSPProds ∧ ℕ)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn ((MMSPProds ⇰ ℕ) -> 𝐼 (MMSPProds ∧ ℕ)
forall a t. ToIter a t => t -> 𝐼 a
iter MMSPProds ⇰ ℕ
γ₁ 𝐼 (MMSPProds ∧ ℕ)
-> 𝐼 (MMSPProds ∧ ℕ) -> 𝐼 ((MMSPProds ∧ ℕ) ∧ (MMSPProds ∧ ℕ))
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a ∧ b)
⧆ (MMSPProds ⇰ ℕ) -> 𝐼 (MMSPProds ∧ ℕ)
forall a t. ToIter a t => t -> 𝐼 a
iter MMSPProds ⇰ ℕ
γ₂) ((((MMSPProds ∧ ℕ) ∧ (MMSPProds ∧ ℕ)) -> MMSPProds ∧ ℕ)
 -> 𝐼 (MMSPProds ∧ ℕ))
-> (((MMSPProds ∧ ℕ) ∧ (MMSPProds ∧ ℕ)) -> MMSPProds ∧ ℕ)
-> 𝐼 (MMSPProds ∧ ℕ)
forall a b. (a -> b) -> a -> b
$ \ ((MMSPProds
δ₁ :* ℕ
d₁) :* (MMSPProds
δ₂ :* ℕ
d₂)) → 
  MMSPProds -> MMSPProds -> MMSPProds
timesProds MMSPProds
δ₁ MMSPProds
δ₂ MMSPProds -> ℕ -> MMSPProds ∧ ℕ
forall a b. a -> b -> a ∧ b
:* (ℕ
d₁ ℕ -> ℕ -> ℕ
forall a. Times a => a -> a -> a
× ℕ
d₂)

-- Sums --

-- ┌─────┐
-- │c +̃ γ̇│
-- └─────┘
cplusSums ∷ ℕ → MMSPSums → MMSPSums
-- c₀ +̃ (c +̇ γ) ≜ (c₀ + c) +̇ γ
cplusSums :: ℕ -> MMSPSums -> MMSPSums
cplusSums ℕ
c₀ (MMSPSums ℕ
c MMSPProds ⇰ ℕ
γ) = ℕ -> (MMSPProds ⇰ ℕ) -> MMSPSums
MMSPSums (ℕ
c₀ ℕ -> ℕ -> ℕ
forall a. Plus a => a -> a -> a
+ ℕ
c) MMSPProds ⇰ ℕ
γ

-- ┌─────┐
-- │γ̇ +̃ γ̇│
-- └─────┘
plusSums ∷ MMSPSums → MMSPSums → MMSPSums
-- c₁ +̇ γ₁ +̃ c₂ +̇ γ₂ ≜ (c₁ + c₂) +̇ (γ₁ +̃ γ₂)
plusSums :: MMSPSums -> MMSPSums -> MMSPSums
plusSums (MMSPSums ℕ
c₁ MMSPProds ⇰ ℕ
γ₁) (MMSPSums ℕ
c₂ MMSPProds ⇰ ℕ
γ₂) = ℕ -> (MMSPProds ⇰ ℕ) -> MMSPSums
MMSPSums (ℕ
c₁ ℕ -> ℕ -> ℕ
forall a. Plus a => a -> a -> a
+ ℕ
c₂) ((MMSPProds ⇰ ℕ) -> MMSPSums) -> (MMSPProds ⇰ ℕ) -> MMSPSums
forall a b. (a -> b) -> a -> b
$ (MMSPProds ⇰ ℕ) -> (MMSPProds ⇰ ℕ) -> MMSPProds ⇰ ℕ
plusSumsProds MMSPProds ⇰ ℕ
γ₁ MMSPProds ⇰ ℕ
γ₂

-- ┌─────┐
-- │γ̇ ×̃ γ̇│
-- └─────┘
timesSums ∷ MMSPSums → MMSPSums → MMSPSums
-- (c₁ +̇ γ₁) ×̃ (c₂ +̇ γ₂) ≜ (c₁ × c₂) +̇ ((c₁ ×̃ γ₂) +̃ (c₂ ×̃ γ₁) +̃ (γ₁ ×̃ γ₂))
timesSums :: MMSPSums -> MMSPSums -> MMSPSums
timesSums (MMSPSums ℕ
c₁ MMSPProds ⇰ ℕ
γ₁) (MMSPSums ℕ
c₂ MMSPProds ⇰ ℕ
γ₂) =
  ℕ -> (MMSPProds ⇰ ℕ) -> MMSPSums
MMSPSums (ℕ
c₁ ℕ -> ℕ -> ℕ
forall a. Times a => a -> a -> a
× ℕ
c₂) ((MMSPProds ⇰ ℕ) -> MMSPSums) -> (MMSPProds ⇰ ℕ) -> MMSPSums
forall a b. (a -> b) -> a -> b
$ (MMSPProds ⇰ ℕ)
-> ((MMSPProds ⇰ ℕ) -> (MMSPProds ⇰ ℕ) -> MMSPProds ⇰ ℕ)
-> [MMSPProds ⇰ ℕ]
-> MMSPProds ⇰ ℕ
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold MMSPProds ⇰ ℕ
zeroSumsProds (MMSPProds ⇰ ℕ) -> (MMSPProds ⇰ ℕ) -> MMSPProds ⇰ ℕ
plusSumsProds
    [ ℕ -> (MMSPProds ⇰ ℕ) -> MMSPProds ⇰ ℕ
ctimesSumsProds ℕ
c₁ MMSPProds ⇰ ℕ
γ₂
    , ℕ -> (MMSPProds ⇰ ℕ) -> MMSPProds ⇰ ℕ
ctimesSumsProds ℕ
c₂ MMSPProds ⇰ ℕ
γ₁
    , (MMSPProds ⇰ ℕ) -> (MMSPProds ⇰ ℕ) -> MMSPProds ⇰ ℕ
timesSumsProds MMSPProds ⇰ ℕ
γ₁ MMSPProds ⇰ ℕ
γ₂
    ]

-----------
-- PRODS --
-----------

-- ┌─────┐
-- │δ ×̃ δ│
-- └─────┘
timesProds ∷ MMSPProds → MMSPProds → MMSPProds
-- δ₁ +̃ δ₂ = ∏{ ω^̇e | ω^̇e ∈ δ₁} × ∏{ ω^̇e | ω^̇e ∈ δ₂ }
--         ≜ ∏( { ω^̇e | ω^̇e ∈ δ₁ , ω ∉ dom(δ₂) }
--            ∪ { ω^̇e | ω^̇e ∈ δ₂ , ω ∉ dom(δ₁) }
--            ∪ { ω^̇(e₁+e₂) | ω^̇e₁ ∈ δ₁ , ω^̇e₂ ∈ δ₂ } )
timesProds :: MMSPProds -> MMSPProds -> MMSPProds
timesProds (MMSPProds MMSPAtom ⇰ ℕ
δ₁) (MMSPProds MMSPAtom ⇰ ℕ
δ₂) = (MMSPAtom ⇰ ℕ) -> MMSPProds
MMSPProds ((MMSPAtom ⇰ ℕ) -> MMSPProds) -> (MMSPAtom ⇰ ℕ) -> MMSPProds
forall a b. (a -> b) -> a -> b
$ MMSPAtom ⇰ ℕ
δ₁ (MMSPAtom ⇰ ℕ) -> (MMSPAtom ⇰ ℕ) -> MMSPAtom ⇰ ℕ
forall a. Plus a => a -> a -> a
+ MMSPAtom ⇰ ℕ
δ₂