----------------------------------------------------------------------------
-- |
-- Module      :  LargeCardinalHierarchy
-- Copyright   :  (c) Stephen E. A. Britton 2010
-- License     :  BSD-style (see LICENSE)
--
-- Maintainer  :  Stephen E. A. Britton (sbritton (at) cbu (dot) edu)
-- Stability   :  unstable
-- Portability :  OS independent
--
-- The /LargeCardinalHierarchy/ module defines a recursively enumerable,
-- countably infinite subclass of the logically
-- (consistent) maximal transfinite set-theoretic universe
-- ZFC+Con(LargeCardinals) (Zermelo-Frankel Set Theory + Axiom of Choice
-- + All known large cardinals consistent with ZFC) via data constructors
-- for each large cardinal within the hierarchy and functions over them.
-- The algebraic data type 'Card' is a Haskell implementation
-- of the set theoretic proper class of all cardinals, /Card/.
-- 'Card' has value constructors for a countably infinite (aleph-null sized)
-- subset of every cardinal type of all known large cardinals consistent
-- with ZFC (Zermelo-Frankel Set Theory + Axiom of Choice) or,
-- equivalently, ZF+GCH (Zermelo-Frankel Set Theory + Generalized Continuum Hypothesis).
--
-----------------------------------------------------------------------------

  module LargeCardinalHierarchy where

  import Control.Monad
       
  data Card = Card Integer
            | Aleph Card
            | WeaklyInaccessible Card
            | StronglyInaccessible Card
            | AlphaInaccessible Card
            | HyperInaccessible Card
            | Hyper2Inaccessible Card
            | WeaklyMahlo Card
            | StronglyMahlo Card
            | AlphaMahlo Card
            | HyperMahlo Card
            | Reflecting Card
            | PiIndescribable (Int, Int) Card
            | TotallyIndescribable Card
            | NuIndescribable Card
            | LambdaUnfoldable Card
            | Unfoldable Card
            | LambdaShrewd Card
            | Shrewd Card
            | Ethereal Card
            | Subtle Card
            | AlmostIneffable Card
            | Ineffable Card
            | NIneffable Card
            | TotallyIneffable Card
            | Remarkable Card
            | AlphaErdos Card
            | GammaErdos Card
            | AlmostRamsey Card
            | Jonsson Card
            | Rowbottom Card
            | Ramsey Card
            | IneffablyRamsey Card
            | Measurable Card
            | ZeroDagger Card
            | LambdaStrong Card
            | Strong Card
            | Woodin Card
            | WeaklyHyperWoodin Card
            | Shelah Card
            | HyperWoodin Card
            | Superstrong Card
            | Subcompact Card
            | StronglyCompact Card
            | Supercompact Card
            | EtaExtendible Card
            | Extendible Card
            | Vopenka Card
            | NSuperstrong Card
            | NAlmostHuge Card
            | NSuperAlmostHuge Card
            | NHuge Card
            | NSuperHuge Card
            | RankIntoRank Card
            | Reinhardt Card
            | TAV          -- the supremum of Card, class of all cardinals
            | AbsoluteInfinity
              deriving (Eq, Ord, Show)

  {-|
    'apply' is a binary higher-order function
     that takes a function /f/ and a list of type /x/ values, [x],
     and returns a new list of values derived from the application of /f/ to
     each of the /x/ values within [x].
  -}
  apply f [x] = [f x]
  apply f (x:xs) = [f x] ++ apply f xs

  {-|
     'zero' is /the/ unique nullary function within the
     /LargeCardinalHierarchy/ module that returns the additive identity element
     (and multiplicative absorbing element within the class of all cardinals),
     cardinal 0, via the 'Card' constructor.
  -}
  zero :: Card
  zero = Card 0

  {-|
     'one' is /the/ unique nullary function within the
     /LargeCardinalHierarchy/ module that returns the multiplicative identity element
     within the class of all cardinals, cardinal 1, via the 'Card' constructor.
  -}
  one :: Card
  one = Card 1

  {-|
     'absolute' is a /type synonym/ (nullary function) for /AbsoluteInfinity/; the
     supremum of the class of all cardinals, 'Card'.
  -}
  absolute :: Card
  absolute = AbsoluteInfinity

  {-|
     'zeros' is a nullary function that returns a countably-infinite (aleph-null sized)
     sequence (a /stream/) of cardinal zeros.
  -}
  zeros :: [Card]
  zeros = repeat zero

  {-|
     'ones' is a nullary function that returns a countably-infinite (aleph-null sized)
     sequence (a /stream/) of cardinal ones.
  -}
  ones :: [Card]
  ones = repeat one

  {-|
     'alefz' is a unary function that takes an 'Int' /n/ and
     returns an /n/-element list of the first /n/ aleph numbers enumerating from
     aleph-null.
  -}
  alefz :: Int -> [Card]
  alefz n = take n (order 1 Aleph)

  {-|
     'tavs' is a nullary function that returns a countably-infinite (aleph-null sized)
     sequence (a /stream/) of 'TAV's; 'TAV' being the symbol for the absolutely infinite
     supremum of the class of all cardinals, 'Card'.
  -}
  tavs :: [Card]
  tavs = repeat TAV

  {-|
     'absolutes' is a nullary function that returns a countably-infinite (aleph-null sized)
     sequence (a /stream/) of 'AbsoluteInfinity's; 'AbsoluteInfinity' being the
     /cardinality/ the class of all cardinals, 'Card'.
  -}
  absolutes :: [Card]
  absolutes = repeat absolute

  {-|
     'absoluteInfinities' is a /type synonym/ (nullary function) for 'absolutes'.
  -}
  absoluteInfinities :: [Card]
  absoluteInfinities = absolutes

  {-|
     '(#)' is binary function from ('Card', 'Card') to 'Card'.
     '(#)' takes two cardinal numbers and returns their binary sum.
     Category-theoretically speaking, '(#)' is a /coproduct/ in the class of
     all cardinals, 'Card'.
   -}
  (#) :: Card -> Card -> Card
  (#) (Card m)         (Card n)         = Card (m + n)
  (#) m                n                = max m n

  {-|
     '(#.)' is a unary (or, multiary) function from ['Card'] to 'Card'.
     '(#.)' takes a list of cardinal numbers and returns their multiary sum.
     Category-theoretically speaking, '(#.)' is a /coproduct/ in the class of
     all cardinals, 'Card'.
   -}
  (#.) :: [Card] -> Card
  (#.) xs = foldl (#) (Card 0) xs

  {-|
     '(*.)' is a binary function from ('Card', 'Card') to 'Card'.
     '(*.)' takes two cardinal numbers and returns their binary product.
   -}
  (*.) :: Card -> Card -> Card
  (*.) (Card m)         (Card n)         = Card (m * n)
  (*.) m                (Card 0)         = Card 0
  (*.) (Card 0)         n                = Card 0
  (*.) m                n                = max m n

  {-|
     'x' is a unary (or, multiary) function from ['Card'] to 'Card'.
     'x' takes a list of cardinal numbers and returns their multiary product.
   -}
  x :: [Card] -> Card
  x xs = foldl (*.) (Card 1) xs


  {-|
     '(^.)' is a binary function from ('Card','Card') to 'Card'.
     '(^.)' take two cardinal numbers and returns the power of the
     zeroth cardinal number exponentiated to the first cardinal number.
   -}
  (^.) :: Card -> Card -> Card
  (^.) (Card m)         (Card n)         = Card (m ^ n)
  (^.) (Card m)         (Aleph (Card n)) = if m == 0 || m == 1
                                              then Card m
                                              else Aleph (Card (n + 1))
  (^.) (Aleph (Card m)) (Card n)         = if n == 0
                                              then Card 1
                                              else Aleph (Card m)
  (^.) (Aleph (Card m)) (Aleph (Card n)) = if m > n
                                              then Aleph (Card m)
                                              else Aleph (Card (n + 1))
  (^.) (Card m)         TAV              = if m == 0 || m == 1
                                              then Card m
                                              else TAV
  (^.) TAV              (Card n)         = if n == 0
                                              then Card 1
                                              else TAV

  {-|
     'cp' is a binary function from [a] & [b] to [(a, b)].
     'cp' takes two /lists/ of elements and returns the
     list of all ordered pairs of elements between the two lists.
     'cp' is the /Cartesian product/ operator.
   -}
  cp :: [a] -> [b] -> [(a, b)]
  cp as bs = [(a, b) | a <- as, b <- bs]

  {-|
     'cartesianProduct' is a binary function from [a] & [b] to [(a, b)].
     'cartesianProduct' takes two lists of elements and returns the
     list of all ordered pairs of elements between the two lists
     'cartesianProduct' is the /Cartesian product/ operator.
   -}
  cartesianProduct :: [a] -> [b] -> [(a, b)]
  cartesianProduct = cp

  {-|
     'powerList' is a unary function from [a] -> [[a]].
     'powerList' takes a list of elements and returns the list of all sublists
     of that list. 'powerList' is a /canonical/ example of Haskell's facilitation
     in expressing functions elegantly.   
  -}
  powerList :: [a] -> [[a]]
  powerList = filterM (const [True,False])

  {-|
     'ascend' is a unary function from 'Integer' to ['Card'].
     'ascend' takes a natural number /n/ and returns a list of aleph cardinals from
     aleph 0 to aleph n.
   -}
  ascend :: Integer -> [Card]
  ascend 0 = [Aleph (Card 0)]
  ascend n = ascend (n - 1) ++ [Aleph (Card n)]

  {-|
     'descend' is a unary function from 'Integer' to ['Card'].
     'descend' takes a natural number /n/ and returns a list of aleph cardinals from
     aleph n to aleph 0.
   -}
  descend :: Integer -> [Card]
  descend 0 = [Aleph (Card 0)]
  descend n = [Aleph (Card n)] ++ descend (n - 1)

  {-|
     'level' is a ternary function from ('Int', 'Card', 'Integer') to 'Card'.
     'level' takes an 'Int' /n/, a 'Card' value constructor /cons/, and an 'Integer' /m/
     and returns a 'Card' equal to /cons/ '$' /cons/ '$' /cons/ '$' ... '$' 'Card' /m/.
   -}
  level :: Int -> (Card -> Card) -> Integer -> Card
  level 0 cons m = Card m
  level n cons m = cons $ level (n - 1) cons m

  {-|
     'ascent' is a quaternary function from ('Int', 'Card', 'Integer', 'Integer') to
     ['Card']. 'ascent' takes an 'Int' /x/, a 'Card' value constructor /cons/, and
     two 'Integer's /y/ and /z/ and returns a list of 'level' /x/ type
     /cons/ 'Card' values from /y/ to /z/, where /y/ <= /z/.
     'ascent' is a generalization of 'ascend'
     over all data constructors in 'Card'.
   -}
  ascent :: Int -> (Card -> Card) -> Integer -> Integer -> [Card]
  ascent x cons y z = apply (level x cons) [y .. z]

  {-|
     'descent' is a quaternary function from ('Int', 'Card', 'Integer', 'Integer') to
     ['Card']. 'descent' takes an 'Int' /x/, a 'Card' value constructor /cons/, and
     two 'Integer's /y/ and /z/ and returns a list of 'level' /x/ type
     /cons/ 'Card' values from /y/ to /z/, where /y/ >= /z/.
     'descent' is a generalization of 'descend'
     over all data constructors in 'Card'.
   -}
  descent :: Int -> (Card -> Card) -> Integer -> Integer -> [Card]
  descent x cons y z = apply (level x cons) [y, y - 1 .. z]

  {-|
     'c' is a unary function that takes an 'Integer' /n/ and
     returns a finite cardinal number, 'Card' /n/.
  -}
  c :: Integer -> Card
  c n = Card n

  {-|
     'alef' is a unary function that takes an 'Integer' /n/ and
     returns a tranfinite aleph number subscripted by cardinal /n/, 'Aleph' /n/.
  -}
  alef :: Integer -> Card
  alef n = aleph 1 n

  {-|
     'aleph' is a binary function from ('Int', 'Integer') to 'Card'.
     'aleph' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'Aleph' whose deepest subscript is /n/.
  -}
  aleph :: Int -> Integer -> Card
  aleph m n = level m Aleph n

  {-|
     'beth' is a binary function from ('Int', 'Integer') to 'Card'.
     'beth' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'Aleph' whose deepest subscript is /n/.
   -}
  beth :: Int -> Integer -> Card
  beth m n = aleph m n

  {-|
     'wInac' is a binary function from ('Int', 'Integer') to 'Card'.
     'wInac' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'WeaklyInaccessible' whose deepest subscript is /n/.
   -}
  wInac :: Int -> Integer -> Card
  wInac m n = level m WeaklyInaccessible n

  -- | 'weaklyInaccessible' is a /function synonym/ for 'wInac'.
  weaklyInaccessible :: Int -> Integer -> Card
  weaklyInaccessible = wInac

  {-|
     'sInac' is a binary function from ('Int', 'Integer') to 'Card'.
     'sInac' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'StronglyInaccessible' whose deepest subscript is /n/.
   -}
  sInac :: Int -> Integer -> Card
  sInac m n = level m StronglyInaccessible n

  -- | 'stronglyInaccessible' is a /function synonym/ for 'sInac'.
  stronglyInaccessible :: Int -> Integer -> Card
  stronglyInaccessible = sInac

  {-|
     'theta' is a binary function from ('Int', 'Integer') to 'Card'.
     'theta' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'StronglyInaccessible' cardinal whose deepest subscript is /n/.
     'theta' is a /function synonym/ for 'sInac'.
   -}
  theta :: Int -> Integer -> Card
  theta = sInac

  {-|
     'aInac' is a binary function from ('Int', 'Integer') to 'Card'.
     'aInac' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'AlphaInaccessible' whose deepest subscript is /n/.
   -}
  aInac :: Int -> Integer -> Card
  aInac m n = level m AlphaInaccessible n

  {-|
     'alphaInaccessible' is a binary function from ('Int', 'Integer') to 'Card'.
     'alphaInaccessible' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'AlphaInaccessible' whose deepest subscript is /n/.
     'alphaInaccessible' is a /function synonym/ for 'aInac'.
   -}
  alphaInaccessible :: Int -> Integer -> Card
  alphaInaccessible = aInac

  {-|
     'hInac' is a binary function from ('Int', 'Integer') to 'Card'.
     'hInac' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'HyperInaccessible' whose deepest subscript is /n/.
   -}
  hInac :: Int -> Integer -> Card
  hInac m n = level m HyperInaccessible n

  {-|
     'hyperInaccessible' is a binary function from ('Int', 'Integer') to 'Card'.
     'hyperInaccessible' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'HyperInaccessible' whose deepest subscript is /n/.
     'hyperInaccessible' is a /function synonym/ for 'hInac'.
   -}
  hyperInaccessible :: Int -> Integer -> Card
  hyperInaccessible = hInac

  {-|
     'nu' is a binary function from ('Int', 'Integer') to 'Card'.
     'nu' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'HyperInaccessible' whose deepest subscript is /n/.
     'nu' is a /function synonym/ for 'hInac'.
   -}
  nu :: Int -> Integer -> Card
  nu = hInac 

  {-|
     'h2Inac' is a binary function from ('Int', 'Integer') to 'Card'.
     'h2Inac' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'Hyper2Inaccessible' whose deepest subscript is /n/.
   -}
  h2Inac :: Int -> Integer -> Card
  h2Inac m n = level m Hyper2Inaccessible n

  {-|
     'hyper2Inaccessible' is a binary function from ('Int', 'Integer') to 'Card'.
     'hyper2Inaccessible' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'Hyper2Inaccessible' whose deepest subscript is /n/.
     'hyper2Inaccessible' is a /function synonym/ for 'h2Inac'.
   -}
  hyper2Inaccessible :: Int -> Integer -> Card
  hyper2Inaccessible = h2Inac

  {-|
     'mu' is a binary function from ('Int', 'Integer') to 'Card'.
     'mu' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'Hyper2Inaccessible' whose deepest subscript is /n/.
     'mu' is a /function synonym/ for 'h2Inac'.
   -}
  mu :: Int -> Integer -> Card
  mu = h2Inac

  {-|
     'wMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
     'wMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'WeaklyMahlo' whose deepest subscript is /n/.
   -}
  wMahlo :: Int -> Integer -> Card
  wMahlo m n = level m WeaklyMahlo n

  {-|
     'weaklyMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
     'weaklyMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'WeaklyMahlo' whose deepest subscript is /n/.
     'weaklyMahlo' is a /function synonym/ for 'wMahlo'.
   -}
  weaklyMahlo :: Int -> Integer -> Card
  weaklyMahlo = wMahlo

  {-|
     'sMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
     'sMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'StronglyMahlo' whose deepest subscript is /n/.
   -}
  sMahlo :: Int -> Integer -> Card
  sMahlo m n = level m StronglyMahlo n

  {-|
     'stronglyMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
     'stronglyMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'StronglyMahlo' whose deepest subscript is /n/.
     'stronglyMahlo' is a /function synonym/ for 'sMahlo'.
   -}
  stronglyMahlo :: Int -> Integer -> Card
  stronglyMahlo = sMahlo

  {-|
     'rho' is a binary function from ('Int', 'Integer') to 'Card'.
     'rho' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     'm' 'level' 'StronglyMahlo' cardinal whose deepest subscript is /n/.
   -}
  rho :: Int -> Integer -> Card
  rho m n = level m StronglyMahlo n

  {-|
     'aMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
     'aMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'AlphaMahlo' whose deepest subscript is /n/.
   -}
  aMahlo :: Int -> Integer -> Card
  aMahlo m n = level m AlphaMahlo n

  {-|
     'alphaMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
     'alphaMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'AlphaMahlo' whose deepest subscript is /n/.
     'alphaMahlo' is a /function synonym/ for 'aMahlo'.
   -}
  alphaMahlo :: Int -> Integer -> Card
  alphaMahlo = aMahlo

  {-|
     'hMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
     'hMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'HyperMahlo' whose deepest subscript is /n/.
   -}     
  hMahlo :: Int -> Integer -> Card  
  hMahlo m n = level m HyperMahlo n

  {-|
     'hyperMahlo' is a binary function from ('Int', 'Integer') to 'Card'.
     'hyperMahlo' takes an 'Int' /m/ and an 'Integer' /n/ and returns an
     /m/ 'level' 'HyperMahlo' whose deepest subscript is /n/.
   -}
  hyperMahlo :: Int -> Integer -> Card
  hyperMahlo = hMahlo

  {-|
    Binary function from (Int, Integer) to Card
    reflect takes an Int m and an Integer n and returns an
    m level reflecting cardinal whose deepest subscript is n
   -}
  reflect :: Int -> Integer -> Card
  reflect m n = level m Reflecting n

  reflecting :: Int -> Integer -> Card
  reflecting = reflect

  {-|
    Binary function from (Int, Int, Int, Integer) to Card
    pii takes an Int x, an Int y, an Int m, and an Integer n
    and returns the m level pi-(x, y)-indescribable cardinal
    whose deepest subscript is n
   -}
  pii :: Int -> Int -> Int -> Integer -> Card
  pii x y m n = level m (PiIndescribable (x, y)) n

  piIndesc :: Int -> Int -> Int -> Integer -> Card
  piIndesc = pii

  piIndescribable :: Int -> Int -> Int -> Integer -> Card
  piIndescribable = pii

  ti :: Int -> Integer -> Card
  ti m n = level m TotallyIndescribable n


  totalIndesc :: Int -> Integer -> Card
  totalIndesc = ti

  totallyIndescribable :: Int -> Integer -> Card
  totallyIndescribable = ti 

  ni :: Int -> Integer -> Card
  ni m n = level m NuIndescribable n        

  nuIndesc :: Int -> Integer -> Card
  nuIndesc = ni

  nuIndescribable :: Int -> Integer -> Card
  nuIndescribable = ni

  lambdaUnfold :: Int -> Integer -> Card
  lambdaUnfold m n = level m LambdaUnfoldable n

  lambdaUnfoldable :: Int -> Integer -> Card
  lambdaUnfoldable = lambdaUnfold

  unfold :: Int -> Integer -> Card
  unfold m n = level m Unfoldable n

  unfoldable :: Int -> Integer -> Card
  unfoldable = unfold

  lambdaShrewd :: Int -> Integer -> Card
  lambdaShrewd m n = level m LambdaShrewd n

  shrewd :: Int -> Integer -> Card
  shrewd m n = level m Shrewd n

  {-|
    Binary function from (Int, Integer) to Card
    ether takes an Int m and an Integer n and returns an
    m level ethereal cardinal whose deepest subscript is n
   -}
  ether :: Int -> Integer -> Card
  ether m n = level m Ethereal n

  ethereal :: Int -> Integer -> Card
  ethereal = ether

  {-|
    Binary function from (Int, Integer) to Card
    subtle takes an Int m and an Integer n and returns an
    m level subtle cardinal whose deepest subscript is n
   -}
  subtle :: Int -> Integer -> Card
  subtle m n = level m Subtle n

  almostIneff :: Int -> Integer -> Card
  almostIneff m n = level m AlmostIneffable n

  almostIneffable :: Int -> Integer -> Card
  almostIneffable = almostIneff

  ineff :: Int -> Integer -> Card
  ineff m n = level m Ineffable n

  ineffable :: Int -> Integer -> Card
  ineffable = ineff

  nIneff :: Int -> Integer -> Card
  nIneff m n = level m NIneffable n

  nIneffable :: Int -> Integer -> Card
  nIneffable = nIneff

  totalIneff :: Int -> Integer -> Card
  totalIneff m n = level m TotallyIneffable n

  totallyIneffable :: Int -> Integer -> Card
  totallyIneffable = totalIneff

  remark :: Int -> Integer -> Card
  remark m n = level m Remarkable n

  remarkable :: Int -> Integer -> Card
  remarkable = remark

  aErdos :: Int -> Integer -> Card
  aErdos m n = level m AlphaErdos n

  alphaErdos :: Int -> Integer -> Card
  alphaErdos = aErdos

  gamma :: Int -> Integer -> Card
  gamma m n = level m GammaErdos n

  gErdos :: Int -> Integer -> Card
  gErdos = gamma

  gammaErdos :: Int -> Integer -> Card
  gammaErdos = gamma

  aRamsey :: Int -> Integer -> Card
  aRamsey m n = level m AlmostRamsey n

  almostRamsey :: Int -> Integer -> Card
  almostRamsey = aRamsey

  jonsson :: Int -> Integer -> Card
  jonsson m n = level m Jonsson n

  rowbottom :: Int -> Integer -> Card
  rowbottom m n = level m Rowbottom n

  ramsey :: Int -> Integer -> Card
  ramsey m n = level m Ramsey n

  iRamsey :: Int -> Integer -> Card
  iRamsey m n = level m IneffablyRamsey n

  ineffablyRamsey :: Int -> Integer -> Card
  ineffablyRamsey = iRamsey

  measure :: Int -> Integer -> Card
  measure m n = level m Measurable n

  measurable :: Int -> Integer -> Card
  measurable = measure
    
  {-|
    Binary function from (Int, Integer) to Card
    kappa takes an Int m and an Integer n and returns an
    m level measurable cardinal whose deepest subscript is n
   -}
  kappa :: Int -> Integer -> Card
  kappa = measure

  zeroDag :: Int -> Integer -> Card
  zeroDag m n = level m ZeroDagger n

  zeroDagger :: Int -> Integer -> Card
  zeroDagger = zeroDag

  lambdaStrong :: Int -> Integer -> Card
  lambdaStrong m n = level m LambdaStrong n

  strong :: Int -> Integer -> Card
  strong m n = level m Strong n

  woodin :: Int -> Integer -> Card
  woodin m n = level m Woodin n

  whWoodin :: Int -> Integer -> Card
  whWoodin m n = level m WeaklyHyperWoodin n

  weaklyHyperWoodin :: Int -> Integer -> Card
  weaklyHyperWoodin = whWoodin

  shelah :: Int -> Integer -> Card
  shelah m n = level m Shelah n

  hWoodin :: Int -> Integer -> Card
  hWoodin m n = level m HyperWoodin n

  hyperWoodin :: Int -> Integer -> Card
  hyperWoodin = hWoodin

  ss :: Int -> Integer -> Card
  ss m n = level m Superstrong n

  supStrong :: Int -> Integer -> Card
  supStrong = ss

  superstrong :: Int -> Integer -> Card
  superstrong = ss

  superStrong :: Int -> Integer -> Card
  superStrong = ss

  subcompact :: Int -> Integer -> Card
  subcompact m n = level m Subcompact n

  stronglyCompact :: Int -> Integer -> Card
  stronglyCompact m n = level m StronglyCompact n

  supCompact :: Int -> Integer -> Card
  supCompact m n = level m Supercompact n

  superCompact :: Int -> Integer -> Card
  superCompact = supCompact

  eta :: Int -> Integer -> Card
  eta m n = level m EtaExtendible n

  etaExtend :: Int -> Integer -> Card
  etaExtend = eta

  etaExtendible :: Int -> Integer -> Card
  etaExtendible = eta

  ex :: Int -> Integer -> Card
  ex m n = level m Extendible n

  extend :: Int -> Integer -> Card
  extend = ex

  extendible :: Int -> Integer -> Card
  extendible = ex

  vopenka :: Int -> Integer -> Card
  vopenka m n = level m Vopenka n

  nss :: Int -> Integer -> Card
  nss m n = level m NSuperstrong n

  nSuperstrong :: Int -> Integer -> Card
  nSuperstrong = nss

  nah :: Int -> Integer -> Card
  nah m n = level m NAlmostHuge n

  nAlmostHuge :: Int -> Integer -> Card
  nAlmostHuge = nah

  nsah :: Int -> Integer -> Card
  nsah m n = level m NSuperAlmostHuge n

  nSuperAlmostHuge :: Int -> Integer -> Card
  nSuperAlmostHuge = nsah

  nh :: Int -> Integer -> Card
  nh m n = level m NHuge n

  nHuge :: Int -> Integer -> Card
  nHuge = nh

  nsh :: Int -> Integer -> Card
  nsh m n = level m NSuperHuge n

  nSuperHuge :: Int -> Integer -> Card
  nSuperHuge = nsh

  rank :: Int -> Integer -> Card
  rank m n = level m RankIntoRank n

  {-|
    Binary function from (Int, Integer) to Card
    lambda takes an Int m and an Integer n and returns an
    m level rank-into-rank cardinal whose deepest subscript is n
   -}
  lambda :: Int -> Integer -> Card
  lambda = rank

  rankIntoRank :: Int -> Integer -> Card
  rankIntoRank = rank

  reinhardt :: Int -> Integer -> Card
  reinhardt m n = level m Reinhardt n

  {-|
     Binary function from 'Int' x 'Card' to Card
     order takes an Int m and a Card card and returns the
     countably infinite list of level m card(s) indexed over
     the natural numbers [0..]. That is, order returns
     [(card m 0), (card m 1), (card m 2), (card m 3), . . .]

     order increases 'linearly' over its second argument
     keeping its first argument constant. order indexes in a
     zero order manner over the natural numbers.
     order m card =
     [(card m 0), (card m 1), (card m 2), (card m 3), . . .]

     fixedpoints increases 'hierarchly' over its first argument
     keeping its second argument constant. fixedpoints indexes
     in a higher order manner over its own arguments.
     fixedpoints m card =
     [(card 1 m), (card 2 m), (card 3 m), (card 4 m), . . .]
   -}
  order :: Int -> (Card -> Card) -> [Card]
  order m card = apply (level m card) [0..]

  {-|
     Binary function from Int x Card to Card
     zeroOrder takes an Int m and a Card card and returns the
     countably infinite list of level m card(s) indexed over
     the natural numbers [0..]. That is, zeroOrder returns
     [(card m 0), (card m 1), (card m 2), (card m 3), . . .]

     zeroOrder increases 'linearly' over its second argument
     keeping its first argument constant. zeroOrder indexes in a
     zero order manner over the natural numbers.
     zeroOrder m card =
     [(card m 0), (card m 1), (card m 2), (card m 3), . . .]

     zeroOrder 1 Aleph =
     [Aleph(0), Aleph(1), Aleph(2), Aleph(3), . . .]

     higherOrder increases 'hierarchly' over its first argument
     keeping its second argument constant. higherOrder indexes
     in a higher order manner over its own arguments.
     higherOrder m card =
     [(card 1 m), (card 2 m), (card 3 m), (card 4 m), . . .]

     higherOrder 1 Aleph =
     [(1), Aleph(1), Aleph(Aleph(1)), Aleph(Aleph(Aleph(1))), . . .]
   -}
  zeroOrder :: Int -> (Card -> Card) -> [Card]
  zeroOrder = order

  {-|
     Binary function from Int x Card to Card
     orderClass takes an Int m and a Card card and returns the
     countably infinite list of level m card(s) indexed over
     the natural numbers [0..]. That is, orderClass returns
     [(card m 0), (card m 1), (card m 2), (card m 3), . . .]
     orderClass is identical to order
   -}
  orderClass :: Int -> (Card -> Card) -> [Card]
  orderClass = order

  {-|
    Unary function from Card to Card
    club takes a Card value constructor card and returns
    the countably infinite list of type card Card fixed points
    indexed over the natural numbers [0..]. That is, club returns
    [(card 1 0), (card 2 0), (card 3 0), . . .]
    club is an implementation of the normal function f: Ordinals -> Ordinals
    that defines a closed and unbounded (club) class of ordinal
    fixed points according to the "Fixed point lemma for normal functions"
   -}
  club :: (Card -> Card) -> [Card]
  club card = iterate card (Card 0)

  {-|
    Binary function from Int x Card to Card
    fixedpoints takes an Int m and a Card value constructor card and returns
    the countably infinite list of type card Card fixed points
    indexed over the natural number m. That is, fixedpoints returns
    [(card 1 m), (card 2 m), (card 3 m), . . .]
    fixedpoints is an implementation of the normal function
    f: Ordinals -> Ordinals
    that defines a closed and unbounded (club) class of ordinal
    fixed points according to the "Fixed point lemma for normal functions"

     fixedpoints increases 'hierarchly' over its first argument
     keeping its second argument constant. fixedpoints indexes
     in a higher order manner over its own arguments.
     fixedpoints m card =
     [(card 1 m), (card 2 m), (card 3 m), (card 4 m), . . .]

     order increases 'linearly' over its second argument
     keeping its first argument constant. order indexes in a
     zero order manner over the natural numbers.
     order m card =
     [(card m 0), (card m 1), (card m 2), (card m 3), . . .]  
   -}
  fixedpoints :: Integer -> (Card -> Card) -> [Card]
  fixedpoints m card = iterate card (Card m)

  {-|
    Binary function from Int x Card to Card
    higherOrder takes an Int m and a Card value constructor card and returns
    the countably infinite list of type card Card fixed points
    indexed over the natural number m. That is, higherOrder returns
    [(card 1 m), (card 2 m), (card 3 m), . . .]
    higherOrder is an implementation of the normal function
    f: Ordinals -> Ordinals
    that defines a closed and unbounded (club) class of ordinal
    fixed points according to the "Fixed point lemma for normal functions"

     higherOrder increases 'hierarchly' over its first argument
     keeping its second argument constant. higherOrder indexes
     in a higher order manner over its own arguments.
     higherOrder m card =
     [(card 1 m), (card 2 m), (card 3 m), (card 4 m), . . .]

     higherOrder 1 Aleph =
     [(1), Aleph(1), Aleph(Aleph(1)), Aleph(Aleph(Aleph(1))), . . .]

     zeroOrder increases 'linearly' over its second argument
     keeping its first argument constant. zeroOrder indexes in a
     zero order manner over the natural numbers.
     zeroOrder m card =
     [(card m 0), (card m 1), (card m 2), (card m 3), . . .]

     zeroOrder 1 Aleph =
     [Aleph(0), Aleph(1), Aleph(2), Aleph(3), . . .]
   -}
  higherOrder :: Integer -> (Card -> Card) -> [Card]
  higherOrder = fixedpoints

  {-|
    Quaternary function from Int x Card x Int x Int to [Card]
    fromTo takes an Int ord, a Card value constructor cons, an Int m,
    and an Int n and returns the list of type cons Card(s) of order
    ord indexed from m to n. That is, fromTo returns
    [(cons ord m), . . . , (cons ord n)]
    fromTo ord cons m n = descent ord cons m n
   -}
  fromTo :: Int -> (Card -> Card) -> Int -> Int -> [Card]
  fromTo ord cons m n = drop m (take (n + 1) (order ord cons))

  alephs :: Int -> [Card]
  alephs n = order n Aleph

  alefs :: Integer -> [Card]
  alefs n = fixedpoints n Aleph

  wInacs :: Int -> [Card]
  wInacs n = order n WeaklyInaccessible

  weaklyInaccessibles :: Int -> [Card]
  weaklyInaccessibles = wInacs

  wInacz :: Integer -> [Card]
  wInacz n = fixedpoints n WeaklyInaccessible

  weaklyInaccessiblez :: Integer -> [Card]
  weaklyInaccessiblez = wInacz

  sInacs :: Int -> [Card]
  sInacs n = order n StronglyInaccessible

  stronglyInaccessibles :: Int -> [Card]
  stronglyInaccessibles = sInacs

  sInacz :: Integer -> [Card]
  sInacz n = fixedpoints n StronglyInaccessible

  stronglyInaccessiblez :: Integer -> [Card]
  stronglyInaccessiblez = sInacz

  aInacs :: Int -> [Card]
  aInacs n = order n AlphaInaccessible

  alphaInaccessibles :: Int -> [Card]
  alphaInaccessibles = aInacs

  aInacz :: Integer -> [Card]
  aInacz n = fixedpoints n AlphaInaccessible

  alphaInaccessiblez :: Integer -> [Card]
  alphaInaccessiblez = aInacz

  hInacs :: Int -> [Card]
  hInacs n = order n HyperInaccessible

  hyperInaccessibles :: Int -> [Card]
  hyperInaccessibles = hInacs

  hInacz :: Integer -> [Card]
  hInacz n = fixedpoints n HyperInaccessible

  hyperInaccessiblez :: Integer -> [Card]
  hyperInaccessiblez = hInacz

  h2Inacs :: Int -> [Card]
  h2Inacs n = order n Hyper2Inaccessible

  hyper2Inaccessibles :: Int -> [Card]
  hyper2Inaccessibles = h2Inacs

  h2Inacz :: Integer -> [Card]
  h2Inacz n = fixedpoints n Hyper2Inaccessible

  hyper2Inaccessiblez :: Integer -> [Card]
  hyper2Inaccessiblez = h2Inacz

  wMahlos :: Int -> [Card]
  wMahlos n = order n WeaklyMahlo

  weaklyMahlos :: Int -> [Card]
  weaklyMahlos = wMahlos

  wMahloz :: Integer -> [Card]
  wMahloz n = fixedpoints n WeaklyMahlo

  weaklyMahloz :: Integer -> [Card]
  weaklyMahloz = wMahloz

  sMahlos :: Int -> [Card]
  sMahlos n = order n StronglyMahlo

  stronglyMahlos :: Int -> [Card]
  stronglyMahlos = sMahlos

  sMahloz :: Integer -> [Card]
  sMahloz n = fixedpoints n StronglyMahlo

  stronglyMahloz :: Integer -> [Card]
  stronglyMahloz = sMahloz

  aMahlos :: Int -> [Card]
  aMahlos n = order n AlphaMahlo

  alphaMahlos :: Int -> [Card]
  alphaMahlos = aMahlos

  aMahloz :: Integer -> [Card]
  aMahloz n = fixedpoints n AlphaMahlo

  alphaMahloz :: Integer -> [Card]
  alphaMahloz = aMahloz

  hMahlos :: Int -> [Card]
  hMahlos n = order n HyperMahlo

  hyperMahlos :: Int -> [Card]
  hyperMahlos = hMahlos

  hMahloz :: Integer -> [Card]
  hMahloz n = fixedpoints n HyperMahlo

  hyperMahloz :: Integer -> [Card]
  hyperMahloz = hMahloz

  reflections :: Int -> [Card]
  reflections n = order n Reflecting

  reflexions :: Integer -> [Card]
  reflexions n = fixedpoints n Reflecting

  piis :: Int -> Int -> Int -> [Card]
  piis super sub order = apply (pii super sub order) [0..]

  piIndescribables :: Int -> Int -> Int -> [Card]
  piIndescribables = piis

  piiz :: Int -> Int -> Integer -> [Card]
  piiz super sub index = iterate (PiIndescribable (super, sub)) (Card index)

  piIndescribablez :: Int -> Int -> Integer -> [Card]
  piIndescribablez = piiz

  tis :: Int -> [Card]
  tis n = order n TotallyIndescribable

  totallyIndescribables :: Int -> [Card]
  totallyIndescribables = tis

  tiz :: Integer -> [Card]
  tiz n = fixedpoints n TotallyIndescribable

  totallyIndescribablez :: Integer -> [Card]
  totallyIndescribablez = tiz

  nis :: Int -> [Card]
  nis n = order n NuIndescribable

  nuIndescribables :: Int -> [Card]
  nuIndescribables = nis

  niz :: Integer -> [Card]
  niz n = fixedpoints n NuIndescribable

  nuIndescribablez :: Integer -> [Card]
  nuIndescribablez = niz

  lambdaUnfolds :: Int -> [Card]
  lambdaUnfolds n = order n LambdaUnfoldable

  lambdaUnfoldables :: Int -> [Card]
  lambdaUnfoldables = lambdaUnfolds

  lambdaUnfoldz :: Integer -> [Card]
  lambdaUnfoldz n = fixedpoints n LambdaUnfoldable

  lambdaUnfoldablez :: Integer -> [Card]
  lambdaUnfoldablez = lambdaUnfoldz

  unfolds :: Int -> [Card]
  unfolds n = order n Unfoldable

  unfoldables :: Int -> [Card]
  unfoldables = unfolds

  unfoldz :: Integer -> [Card]
  unfoldz n = fixedpoints n Unfoldable

  unfoldablez :: Integer -> [Card]
  unfoldablez = unfoldz

  lambdaShrewds :: Int -> [Card]
  lambdaShrewds n = order n LambdaShrewd

  lambdaShrewdz :: Integer -> [Card]
  lambdaShrewdz n = fixedpoints n LambdaShrewd

  shrewds :: Int -> [Card]
  shrewds n = order n Shrewd

  shrewdz :: Integer -> [Card]
  shrewdz n = fixedpoints n Shrewd

  ethers :: Int -> [Card]
  ethers n = order n Ethereal

  ethereals :: Int -> [Card]
  ethereals = ethers

  etherz :: Integer -> [Card]
  etherz n = fixedpoints n Ethereal

  etherealz :: Integer -> [Card]
  etherealz = etherz

  subtles :: Int -> [Card]
  subtles n = order n Subtle

  subtlez :: Integer -> [Card]
  subtlez n = fixedpoints n Subtle

  almostIneffs :: Int -> [Card]
  almostIneffs n = order n AlmostIneffable

  almostIneffables :: Int -> [Card]
  almostIneffables = almostIneffs

  almostIneffz :: Integer -> [Card]
  almostIneffz n = fixedpoints n AlmostIneffable

  almostIneffablez :: Integer -> [Card]
  almostIneffablez = almostIneffz

  ineffs :: Int -> [Card]
  ineffs n = order n Ineffable

  ineffables :: Int -> [Card]
  ineffables = ineffs

  ineffz :: Integer -> [Card]
  ineffz n = fixedpoints n Ineffable

  ineffablez :: Integer -> [Card]
  ineffablez = ineffz

  nIneffs :: Int -> [Card]
  nIneffs n = order n NIneffable

  nIneffables :: Int -> [Card]
  nIneffables = nIneffs

  nIneffz :: Integer -> [Card]
  nIneffz n = fixedpoints n NIneffable

  nIneffablez :: Integer -> [Card]
  nIneffablez = nIneffz

  totalIneffs :: Int -> [Card]
  totalIneffs n = order n TotallyIneffable

  totallyIneffables :: Int -> [Card]
  totallyIneffables = totalIneffs

  totalIneffz :: Integer -> [Card]
  totalIneffz n = fixedpoints n TotallyIneffable

  totallyIneffablez :: Integer -> [Card]
  totallyIneffablez = totalIneffz

  remarkables :: Int -> [Card]
  remarkables n = order n Remarkable

  remarkablez :: Integer -> [Card]
  remarkablez n = fixedpoints n Remarkable

  aErdoss :: Int -> [Card]
  aErdoss n = order n AlphaErdos

  alphaErdoss :: Int -> [Card]
  alphaErdoss = aErdoss

  aErdosz :: Integer -> [Card]
  aErdosz n = fixedpoints n AlphaErdos

  alphaErdosz :: Integer -> [Card]
  alphaErdosz = aErdosz

  gErdoss :: Int -> [Card]
  gErdoss n = order n GammaErdos

  gammaErdoss :: Int -> [Card]
  gammaErdoss = gErdoss

  gErdosz :: Integer -> [Card]
  gErdosz n = fixedpoints n GammaErdos

  gammaErdosz :: Integer -> [Card]
  gammaErdosz = gErdosz

  aRamseys :: Int -> [Card]
  aRamseys n = order n AlmostRamsey

  almostRamseys :: Int -> [Card]
  almostRamseys = aRamseys

  aRamseyz :: Integer -> [Card]
  aRamseyz n = fixedpoints n AlmostRamsey

  almostRamseyz :: Integer -> [Card]
  almostRamseyz = aRamseyz

  jonssons :: Int -> [Card]
  jonssons n = order n Jonsson

  jonssonz :: Integer -> [Card]
  jonssonz n = fixedpoints n Jonsson

  rowbottoms :: Int -> [Card]
  rowbottoms n = order n Rowbottom

  rowbottomz :: Integer -> [Card]
  rowbottomz n = fixedpoints n Rowbottom
  
  ramseys :: Int -> [Card]
  ramseys n = order n Ramsey

  ramseyz :: Integer -> [Card]
  ramseyz n = fixedpoints n Ramsey

  iRamseys :: Int -> [Card]
  iRamseys n = order n IneffablyRamsey

  ineffablyRamseys :: Int -> [Card]
  ineffablyRamseys = iRamseys

  iRamseyz :: Integer -> [Card]
  iRamseyz n = fixedpoints n IneffablyRamsey

  ineffablyRamseyz :: Integer -> [Card]
  ineffablyRamseyz = iRamseyz

  measures :: Int -> [Card]
  measures n = order n Measurable

  measurables :: Int -> [Card]
  measurables = measures

  measurez :: Integer -> [Card]
  measurez n = fixedpoints n Measurable

  measurablez :: Integer -> [Card]
  measurablez = measurez

  zeroDags :: Int -> [Card]
  zeroDags n = order n ZeroDagger

  zeroDaggers :: Int -> [Card]
  zeroDaggers = zeroDags

  zeroDagz :: Integer -> [Card]
  zeroDagz n = fixedpoints n ZeroDagger

  zeroDaggerz :: Integer -> [Card]
  zeroDaggerz = zeroDagz

  lambdaStrongs :: Int -> [Card]
  lambdaStrongs n = order n LambdaStrong

  lambdaStrongz :: Integer -> [Card]
  lambdaStrongz n = fixedpoints n LambdaStrong

  strongs :: Int -> [Card]
  strongs n = order n Strong

  strongz :: Integer -> [Card]
  strongz n = fixedpoints n Strong

  woodins :: Int -> [Card]
  woodins n = order n Woodin

  woodinz :: Integer -> [Card]
  woodinz n = fixedpoints n Woodin

  whWoodins :: Int -> [Card]
  whWoodins n = order n WeaklyHyperWoodin

  weaklyHyperWoodins :: Int -> [Card]
  weaklyHyperWoodins = whWoodins

  whWoodinz :: Integer -> [Card]
  whWoodinz n = fixedpoints n WeaklyHyperWoodin

  weaklyHyperWoodinz :: Integer -> [Card]
  weaklyHyperWoodinz = whWoodinz

  shelahs :: Int -> [Card]
  shelahs n = order n Shelah

  shelahz :: Integer -> [Card]
  shelahz n = fixedpoints n Shelah

  hWoodins :: Int -> [Card]
  hWoodins n = order n HyperWoodin

  hyperWoodins :: Int -> [Card]
  hyperWoodins = hWoodins

  hWoodinz :: Integer -> [Card]
  hWoodinz n = fixedpoints n HyperWoodin

  hyperWoodinz :: Integer -> [Card]
  hyperWoodinz = hWoodinz

  sss :: Int -> [Card]
  sss n = order n Superstrong

  superstrongs :: Int -> [Card]
  superstrongs = sss

  ssz :: Integer -> [Card]
  ssz n = fixedpoints n Superstrong

  superstrongz :: Integer -> [Card]
  superstrongz = ssz

  scs :: Int -> [Card]
  scs n = order n Subcompact

  subcompacts :: Int -> [Card]
  subcompacts = scs

  scz :: Integer -> [Card]
  scz n = fixedpoints n Subcompact

  subcompactz :: Integer -> [Card]
  subcompactz = scz

  stronglycompacts :: Int -> [Card]
  stronglycompacts n = order n StronglyCompact

  stronglycompactz :: Integer -> [Card]
  stronglycompactz n = fixedpoints n StronglyCompact

  supercompacts :: Int -> [Card]
  supercompacts n = order n Supercompact

  supercompactz :: Integer -> [Card]
  supercompactz n = fixedpoints n Supercompact

  etas :: Int -> [Card]
  etas n = order n EtaExtendible

  etaExtendibles :: Int -> [Card]
  etaExtendibles = etas

  etaz :: Integer -> [Card]
  etaz n = fixedpoints n EtaExtendible

  etaExtendiblez :: Integer -> [Card]
  etaExtendiblez = etaz

  extends :: Int -> [Card]
  extends n = order n Extendible

  extendibles :: Int -> [Card]
  extendibles = extends

  extendz :: Integer -> [Card]
  extendz n = fixedpoints n Extendible

  extendiblez :: Integer -> [Card]
  extendiblez = extendz

  vopenkas :: Int -> [Card]
  vopenkas n = order n Vopenka

  vopenkaz :: Integer -> [Card]
  vopenkaz n = fixedpoints n Vopenka

  nsss :: Int -> [Card]
  nsss n = order n NSuperstrong

  nSuperstrongs :: Int -> [Card]
  nSuperstrongs = nsss

  nssz :: Integer -> [Card]
  nssz n = fixedpoints n NSuperstrong

  nSuperstrongz :: Integer -> [Card]
  nSuperstrongz = nssz

  nahs :: Int -> [Card]
  nahs n = order n NAlmostHuge

  nAlmostHuges :: Int -> [Card]
  nAlmostHuges = nahs

  nahz :: Integer -> [Card]
  nahz n = fixedpoints n NAlmostHuge

  nAlmostHugez :: Integer -> [Card]
  nAlmostHugez = nahz

  nsahs :: Int -> [Card]
  nsahs n = order n NSuperAlmostHuge

  nSuperAlmostHuges :: Int -> [Card]
  nSuperAlmostHuges = nsahs

  nsahz :: Integer -> [Card]
  nsahz n = fixedpoints n NSuperAlmostHuge

  nSuperAlmostHugez :: Integer -> [Card]
  nSuperAlmostHugez = nsahz

  nHuges :: Int -> [Card]
  nHuges n = order n NHuge

  nHugez :: Integer -> [Card]
  nHugez n = fixedpoints n NHuge

  nshs :: Int -> [Card]
  nshs n = order n NSuperHuge

  nSuperHuges :: Int -> [Card]
  nSuperHuges = nshs

  nshz :: Integer -> [Card]
  nshz n = fixedpoints n NSuperHuge

  nSuperHugez :: Integer -> [Card]
  nSuperHugez = nshz

  ranks :: Int -> [Card]
  ranks n = order n RankIntoRank

  rankIntoRanks :: Int -> [Card]
  rankIntoRanks = ranks

  rankz :: Integer -> [Card]
  rankz n = fixedpoints n RankIntoRank

  rankIntoRankz :: Integer -> [Card]
  rankIntoRankz = rankz

  reinhardts :: Int -> [Card]
  reinhardts n = order n Reinhardt

  reinhardtz :: Integer -> [Card]
  reinhardtz n = fixedpoints n Reinhardt