(Eq [Char])
-- RJ: Issues with TypeClasses? Ord?

module Meas where

import Language.Haskell.Liquid.Prelude
import qualified Data.Map as M
import Data.List (foldl')

--{-# ANN module "spec   $LIQUIDHS/List.spec" #-}
--{-# ANN module "hquals $LIQUIDHS/List.hquals" #-}

----------------------------------------------------------------
--- Step 1: Map each element into key-value list (concatMap) ---
----------------------------------------------------------------

expand          :: (a -> [(k,v)]) -> [a] -> [(k, v)]
forall a b c.
({VV:a | (len([VV]) > 0),
         (len([VV]) >= 0),
         (len([VV]) = 0),
         (~ ((? nonnull([VV])))),
         (? nonnull([VV]))}
 -> {VV:[{VV:({VV:b | (len([VV]) > 0),
                      (len([VV]) >= 0),
                      (len([VV]) = 0),
                      (~ ((? nonnull([VV])))),
                      (? nonnull([VV]))},
              {VV:c | (? nonnull([VV])),
                      (~ ((? nonnull([VV])))),
                      (len([VV]) = 0),
                      (len([VV]) >= 0),
                      (len([VV]) > 0)}) | (len([VV]) > 0),
                                          (len([VV]) >= 0),
                                          (len([VV]) = 0),
                                          (~ ((? nonnull([VV])))),
                                          (? nonnull([VV]))}] | (len([VV]) > 0),
                                                                (len([VV]) >= 0),
                                                                (len([VV]) = 0),
                                                                (~ ((? nonnull([VV])))),
                                                                (? nonnull([VV]))})
-> X1:{VV:[a] | (len([VV]) > 0),(len([VV]) >= 0),(? nonnull([VV]))}
-> [{VV:({VV:b | (len([VV]) = len([X1])),
                 (len([VV]) > 0),
                 (len([VV]) >= 0),
                 (len([VV]) = 0),
                 (~ ((? nonnull([VV])))),
                 (? nonnull([VV]))},
         {VV:c | (len([VV]) = len([X1])),
                 (len([VV]) > 0),
                 (len([VV]) >= 0),
                 (len([VV]) = 0),
                 (~ ((? nonnull([VV])))),
                 (? nonnull([VV]))}) | (len([VV]) = len([X1])),
                                       (len([VV]) > 0),
                                       (len([VV]) >= 0),
                                       (len([VV]) = 0),
                                       (~ ((? nonnull([VV])))),
                                       (? nonnull([VV]))}]expand {VV:a | (len([VV]) > 0),
        (len([VV]) >= 0),
        (len([VV]) = 0),
        (~ ((? nonnull([VV])))),
        (? nonnull([VV]))}
-> {VV:[{VV:({VV:d | (len([VV]) > 0),
                     (len([VV]) >= 0),
                     (len([VV]) = 0),
                     (~ ((? nonnull([VV])))),
                     (? nonnull([VV]))},
             {VV:e | (? nonnull([VV])),
                     (~ ((? nonnull([VV])))),
                     (len([VV]) = 0),
                     (len([VV]) >= 0),
                     (len([VV]) > 0)}) | (len([VV]) > 0),
                                         (len([VV]) >= 0),
                                         (len([VV]) = 0),
                                         (~ ((? nonnull([VV])))),
                                         (? nonnull([VV]))}] | (len([VV]) > 0),
                                                               (len([VV]) >= 0),
                                                               (len([VV]) = 0),
                                                               (~ ((? nonnull([VV])))),
                                                               (? nonnull([VV]))}f []     = forall a.
{VV:[a] | ((? nonnull([VV])) <=> false),
          (nully([VV]) = 0),
          (len([VV]) = 0)}[]
expand f (x:xs) = {VV:[{VV:({VV:c | (len([VV]) = len([x])),
                  (len([VV]) > 0),
                  (len([VV]) >= 0),
                  (len([VV]) = 0),
                  (~ ((? nonnull([VV])))),
                  (? nonnull([VV]))},
          {VV:d | (? nonnull([VV])),
                  (~ ((? nonnull([VV])))),
                  (len([VV]) = 0),
                  (len([VV]) >= 0),
                  (len([VV]) > 0),
                  (len([VV]) = len([x]))}) | (len([VV]) = len([x])),
                                             (len([VV]) > 0),
                                             (len([VV]) >= 0),
                                             (len([VV]) = 0),
                                             (~ ((? nonnull([VV])))),
                                             (? nonnull([VV]))}] | (len([VV]) = len([x])),
                                                                   (len([VV]) > 0),
                                                                   (len([VV]) >= 0),
                                                                   (len([VV]) = 0),
                                                                   (~ ((? nonnull([VV])))),
                                                                   (? nonnull([VV]))}({VV:a | (len([VV]) > 0),
        (len([VV]) >= 0),
        (len([VV]) = 0),
        (~ ((? nonnull([VV])))),
        (? nonnull([VV]))}
-> {VV:[{VV:({VV:d | (len([VV]) > 0),
                     (len([VV]) >= 0),
                     (len([VV]) = 0),
                     (~ ((? nonnull([VV])))),
                     (? nonnull([VV]))},
             {VV:e | (? nonnull([VV])),
                     (~ ((? nonnull([VV])))),
                     (len([VV]) = 0),
                     (len([VV]) >= 0),
                     (len([VV]) > 0)}) | (len([VV]) > 0),
                                         (len([VV]) >= 0),
                                         (len([VV]) = 0),
                                         (~ ((? nonnull([VV])))),
                                         (? nonnull([VV]))}] | (len([VV]) > 0),
                                                               (len([VV]) >= 0),
                                                               (len([VV]) = 0),
                                                               (~ ((? nonnull([VV])))),
                                                               (? nonnull([VV]))}f {VV:a | true,
        (? nonnull([VV])),
        (~ ((? nonnull([VV])))),
        (len([VV]) = 0),
        (len([VV]) >= 0),
        (len([VV]) > 0),
        (VV = x)}x) forall a. [a] -> [a] -> [a]++ (forall a b c.
({VV:a | (len([VV]) > 0),
         (len([VV]) >= 0),
         (len([VV]) = 0),
         (~ ((? nonnull([VV])))),
         (? nonnull([VV]))}
 -> {VV:[{VV:({VV:b | (len([VV]) > 0),
                      (len([VV]) >= 0),
                      (len([VV]) = 0),
                      (~ ((? nonnull([VV])))),
                      (? nonnull([VV]))},
              {VV:c | (? nonnull([VV])),
                      (~ ((? nonnull([VV])))),
                      (len([VV]) = 0),
                      (len([VV]) >= 0),
                      (len([VV]) > 0)}) | (len([VV]) > 0),
                                          (len([VV]) >= 0),
                                          (len([VV]) = 0),
                                          (~ ((? nonnull([VV])))),
                                          (? nonnull([VV]))}] | (len([VV]) > 0),
                                                                (len([VV]) >= 0),
                                                                (len([VV]) = 0),
                                                                (~ ((? nonnull([VV])))),
                                                                (? nonnull([VV]))})
-> X1:{VV:[a] | (len([VV]) > 0),(len([VV]) >= 0),(? nonnull([VV]))}
-> [{VV:({VV:b | (len([VV]) = len([X1])),
                 (len([VV]) > 0),
                 (len([VV]) >= 0),
                 (len([VV]) = 0),
                 (~ ((? nonnull([VV])))),
                 (? nonnull([VV]))},
         {VV:c | (len([VV]) = len([X1])),
                 (len([VV]) > 0),
                 (len([VV]) >= 0),
                 (len([VV]) = 0),
                 (~ ((? nonnull([VV])))),
                 (? nonnull([VV]))}) | (len([VV]) = len([X1])),
                                       (len([VV]) > 0),
                                       (len([VV]) >= 0),
                                       (len([VV]) = 0),
                                       (~ ((? nonnull([VV])))),
                                       (? nonnull([VV]))}]expand {VV:a | (len([VV]) > 0),
        (len([VV]) >= 0),
        (len([VV]) = 0),
        (~ ((? nonnull([VV])))),
        (? nonnull([VV]))}
-> {VV:[{VV:({VV:d | (len([VV]) > 0),
                     (len([VV]) >= 0),
                     (len([VV]) = 0),
                     (~ ((? nonnull([VV])))),
                     (? nonnull([VV]))},
             {VV:e | (? nonnull([VV])),
                     (~ ((? nonnull([VV])))),
                     (len([VV]) = 0),
                     (len([VV]) >= 0),
                     (len([VV]) > 0)}) | (len([VV]) > 0),
                                         (len([VV]) >= 0),
                                         (len([VV]) = 0),
                                         (~ ((? nonnull([VV])))),
                                         (? nonnull([VV]))}] | (len([VV]) > 0),
                                                               (len([VV]) >= 0),
                                                               (len([VV]) = 0),
                                                               (~ ((? nonnull([VV])))),
                                                               (? nonnull([VV]))}f {VV:[b] | (VV = xs)}xs)

----------------------------------------------------------------
--- Step 2: Group By Key ---------------------------------------
----------------------------------------------------------------

group :: (Ord k) => [(k, v)] -> M.Map k [v]
forall a b.
(Ord a)
-> [{VV:({VV:a | (len([VV]) > 0),
                 (len([VV]) >= 0),
                 (len([VV]) = 0),
                 (~ ((? nonnull([VV])))),
                 (? nonnull([VV]))},
         {VV:b | (len([VV]) > 0),
                 (len([VV]) >= 0),
                 (len([VV]) = 0),
                 (~ ((? nonnull([VV])))),
                 (? nonnull([VV]))}) | (len([VV]) > 0),
                                       (len([VV]) >= 0),
                                       (len([VV]) = 0),
                                       (~ ((? nonnull([VV])))),
                                       (? nonnull([VV]))}]
-> {VV:Map
         {VV:a | (len([VV]) > 0),
                 (len([VV]) >= 0),
                 (len([VV]) = 0),
                 (~ ((? nonnull([VV])))),
                 (? nonnull([VV]))}
         {VV:[{VV:b | (len([VV]) > 0),
                      (len([VV]) >= 0),
                      (len([VV]) = 0),
                      (~ ((? nonnull([VV])))),
                      (? nonnull([VV]))}] | (len([VV]) > 0),
                                            (len([VV]) >= 0),
                                            (len([VV]) = 0),
                                            (~ ((? nonnull([VV])))),
                                            (? nonnull([VV]))} | (? nonnull([VV])),
                                                                 (~ ((? nonnull([VV])))),
                                                                 (len([VV]) = 0),
                                                                 (len([VV]) >= 0),
                                                                 (len([VV]) > 0)}group = forall a b. (a -> b -> a) -> a -> [b] -> afoldl' forall a b.
(Ord b)
-> m:Map
       {VV:b | (len([VV]) > 0),
               (len([VV]) >= 0),
               (len([VV]) = 0),
               (~ ((? nonnull([VV])))),
               (? nonnull([VV]))}
       {VV:[{VV:a | (len([VV]) > 0),
                    (len([VV]) >= 0),
                    (len([VV]) = 0),
                    (~ ((? nonnull([VV])))),
                    (? nonnull([VV]))}] | (? nonnull([VV])),
                                          (~ ((? nonnull([VV])))),
                                          (len([VV]) = 0),
                                          (len([VV]) >= 0),
                                          (len([VV]) > 0)}
-> X1:{VV:({VV:b | (len([VV]) = len([m])),
                   (len([VV]) > 0),
                   (len([VV]) >= 0),
                   (len([VV]) = 0),
                   (~ ((? nonnull([VV])))),
                   (? nonnull([VV]))},
           {VV:a | (len([VV]) = len([m])),
                   (len([VV]) > 0),
                   (len([VV]) >= 0),
                   (len([VV]) = 0),
                   (~ ((? nonnull([VV])))),
                   (? nonnull([VV]))}) | (len([VV]) = len([m])),
                                         (len([VV]) > 0),
                                         (len([VV]) >= 0),
                                         (len([VV]) = 0),
                                         (~ ((? nonnull([VV])))),
                                         (? nonnull([VV]))}
-> Map
     {VV:b | (len([VV]) = len([X1])),
             (len([VV]) = len([m])),
             (len([VV]) > 0),
             (len([VV]) >= 0),
             (len([VV]) = 0),
             (~ ((? nonnull([VV])))),
             (? nonnull([VV]))}
     {VV:[{VV:a | (len([VV]) = len([X1])),
                  (len([VV]) = len([m])),
                  (len([VV]) > 0),
                  (len([VV]) >= 0),
                  (len([VV]) = 0),
                  (~ ((? nonnull([VV])))),
                  (? nonnull([VV]))}] | (len([VV]) = len([X1])),
                                        (len([VV]) = len([m])),
                                        (len([VV]) > 0),
                                        (len([VV]) >= 0),
                                        (len([VV]) = 0),
                                        (~ ((? nonnull([VV])))),
                                        (? nonnull([VV]))}addKV  forall a b. Map a bM.empty
  
forall a b.
(Ord b)
-> m:Map
       {VV:b | (len([VV]) > 0),
               (len([VV]) >= 0),
               (len([VV]) = 0),
               (~ ((? nonnull([VV])))),
               (? nonnull([VV]))}
       {VV:[{VV:a | (len([VV]) > 0),
                    (len([VV]) >= 0),
                    (len([VV]) = 0),
                    (~ ((? nonnull([VV])))),
                    (? nonnull([VV]))}] | (? nonnull([VV])),
                                          (~ ((? nonnull([VV])))),
                                          (len([VV]) = 0),
                                          (len([VV]) >= 0),
                                          (len([VV]) > 0)}
-> X1:{VV:({VV:b | (len([VV]) = len([m])),
                   (len([VV]) > 0),
                   (len([VV]) >= 0),
                   (len([VV]) = 0),
                   (~ ((? nonnull([VV])))),
                   (? nonnull([VV]))},
           {VV:a | (len([VV]) = len([m])),
                   (len([VV]) > 0),
                   (len([VV]) >= 0),
                   (len([VV]) = 0),
                   (~ ((? nonnull([VV])))),
                   (? nonnull([VV]))}) | (len([VV]) = len([m])),
                                         (len([VV]) > 0),
                                         (len([VV]) >= 0),
                                         (len([VV]) = 0),
                                         (~ ((? nonnull([VV])))),
                                         (? nonnull([VV]))}
-> Map
     {VV:b | (len([VV]) = len([X1])),
             (len([VV]) = len([m])),
             (len([VV]) > 0),
             (len([VV]) >= 0),
             (len([VV]) = 0),
             (~ ((? nonnull([VV])))),
             (? nonnull([VV]))}
     {VV:[{VV:a | (len([VV]) = len([X1])),
                  (len([VV]) = len([m])),
                  (len([VV]) > 0),
                  (len([VV]) >= 0),
                  (len([VV]) = 0),
                  (~ ((? nonnull([VV])))),
                  (? nonnull([VV]))}] | (len([VV]) = len([X1])),
                                        (len([VV]) = len([m])),
                                        (len([VV]) > 0),
                                        (len([VV]) >= 0),
                                        (len([VV]) = 0),
                                        (~ ((? nonnull([VV])))),
                                        (? nonnull([VV]))}addKV Map
  {VV:c | (len([VV]) > 0),
          (len([VV]) >= 0),
          (len([VV]) = 0),
          (~ ((? nonnull([VV])))),
          (? nonnull([VV]))}
  {VV:[{VV:e | (len([VV]) > 0),
               (len([VV]) >= 0),
               (len([VV]) = 0),
               (~ ((? nonnull([VV])))),
               (? nonnull([VV]))}] | (? nonnull([VV])),
                                     (~ ((? nonnull([VV])))),
                                     (len([VV]) = 0),
                                     (len([VV]) >= 0),
                                     (len([VV]) > 0)}m (k, v) = forall a b. (Ord a) -> a -> b -> Map a b -> Map a bM.insert {VV:a | (len([VV]) = len([m])),
        (len([VV]) > 0),
        (len([VV]) >= 0),
        (len([VV]) = 0),
        (~ ((? nonnull([VV])))),
        (? nonnull([VV])),
        (len([VV]) = len([m])),
        (len([VV]) > 0),
        (len([VV]) >= 0),
        (len([VV]) = 0),
        (~ ((? nonnull([VV])))),
        (? nonnull([VV])),
        (VV = k)}k vs' {VV:Map
      {VV:c | (len([VV]) > 0),
              (len([VV]) >= 0),
              (len([VV]) = 0),
              (~ ((? nonnull([VV])))),
              (? nonnull([VV]))}
      {VV:[{VV:e | (len([VV]) > 0),
                   (len([VV]) >= 0),
                   (len([VV]) = 0),
                   (~ ((? nonnull([VV])))),
                   (? nonnull([VV]))}] | (? nonnull([VV])),
                                         (~ ((? nonnull([VV])))),
                                         (len([VV]) = 0),
                                         (len([VV]) >= 0),
                                         (len([VV]) > 0)} | true,(VV = m)}m
  where vs' = {VV:a | (len([VV]) = len([m])),
        (len([VV]) > 0),
        (len([VV]) >= 0),
        (len([VV]) = 0),
        (~ ((? nonnull([VV])))),
        (? nonnull([VV])),
        (len([VV]) = len([m])),
        (len([VV]) = len([k])),
        (len([VV]) > 0),
        (len([VV]) >= 0),
        (len([VV]) = 0),
        (~ ((? nonnull([VV])))),
        (? nonnull([VV])),
        (VV = v)}v forall a.
a
-> ys:[a]
-> {VV:[a] | ((? nonnull([VV])) <=> true),
             (nully([VV]) = 1),
             (len([VV]) = (1 + len([ys])))}: (forall a b. (Ord a) -> b -> a -> Map a b -> bM.findWithDefault forall a.
{VV:[a] | ((? nonnull([VV])) <=> false),
          (nully([VV]) = 0),
          (len([VV]) = 0)}[] {VV:a | (len([VV]) = len([m])),
        (len([VV]) > 0),
        (len([VV]) >= 0),
        (len([VV]) = 0),
        (~ ((? nonnull([VV])))),
        (? nonnull([VV])),
        (len([VV]) = len([m])),
        (len([VV]) > 0),
        (len([VV]) >= 0),
        (len([VV]) = 0),
        (~ ((? nonnull([VV])))),
        (? nonnull([VV])),
        (VV = k)}k {VV:Map
      {VV:c | (len([VV]) > 0),
              (len([VV]) >= 0),
              (len([VV]) = 0),
              (~ ((? nonnull([VV])))),
              (? nonnull([VV]))}
      {VV:[{VV:e | (len([VV]) > 0),
                   (len([VV]) >= 0),
                   (len([VV]) = 0),
                   (~ ((? nonnull([VV])))),
                   (? nonnull([VV]))}] | (? nonnull([VV])),
                                         (~ ((? nonnull([VV])))),
                                         (len([VV]) = 0),
                                         (len([VV]) >= 0),
                                         (len([VV]) > 0)} | true,(VV = m)}m)

----------------------------------------------------------------
--- Step 3: Group By Key ---------------------------------------
----------------------------------------------------------------

forall a b.
({VV:a | (? nonnull([VV])),
         (~ ((? nonnull([VV])))),
         (len([VV]) = 0),
         (len([VV]) >= 0),
         (len([VV]) > 0)}
 -> {VV:a | (? nonnull([VV])),
            (~ ((? nonnull([VV])))),
            (len([VV]) = 0),
            (len([VV]) >= 0),
            (len([VV]) > 0)}
 -> {VV:a | (? nonnull([VV])),
            (~ ((? nonnull([VV])))),
            (len([VV]) = 0),
            (len([VV]) >= 0),
            (len([VV]) > 0)})
-> {VV:Map
         {VV:b | (len([VV]) > 0),
                 (len([VV]) >= 0),
                 (len([VV]) = 0),
                 (~ ((? nonnull([VV])))),
                 (? nonnull([VV]))}
         {VV:[{VV:a | (len([VV]) > 0),
                      (len([VV]) >= 0),
                      (len([VV]) = 0),
                      (~ ((? nonnull([VV])))),
                      (? nonnull([VV]))}] | (len([VV]) > 0),
                                            (len([VV]) >= 0),
                                            (len([VV]) = 0),
                                            (~ ((? nonnull([VV])))),
                                            (? nonnull([VV]))} | (? nonnull([VV])),
                                                                 (~ ((? nonnull([VV])))),
                                                                 (len([VV]) = 0),
                                                                 (len([VV]) >= 0),
                                                                 (len([VV]) > 0)}
-> {VV:[{VV:({VV:b | (? nonnull([VV])),
                     (~ ((? nonnull([VV])))),
                     (len([VV]) = 0),
                     (len([VV]) >= 0),
                     (len([VV]) > 0)},
             {VV:a | (? nonnull([VV])),
                     (~ ((? nonnull([VV])))),
                     (len([VV]) = 0),
                     (len([VV]) >= 0),
                     (len([VV]) > 0)}) | (? nonnull([VV])),
                                         (~ ((? nonnull([VV])))),
                                         (len([VV]) = 0),
                                         (len([VV]) >= 0),
                                         (len([VV]) > 0)}] | (? nonnull([VV])),
                                                             (~ ((? nonnull([VV])))),
                                                             (len([VV]) = 0),
                                                             (len([VV]) >= 0),
                                                             (len([VV]) > 0)}collapse {VV:a | (? nonnull([VV])),
        (~ ((? nonnull([VV])))),
        (len([VV]) = 0),
        (len([VV]) >= 0),
        (len([VV]) > 0)}
-> {VV:a | (? nonnull([VV])),
           (~ ((? nonnull([VV])))),
           (len([VV]) = 0),
           (len([VV]) >= 0),
           (len([VV]) > 0)}
-> {VV:a | (? nonnull([VV])),
           (~ ((? nonnull([VV])))),
           (len([VV]) = 0),
           (len([VV]) >= 0),
           (len([VV]) > 0)}f = forall a b c. (a -> b -> c -> c) -> c -> Map a b -> cM.foldrWithKey {VV:[{VV:b | (len([VV]) = len([k])),
             (len([VV]) > 0),
             (len([VV]) >= 0),
             (len([VV]) = 0),
             (~ ((? nonnull([VV])))),
             (? nonnull([VV]))}] | (len([VV]) = len([k])),
                                   (len([VV]) > 0),
                                   (len([VV]) >= 0),
                                   (len([VV]) = 0),
                                   (~ ((? nonnull([VV])))),
                                   (? nonnull([VV])),
                                   (VV = X1)}reduceKV forall a.
{VV:[a] | ((? nonnull([VV])) <=> false),
          (nully([VV]) = 0),
          (len([VV]) = 0)}[]
  where reduceKV {VV:a | (? nonnull([VV])),
        (~ ((? nonnull([VV])))),
        (len([VV]) = 0),
        (len([VV]) >= 0),
        (len([VV]) > 0)}k (v:vs) {VV:[{VV:({VV:c | (? nonnull([VV])),
                  (~ ((? nonnull([VV])))),
                  (len([VV]) = 0),
                  (len([VV]) >= 0),
                  (len([VV]) > 0),
                  (len([VV]) = len([k])),
                  (len([VV]) = len([X1])),
                  (VV < k),
                  (VV <= k),
                  (k < VV),
                  (k <= VV)},
          {VV:d | (? nonnull([VV])),
                  (~ ((? nonnull([VV])))),
                  (len([VV]) = 0),
                  (len([VV]) >= 0),
                  (len([VV]) > 0),
                  (len([VV]) = len([k])),
                  (len([VV]) = len([X1]))}) | (? nonnull([VV])),
                                              (~ ((? nonnull([VV])))),
                                              (len([VV]) = 0),
                                              (len([VV]) >= 0),
                                              (len([VV]) > 0),
                                              (len([VV]) = len([k])),
                                              (len([VV]) = len([X1]))}] | (? nonnull([VV])),
                                                                          (len([VV]) > 0),
                                                                          (len([VV]) = len([k])),
                                                                          (len([VV]) = len([X1])),
                                                                          (len([VV]) >= 0),
                                                                          (len([VV]) = 0),
                                                                          (~ ((? nonnull([VV]))))}acc = forall a b. a -> b -> (a, b)({VV:a | (? nonnull([VV])),
        (~ ((? nonnull([VV])))),
        (len([VV]) = 0),
        (len([VV]) >= 0),
        (len([VV]) > 0),
        (VV = k)}k, forall a b. (a -> b -> a) -> a -> [b] -> afoldl' {VV:a | (? nonnull([VV])),
        (~ ((? nonnull([VV])))),
        (len([VV]) = 0),
        (len([VV]) >= 0),
        (len([VV]) > 0)}
-> {VV:a | (? nonnull([VV])),
           (~ ((? nonnull([VV])))),
           (len([VV]) = 0),
           (len([VV]) >= 0),
           (len([VV]) > 0)}
-> {VV:a | (? nonnull([VV])),
           (~ ((? nonnull([VV])))),
           (len([VV]) = 0),
           (len([VV]) >= 0),
           (len([VV]) > 0)}f {VV:a | (len([VV]) = len([k])),
        (len([VV]) > 0),
        (len([VV]) >= 0),
        (len([VV]) = 0),
        (~ ((? nonnull([VV])))),
        (? nonnull([VV])),
        (len([VV]) = len([k])),
        (len([VV]) > 0),
        (len([VV]) >= 0),
        (len([VV]) = 0),
        (~ ((? nonnull([VV])))),
        (? nonnull([VV])),
        (VV = v)}v {VV:[{VV:b | (len([VV]) = len([k])),
             (len([VV]) > 0),
             (len([VV]) >= 0),
             (len([VV]) = 0),
             (~ ((? nonnull([VV])))),
             (? nonnull([VV]))}] | (VV = vs)}vs) forall a.
a
-> ys:[a]
-> {VV:[a] | ((? nonnull([VV])) <=> true),
             (nully([VV]) = 1),
             (len([VV]) = (1 + len([ys])))}: {VV:[{VV:({VV:c | (? nonnull([VV])),
                  (~ ((? nonnull([VV])))),
                  (len([VV]) = 0),
                  (len([VV]) >= 0),
                  (len([VV]) > 0),
                  (len([VV]) = len([k])),
                  (len([VV]) = len([X1])),
                  (VV < k),
                  (VV <= k),
                  (k < VV),
                  (k <= VV)},
          {VV:d | (? nonnull([VV])),
                  (~ ((? nonnull([VV])))),
                  (len([VV]) = 0),
                  (len([VV]) >= 0),
                  (len([VV]) > 0),
                  (len([VV]) = len([k])),
                  (len([VV]) = len([X1]))}) | (? nonnull([VV])),
                                              (~ ((? nonnull([VV])))),
                                              (len([VV]) = 0),
                                              (len([VV]) >= 0),
                                              (len([VV]) > 0),
                                              (len([VV]) = len([k])),
                                              (len([VV]) = len([X1]))}] | (? nonnull([VV])),
                                                                          (len([VV]) > 0),
                                                                          (len([VV]) = len([k])),
                                                                          (len([VV]) = len([X1])),
                                                                          (len([VV]) >= 0),
                                                                          (len([VV]) = 0),
                                                                          (~ ((? nonnull([VV])))),
                                                                          (VV = acc)}acc
        reduceKV k []     _   = forall a. {VV:Bool | (? VV)} -> acrash {VV:Bool | (~ ((? VV))),(VV = False)}False --error $ show (assert False)

----------------------------------------------------------------
--- Putting it All Together ------------------------------------
----------------------------------------------------------------

forall a b c.
(Ord b)
-> ({VV:c | (? nonnull([VV])),
            (~ ((? nonnull([VV])))),
            (len([VV]) = 0),
            (len([VV]) >= 0),
            (len([VV]) > 0)}
    -> {VV:[{VV:({VV:b | (len([VV]) > 0),
                         (len([VV]) >= 0),
                         (len([VV]) = 0),
                         (~ ((? nonnull([VV])))),
                         (? nonnull([VV]))},
                 a) | (len([VV]) > 0),
                      (len([VV]) >= 0),
                      (len([VV]) = 0),
                      (~ ((? nonnull([VV])))),
                      (? nonnull([VV]))}] | (len([VV]) > 0),
                                            (len([VV]) >= 0),
                                            (len([VV]) = 0),
                                            (~ ((? nonnull([VV])))),
                                            (? nonnull([VV]))})
-> (a -> a -> a)
-> {VV:[c] | (? nonnull([VV])),(len([VV]) >= 0),(len([VV]) > 0)}
-> {VV:[{VV:({VV:b | (? nonnull([VV])),
                     (~ ((? nonnull([VV])))),
                     (len([VV]) = 0),
                     (len([VV]) >= 0),
                     (len([VV]) > 0)},
             a) | (? nonnull([VV])),
                  (~ ((? nonnull([VV])))),
                  (len([VV]) = 0),
                  (len([VV]) >= 0),
                  (len([VV]) > 0)}] | (? nonnull([VV])),
                                      (~ ((? nonnull([VV])))),
                                      (len([VV]) = 0),
                                      (len([VV]) >= 0),
                                      (len([VV]) > 0)}mapReduce {VV:a | (? nonnull([VV])),
        (~ ((? nonnull([VV])))),
        (len([VV]) = 0),
        (len([VV]) >= 0),
        (len([VV]) > 0)}
-> {VV:[{VV:({VV:d | (len([VV]) > 0),
                     (len([VV]) >= 0),
                     (len([VV]) = 0),
                     (~ ((? nonnull([VV])))),
                     (? nonnull([VV]))},
             e) | (len([VV]) > 0),
                  (len([VV]) >= 0),
                  (len([VV]) = 0),
                  (~ ((? nonnull([VV])))),
                  (? nonnull([VV]))}] | (len([VV]) > 0),
                                        (len([VV]) >= 0),
                                        (len([VV]) = 0),
                                        (~ ((? nonnull([VV])))),
                                        (? nonnull([VV]))}fmap a -> a -> afred = forall a b.
({VV:a | (? nonnull([VV])),
         (~ ((? nonnull([VV])))),
         (len([VV]) = 0),
         (len([VV]) >= 0),
         (len([VV]) > 0)}
 -> {VV:a | (? nonnull([VV])),
            (~ ((? nonnull([VV])))),
            (len([VV]) = 0),
            (len([VV]) >= 0),
            (len([VV]) > 0)}
 -> {VV:a | (? nonnull([VV])),
            (~ ((? nonnull([VV])))),
            (len([VV]) = 0),
            (len([VV]) >= 0),
            (len([VV]) > 0)})
-> {VV:Map
         {VV:b | (len([VV]) > 0),
                 (len([VV]) >= 0),
                 (len([VV]) = 0),
                 (~ ((? nonnull([VV])))),
                 (? nonnull([VV]))}
         {VV:[{VV:a | (len([VV]) > 0),
                      (len([VV]) >= 0),
                      (len([VV]) = 0),
                      (~ ((? nonnull([VV])))),
                      (? nonnull([VV]))}] | (len([VV]) > 0),
                                            (len([VV]) >= 0),
                                            (len([VV]) = 0),
                                            (~ ((? nonnull([VV])))),
                                            (? nonnull([VV]))} | (? nonnull([VV])),
                                                                 (~ ((? nonnull([VV])))),
                                                                 (len([VV]) = 0),
                                                                 (len([VV]) >= 0),
                                                                 (len([VV]) > 0)}
-> {VV:[{VV:({VV:b | (? nonnull([VV])),
                     (~ ((? nonnull([VV])))),
                     (len([VV]) = 0),
                     (len([VV]) >= 0),
                     (len([VV]) > 0)},
             {VV:a | (? nonnull([VV])),
                     (~ ((? nonnull([VV])))),
                     (len([VV]) = 0),
                     (len([VV]) >= 0),
                     (len([VV]) > 0)}) | (? nonnull([VV])),
                                         (~ ((? nonnull([VV])))),
                                         (len([VV]) = 0),
                                         (len([VV]) >= 0),
                                         (len([VV]) > 0)}] | (? nonnull([VV])),
                                                             (~ ((? nonnull([VV])))),
                                                             (len([VV]) = 0),
                                                             (len([VV]) >= 0),
                                                             (len([VV]) > 0)}collapse a -> a -> afred forall a b c. (a -> b) -> (c -> a) -> c -> b. forall a b.
(Ord a)
-> [{VV:({VV:a | (len([VV]) > 0),
                 (len([VV]) >= 0),
                 (len([VV]) = 0),
                 (~ ((? nonnull([VV])))),
                 (? nonnull([VV]))},
         {VV:b | (len([VV]) > 0),
                 (len([VV]) >= 0),
                 (len([VV]) = 0),
                 (~ ((? nonnull([VV])))),
                 (? nonnull([VV]))}) | (len([VV]) > 0),
                                       (len([VV]) >= 0),
                                       (len([VV]) = 0),
                                       (~ ((? nonnull([VV])))),
                                       (? nonnull([VV]))}]
-> {VV:Map
         {VV:a | (len([VV]) > 0),
                 (len([VV]) >= 0),
                 (len([VV]) = 0),
                 (~ ((? nonnull([VV])))),
                 (? nonnull([VV]))}
         {VV:[{VV:b | (len([VV]) > 0),
                      (len([VV]) >= 0),
                      (len([VV]) = 0),
                      (~ ((? nonnull([VV])))),
                      (? nonnull([VV]))}] | (len([VV]) > 0),
                                            (len([VV]) >= 0),
                                            (len([VV]) = 0),
                                            (~ ((? nonnull([VV])))),
                                            (? nonnull([VV]))} | (? nonnull([VV])),
                                                                 (~ ((? nonnull([VV])))),
                                                                 (len([VV]) = 0),
                                                                 (len([VV]) >= 0),
                                                                 (len([VV]) > 0)}group forall a b c. (a -> b) -> (c -> a) -> c -> b. forall a b c.
({VV:a | (len([VV]) > 0),
         (len([VV]) >= 0),
         (len([VV]) = 0),
         (~ ((? nonnull([VV])))),
         (? nonnull([VV]))}
 -> {VV:[{VV:({VV:b | (len([VV]) > 0),
                      (len([VV]) >= 0),
                      (len([VV]) = 0),
                      (~ ((? nonnull([VV])))),
                      (? nonnull([VV]))},
              {VV:c | (? nonnull([VV])),
                      (~ ((? nonnull([VV])))),
                      (len([VV]) = 0),
                      (len([VV]) >= 0),
                      (len([VV]) > 0)}) | (len([VV]) > 0),
                                          (len([VV]) >= 0),
                                          (len([VV]) = 0),
                                          (~ ((? nonnull([VV])))),
                                          (? nonnull([VV]))}] | (len([VV]) > 0),
                                                                (len([VV]) >= 0),
                                                                (len([VV]) = 0),
                                                                (~ ((? nonnull([VV])))),
                                                                (? nonnull([VV]))})
-> X1:{VV:[a] | (len([VV]) > 0),(len([VV]) >= 0),(? nonnull([VV]))}
-> [{VV:({VV:b | (len([VV]) = len([X1])),
                 (len([VV]) > 0),
                 (len([VV]) >= 0),
                 (len([VV]) = 0),
                 (~ ((? nonnull([VV])))),
                 (? nonnull([VV]))},
         {VV:c | (len([VV]) = len([X1])),
                 (len([VV]) > 0),
                 (len([VV]) >= 0),
                 (len([VV]) = 0),
                 (~ ((? nonnull([VV])))),
                 (? nonnull([VV]))}) | (len([VV]) = len([X1])),
                                       (len([VV]) > 0),
                                       (len([VV]) >= 0),
                                       (len([VV]) = 0),
                                       (~ ((? nonnull([VV])))),
                                       (? nonnull([VV]))}]expand {VV:a | (? nonnull([VV])),
        (~ ((? nonnull([VV])))),
        (len([VV]) = 0),
        (len([VV]) >= 0),
        (len([VV]) > 0)}
-> {VV:[{VV:({VV:d | (len([VV]) > 0),
                     (len([VV]) >= 0),
                     (len([VV]) = 0),
                     (~ ((? nonnull([VV])))),
                     (? nonnull([VV]))},
             e) | (len([VV]) > 0),
                  (len([VV]) >= 0),
                  (len([VV]) = 0),
                  (~ ((? nonnull([VV])))),
                  (? nonnull([VV]))}] | (len([VV]) > 0),
                                        (len([VV]) >= 0),
                                        (len([VV]) = 0),
                                        (~ ((? nonnull([VV])))),
                                        (? nonnull([VV]))}fmap 

----------------------------------------------------------------
--- "Word Count" -----------------------------------------------
----------------------------------------------------------------

{VV:[[{VV:Char | (? nonnull([VV])),
                 (~ ((? nonnull([VV])))),
                 (len([VV]) = 0),
                 (len([VV]) >= 0),
                 (len([VV]) > 0)}]] | (? nonnull([VV])),
                                      (len([VV]) >= 0),
                                      (len([VV]) > 0)}
-> {VV:[{VV:({VV:[{VV:Char | (? nonnull([VV])),
                             (~ ((? nonnull([VV])))),
                             (len([VV]) = 0),
                             (len([VV]) >= 0),
                             (len([VV]) > 0)}] | (len([VV]) > 0),
                                                 (len([VV]) >= 0),
                                                 (len([VV]) = 0),
                                                 (~ ((? nonnull([VV])))),
                                                 (? nonnull([VV])),
                                                 (? nonnull([VV])),
                                                 (~ ((? nonnull([VV])))),
                                                 (len([VV]) = 0),
                                                 (len([VV]) >= 0),
                                                 (len([VV]) > 0)},
             {VV:Int | (0 = VV),(0 <= VV),true}) | (? nonnull([VV])),
                                                   (~ ((? nonnull([VV])))),
                                                   (len([VV]) = 0),
                                                   (len([VV]) >= 0),
                                                   (len([VV]) > 0)}] | (? nonnull([VV])),
                                                                       (~ ((? nonnull([VV])))),
                                                                       (len([VV]) = 0),
                                                                       (len([VV]) >= 0),
                                                                       (len([VV]) > 0)}wordCount  = (Ord [Char])mapReduce fm x:Int -> y:Int -> {VV:Int | (VV = (x + y))}plus 
  where fm = {VV:[{VV:[{VV:Char | (? nonnull([VV])),
                     (~ ((? nonnull([VV])))),
                     (len([VV]) = 0),
                     (len([VV]) >= 0),
                     (len([VV]) > 0),
                     (len([VV]) = len([doc]))}] | (? nonnull([VV])),
                                                  (~ ((? nonnull([VV])))),
                                                  (len([VV]) = 0),
                                                  (len([VV]) >= 0),
                                                  (len([VV]) > 0),
                                                  (len([VV]) = len([doc])),
                                                  (VV < doc),
                                                  (VV <= doc),
                                                  (doc < VV),
                                                  (doc <= VV)}] | (? nonnull([VV])),
                                                                  (~ ((? nonnull([VV])))),
                                                                  (len([VV]) = 0),
                                                                  (len([VV]) >= 0),
                                                                  (len([VV]) > 0),
                                                                  (len([VV]) = len([doc])),
                                                                  (VV = X1)}\{VV:[{VV:Char | (? nonnull([VV])),
                (~ ((? nonnull([VV])))),
                (len([VV]) = 0),
                (len([VV]) >= 0),
                (len([VV]) > 0)}] | (len([VV]) > 0),
                                    (len([VV]) >= 0),
                                    (len([VV]) = 0),
                                    (~ ((? nonnull([VV])))),
                                    (? nonnull([VV]))}doc -> [ forall a b. a -> b -> (a, b)({VV:[{VV:Char | (? nonnull([VV])),
                (~ ((? nonnull([VV])))),
                (len([VV]) = 0),
                (len([VV]) >= 0),
                (len([VV]) > 0),
                (len([VV]) = len([doc]))}] | (? nonnull([VV])),
                                             (~ ((? nonnull([VV])))),
                                             (len([VV]) = 0),
                                             (len([VV]) >= 0),
                                             (len([VV]) > 0),
                                             (len([VV]) = len([doc])),
                                             (VV < doc),
                                             (VV <= doc),
                                             (doc < VV),
                                             (doc <= VV),
                                             (? nonnull([VV])),
                                             (~ ((? nonnull([VV])))),
                                             (len([VV]) = 0),
                                             (len([VV]) >= 0),
                                             (len([VV]) > 0),
                                             (len([VV]) = len([doc])),
                                             (VV = X1)}w,x:Int# -> {VV:Int | (VV = (x  :  int))}1) | w <- [Char] -> [[Char]]words {VV:[{VV:Char | (? nonnull([VV])),
                (~ ((? nonnull([VV])))),
                (len([VV]) = 0),
                (len([VV]) >= 0),
                (len([VV]) > 0)}] | (len([VV]) > 0),
                                    (len([VV]) >= 0),
                                    (len([VV]) = 0),
                                    (~ ((? nonnull([VV])))),
                                    (? nonnull([VV])),
                                    (VV = doc)}doc]

{VV:IO
      {VV:() | (? nonnull([VV])),
               (~ ((? nonnull([VV])))),
               (len([VV]) = 0),
               (len([VV]) >= 0),
               (len([VV]) > 0)} | (? nonnull([VV])),
                                  (~ ((? nonnull([VV])))),
                                  (len([VV]) = 0),
                                  (len([VV]) >= 0),
                                  (len([VV]) > 0)}main = [Char] -> IO ()putStrLn forall a b. (a -> b) -> a -> b$ forall a. (Show a) -> a -> [Char]show forall a b. (a -> b) -> a -> b$ {VV:[[{VV:Char | (? nonnull([VV])),
                 (~ ((? nonnull([VV])))),
                 (len([VV]) = 0),
                 (len([VV]) >= 0),
                 (len([VV]) > 0)}]] | (? nonnull([VV])),
                                      (len([VV]) >= 0),
                                      (len([VV]) > 0)}
-> {VV:[{VV:({VV:[{VV:Char | (? nonnull([VV])),
                             (~ ((? nonnull([VV])))),
                             (len([VV]) = 0),
                             (len([VV]) >= 0),
                             (len([VV]) > 0)}] | (len([VV]) > 0),
                                                 (len([VV]) >= 0),
                                                 (len([VV]) = 0),
                                                 (~ ((? nonnull([VV])))),
                                                 (? nonnull([VV])),
                                                 (? nonnull([VV])),
                                                 (~ ((? nonnull([VV])))),
                                                 (len([VV]) = 0),
                                                 (len([VV]) >= 0),
                                                 (len([VV]) > 0)},
             {VV:Int | (0 = VV),(0 <= VV),true}) | (? nonnull([VV])),
                                                   (~ ((? nonnull([VV])))),
                                                   (len([VV]) = 0),
                                                   (len([VV]) >= 0),
                                                   (len([VV]) > 0)}] | (? nonnull([VV])),
                                                                       (~ ((? nonnull([VV])))),
                                                                       (len([VV]) = 0),
                                                                       (len([VV]) >= 0),
                                                                       (len([VV]) > 0)}wordCount docs
  where docs = [ Addr# -> [Char]"this is the end"
               , Addr# -> [Char]"go to the end"
               , Addr# -> [Char]"the end is the beginning"]