content: {-
  NV TODO 
  1. refine data type
  2. connect it with Steps 1 & 2
  3. connect it with dyn programming 
  -}
  
  
  
  {-# LANGUAGE KindSignatures      #-}
  {-# LANGUAGE DataKinds           #-}
  {-# LANGUAGE OverloadedStrings   #-}
  {-# LANGUAGE RankNTypes          #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE GADTs               #-}
  
  
  {-@ LIQUID "--higherorder"         @-}
  {-@ LIQUID "--totality"            @-}
  {-@ LIQUID "--exactdc"             @-}
  
  module Main where
  
  import Language.Haskell.Liquid.String
  import GHC.TypeLits
  import Data.String hiding (fromString)
  import Data.Proxy 
  import Prelude hiding (mempty, mappend, id, mconcat, map)
  import Language.Haskell.Liquid.ProofCombinators 
  
  import Data.Maybe 
  
  -- | Interface 
  
  main :: IO ()
  main = 
     do input     <- fromString <$> readFile "input.txt"
        let mi1    = toMI input :: MI "abcab" SMTString
        let is1    = getIndex mi1 
        putStrLn ("Serial   Indices: " ++ show is1)
        let mi2    = toMIPar input :: MI "abcab" SMTString
        let is2    = getIndex mi2 
        putStrLn ("Parallel Indices: " ++ show is2)
        putStrLn ("Are equal? " ++ show (is1 == is2))
  
  {-
  main :: IO ()
  main = 
    do input     <- fromString <$> readFile "input.txt"
       case someSymbolVal "x" of 
              SomeSymbol (_ :: Proxy y) ->            
        let mi1    = toMI input :: MI y SMTString
        let is1    = getIndex mi1 
        putStrLn ("Serial   Indices: " ++ show is1)
        let mi2    = toMIPar input :: MI "abcab" SMTString
        let is2    = getIndex mi2 
        putStrLn ("Parallel Indices: " ++ show is2)
        putStrLn ("Are equal? " ++ show (is1 == is2))
  
  
  -}
  
  test1   = indices input1 
  input1  = fromString $ clone 100 "ababcabcab"
  
  
  indices :: SMTString -> List Int 
  indices input 
    = case toMI input :: MI "abcab" SMTString  of 
        MI _ i -> i 
  
  
  {-
  
  
  
    |
  -}
  
  mconcatPar :: forall (target :: Symbol). (KnownSymbol target) =>  Int -> [MI target SMTString] -> MI target SMTString
  mconcatPar n xs = mconcat (mconcatPar' n xs)
  
  {-@ Lazy mconcatPar' @-}
  -- Termination proof is terribly slow and will change... 
  {-@ mconcatPar' :: forall (target :: Symbol). (KnownSymbol target) =>  Int -> xs:[MI target SMTString] -> [MI target SMTString] @-}
  mconcatPar' :: forall (target :: Symbol). (KnownSymbol target) =>  Int -> [MI target SMTString] -> [MI target SMTString]
  mconcatPar' n xs | length xs <= n = [mconcat xs]  
  mconcatPar' n xs = let (x, r) = splitAt n xs 
                     in mconcatPar' n (mconcat x:mconcatPar' n r)
  
  toMIPar :: forall (target :: Symbol). (KnownSymbol target) => SMTString -> MI target SMTString 
  toMIPar input = undefined 
  
  toMI :: forall (target :: Symbol). (KnownSymbol target) => SMTString -> MI target SMTString 
  toMI input = if isNullString input then mempty else  MI input (makeIndices input (fromString (symbolVal (Proxy :: Proxy target))) 0 (stringLen input - 1))
  
  getIndex :: forall (target :: Symbol).  MI target SMTString -> List Int 
  getIndex (MI _ i) = i 
  
  clone :: Int -> [a] -> [a]
  clone i xs | i <= 0 = [] 
  clone 1 xs = xs 
  clone n xs = xs ++ clone (n-1) xs
  
  mconcat :: forall (target :: Symbol). (KnownSymbol target) => [MI target SMTString] -> MI target SMTString
  mconcat []       = mempty 
  mconcat [x]      = x 
  mconcat [x1, x2] = mappend x1 x2 
  mconcat (x:xs)   = mappend x (mconcat xs)
  
  
  -- | Indexing Structure Definition 
  
  -- Structure that defines valid indeces of a type level target 
  -- symbol in a value level string
  
  data MI (target :: Symbol) s where 
    MI :: SMTString        -- input string
       -> (List Int)      -- valid indeces of target in input
       -> MI target s
    deriving (Show)
  
  {-@ data MI target s 
    = MI { input :: SMTString
         , idxes   :: List Int 
         } @-}
  
  
  {- data MI target s 
    = MI { input :: SMTString
         , List :: List (GoodIndex input target)
         } @-}
  
  
  {-@ measure indixesMI @-}
  indixesMI (MI _ is) = is 
  {-@ measure inputMI @-}
  inputMI (MI i _) = i 
  
  
  
  {-@ type GoodIndex Input Target 
    = {i:Int |  IsGoodIndex Input Target i}
    @-}
  
  {-@ type GoodIndexTwo Input Input2 Target 
    = {i:Int |  IsGoodIndex Input Target i && IsGoodIndex (concatString Input Input2) Target i }
    @-}
  
  {-@ predicate IsGoodIndex Input Target I
    =  (subString Input I (stringLen Target)  == Target)
    && (I + stringLen Target <= stringLen Input)
    && (0 <= I)
    @-}
  
  
  -- | Monoid methods 
  
  {-@ reflect mempty @-}
  mempty :: forall (target :: Symbol). MI target SMTString
  mempty = MI stringEmp N
  
  {-@ reflect mappend @-}
  mappend :: forall (target :: Symbol).  (KnownSymbol target) => MI target SMTString -> MI target SMTString -> MI target SMTString
  mappend (MI i1 is1) (MI i2 is2)
    = MI (concatString i1 i2) -- (mappendMakeIndixes i1 i2 (fromString (symbolVal (Proxy :: Proxy target))) is1 is2)
      ((is1 
          `append` 
        makeNewIndices i1 i2 (fromString (symbolVal (Proxy :: Proxy target))))
          `append` 
        map (shift (stringLen i1)) is2)            
   
  
  -------------------------------------------------------------------------------
  --------------- PROOFS  -------------------------------------------------------
  -------------------------------------------------------------------------------
  
  mempty_left :: forall (target :: Symbol). (KnownSymbol target) => MI target SMTString -> Proof
  {-@ mempty_left :: xs:MI target SMTString -> {mappend xs mempty == xs } @-}
  mempty_left (MI i1 is1)
    =   mappend (MI i1 is1) (mempty :: MI target SMTString)
    ==. mappend (MI i1 is1) (MI stringEmp N) 
    ==. MI (concatString i1 stringEmp)  
         (is1 `append` map (shift (stringLen i1)) N
              `append` makeNewIndices i1 stringEmp (fromString (symbolVal (Proxy :: Proxy target))))
    ==. MI (concatString i1 stringEmp)  
         ((is1 `append` N)
              `append` makeNewIndices i1 stringEmp (fromString (symbolVal (Proxy :: Proxy target))))
    ==. MI (concatString i1 stringEmp)  
         (is1 `append` makeNewIndices i1 stringEmp (fromString (symbolVal (Proxy :: Proxy target))))
        ? appendEmp is1 
    ==. MI (concatString i1 stringEmp)  
         (is1 `append` N) 
        ? makeNewIndicesNullLeft i1 (fromString (symbolVal (Proxy :: Proxy target)))
    ==. MI (concatString i1 stringEmp) is1 
        ? appendEmp is1 
    ==. MI i1 is1 
        ? concatStringNeutral i1 
    *** QED 
  
  
  
  
  
  mempty_right :: forall (target :: Symbol). (KnownSymbol target) => MI target SMTString -> Proof
  {-@ mempty_right :: xs:MI target SMTString -> {mappend mempty xs == xs } @-}
  mempty_right (MI i is)
    =   mappend (mempty :: MI target SMTString) (MI i is) 
    ==. mappend (MI stringEmp N) (MI i is) 
    ==. MI (concatString stringEmp i)  
         (N `append` makeNewIndices stringEmp i (fromString (symbolVal (Proxy :: Proxy target)))
                 `append` map (shift (stringLen stringEmp)) is)
    ==. MI (concatString stringEmp i)  
         ( makeNewIndices stringEmp i (fromString (symbolVal (Proxy :: Proxy target)))
          `append`
           map (shift (stringLen stringEmp)) is)
    ==. MI (concatString stringEmp i)  
         ( makeNewIndices stringEmp i (fromString (symbolVal (Proxy :: Proxy target)))
           `append` 
           map (shift 0) is)
    ==. MI (concatString stringEmp i)  
         (makeNewIndices stringEmp i (fromString (symbolVal (Proxy :: Proxy target)))
          `append` 
          is)
         ? mapShiftZero is 
    ==. MI (concatString stringEmp i)  
         (N `append` is) 
        ? makeNewIndicesNullRight i (fromString (symbolVal (Proxy :: Proxy target)))
    ==. MI (concatString stringEmp i) is 
    ==. MI i is 
        ? concatStringNeutralRight i
    *** QED 
  
  {-@ mappend_assoc 
    :: x:MI target SMTString -> y:MI target SMTString -> z:MI target SMTString
    -> {v:Proof | mappend x (mappend y z) = mappend (mappend x y) z}
    @-}
  mappend_assoc 
       :: forall (target :: Symbol). (KnownSymbol target) 
       => MI target SMTString ->  MI target SMTString ->  MI target SMTString -> Proof
  mappend_assoc x@(MI xi xis) y@(MI yi yis) z@(MI zi zis)
    | stringLen (fromString (symbolVal (Proxy :: Proxy target))) <= stringLen yi 
    =   mappend x (mappend y z)
    ==. mappend (MI xi xis) (mappend (MI yi yis) (MI zi zis))
    ==. mappend (MI xi xis) 
                (MI (concatString yi zi)  
                    ((yis 
                      `append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
                      `append` map (shift (stringLen yi)) zis))
    ==. MI (concatString xi (concatString yi zi))  
           ((xis `append` 
                 makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
                 `append` 
                    map (shift (stringLen xi)) 
                    ((yis 
                      `append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
                      `append` map (shift (stringLen yi)) zis)
                )
    ==. MI (concatString (concatString xi yi) zi)  
           ((xis `append` 
                 makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
                 `append` 
                    map (shift (stringLen xi)) 
                    ((yis 
                      `append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
                      `append` map (shift (stringLen yi)) zis)
                )
        ? concatStringAssoc xi yi zi 
    ==. MI (concatString (concatString xi yi) zi)  
           ((xis `append` 
                 makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
                 `append` 
                    (
                      (map (shift (stringLen xi)) (yis 
                      `append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target)))))
                      `append` 
                      map (shift (stringLen xi)) (map (shift (stringLen yi)) zis))
                )
        ? map_append (shift (stringLen xi)) 
                     (yis `append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target)))) 
                     (map (shift (stringLen yi)) zis)
    ==. MI (concatString (concatString xi yi) zi)  
           ((xis `append` 
                 makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
                 `append` 
                    (
                      (map (shift (stringLen xi)) yis 
                      `append` (map (shift (stringLen xi)) (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))))
                      `append` 
                      map (shift (stringLen xi)) (map (shift (stringLen yi)) zis))
                )
        ? map_append (shift (stringLen xi)) yis (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
    ==. MI (concatString (concatString xi yi) zi)  
           ((xis `append` 
                 makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
                 `append` 
                    (
                      (map (shift (stringLen xi)) yis 
                      `append` (map (shift (stringLen xi)) (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))))
                      `append` 
                      map (shift (stringLen (concatString xi yi))) zis)
                )
        ? map_len_fusion xi yi zis 
  -- ((x1~x2) ~ ((x3~x4) ~ x5))
  -- == 
  --   ((((x1~x2) ~x3) ~x4) ~x5
    ==. MI (concatString (concatString xi yi) zi)
           (((( xis 
                 `append` 
                makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))                      `append` map (shift (stringLen xi)) yis)
                 `append` 
                map (shift (stringLen xi)) yis)
                 `append`
                map (shift (stringLen (concatString xi yi))) zis)
  
        ? appendReorder xis
                        (makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
                        (map (shift (stringLen xi)) yis)
                        (map (shift (stringLen xi)) (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target)))))
                        (map (shift (stringLen (concatString xi yi))) zis)
  -- ((((x1 ~ x2) ~ x3) ~ x4) ~ x5)
  -- 
  -- ((((x1 ~ x2) ~ x3) ~ x4) ~ x5)
  
    ==. MI (concatString (concatString xi yi) zi)
           (((( xis 
                 `append` 
                makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
                 `append` 
                map (shift (stringLen xi)) yis)
                 `append`
                makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target))))
                 `append` 
                map (shift (stringLen (concatString xi yi))) zis 
            )
        ? shiftIndexes xi yi zi (fromString (symbolVal (Proxy :: Proxy target)))
    ==. mappend (MI (concatString xi yi)  
                    ( (xis `append` makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
                         `append` map (shift (stringLen xi)) yis
                    )
                ) (MI zi zis)
    ==. mappend (mappend (MI xi xis) (MI yi yis)) (MI zi zis)
    *** QED 
  
  
  
  mappend_assoc x@(MI xi xis) y@(MI yi yis) z@(MI zi zis)
    | stringLen yi < stringLen (fromString (symbolVal (Proxy :: Proxy target))) 
    =   mappend x (mappend y z)
    ==. mappend (MI xi xis) (mappend (MI yi yis) (MI zi zis))
    ==. mappend (MI xi xis) 
                (MI (concatString yi zi)  
                    ((yis 
                      `append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
                      `append` map (shift (stringLen yi)) zis))
    ==. MI (concatString xi (concatString yi zi))  
           ((xis `append` 
                 makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
                 `append` 
                    map (shift (stringLen xi)) 
                    ((yis 
                      `append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
                      `append` map (shift (stringLen yi)) zis)
                )
    ==. MI (concatString (concatString xi yi) zi)  
           ((xis `append` 
                 makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
                 `append` 
                    map (shift (stringLen xi)) 
                    ((yis 
                      `append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
                      `append` map (shift (stringLen yi)) zis)
                )
        ? concatStringAssoc xi yi zi 
    ==. MI (concatString (concatString xi yi) zi)  
           ((xis `append` 
                 makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
                 `append` 
                    map (shift (stringLen xi)) 
                    ((N 
                      `append` makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
                      `append` map (shift (stringLen yi)) zis)
                )
          ? emptyIndexes y (assumeGoodIndex yi (fromString (symbolVal (Proxy :: Proxy target))) yis)
    ==. MI (concatString (concatString xi yi) zi)  
           ((xis `append` 
                 makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
                 `append` 
                    map (shift (stringLen xi)) 
                    (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target)))
                      `append` map (shift (stringLen yi)) zis)
                )
    ==. MI (concatString (concatString xi yi) zi)  
           ((xis `append` 
                 makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
                 `append` 
                    (map (shift (stringLen xi)) (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
                    `append` map (shift (stringLen xi)) (map (shift (stringLen yi)) zis))
                )
        ? map_append (shift (stringLen xi)) 
                     (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target)))) 
                     (map (shift (stringLen yi)) zis)
  
    ==. MI (concatString (concatString xi yi) zi)  
           ((xis `append` 
                 makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
                 `append` 
                    (map (shift (stringLen xi)) (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target))))
                    `append` map (shift (stringLen xi)) (map (shift (stringLen yi)) zis))
                )
        ? map_len_fusion xi yi zis 
  -- ((x1~x2) ~ (x3~x4))
  -- == 
  -- (x1 ~ (x2~x3)) ~ x4
    ==. MI (concatString (concatString xi yi) zi)  
           ((xis `append` 
                 (makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target)))
                 `append` 
                  map (shift (stringLen xi)) (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target)))))
                    `append` map (shift (stringLen xi)) (map (shift (stringLen yi)) zis))
                )
        ? appendGroupNew xis
                         (makeNewIndices xi (concatString yi zi) (fromString (symbolVal (Proxy :: Proxy target))))
                         (map (shift (stringLen xi)) (makeNewIndices yi zi (fromString (symbolVal (Proxy :: Proxy target)))))
                         (map (shift (stringLen xi)) (map (shift (stringLen yi)) zis))
  
  
    ==. MI (concatString (concatString xi yi) zi)  
           ((xis `append` 
                 (makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target)))
                 `append` 
                  makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target))))
                    `append` map (shift (stringLen xi)) (map (shift (stringLen yi)) zis))
                )
        ? shiftNewIndexes xi yi zi (fromString (symbolVal (Proxy :: Proxy target)))
    ==. MI (concatString (concatString xi yi) zi)  
           ((xis `append` 
                 (makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target)))
                 `append` 
                  makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target))))
                    `append` map (shift (stringLen (concatString xi yi))) zis)
                )
        ? map_len_fusion xi yi zis 
  
  -- (x1 ~ (x2 ~ x3)) ~ x4 == ((x1 ~ x2) ~ x3) ~ x4
    ==. MI (concatString (concatString xi yi) zi)  
           (((xis `append` makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
           `append`
              (makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target)))))
           `append` 
              map (shift (stringLen (concatString xi yi))) zis )
        ? appendUnGroupNew xis 
                           (makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
                           (makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target))))
                           (map (shift (stringLen (concatString xi yi))) zis)
  
    ==. MI (concatString (concatString xi yi) zi)  
          ((((xis `append` makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
                         `append` N
                    )
           `append`
              (makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target)))))
           `append` 
              map (shift (stringLen (concatString xi yi))) zis )
            ? appendEmp (xis `append` makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
    ==. MI (concatString (concatString xi yi) zi)  
          ((((xis `append` makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
                         `append` map (shift (stringLen xi)) N
                    )
           `append`
              (makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target)))))
           `append` 
              map (shift (stringLen (concatString xi yi))) zis )
    ==. MI (concatString (concatString xi yi) zi)  
          ((((xis `append` makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
                         `append` map (shift (stringLen xi)) yis
                    )
           `append`
              (makeNewIndices (concatString xi yi) zi (fromString (symbolVal (Proxy :: Proxy target)))))
           `append` 
              map (shift (stringLen (concatString xi yi))) zis )
        ?emptyIndexes y (assumeGoodIndex yi (fromString (symbolVal (Proxy :: Proxy target))) yis)
    ==. mappend (MI (concatString xi yi)  
                    ( (xis `append` makeNewIndices xi yi (fromString (symbolVal (Proxy :: Proxy target))))
                           `append` map (shift (stringLen xi)) yis
                    )
                ) (MI zi zis)
    ==. mappend (mappend (MI xi xis) (MI yi yis)) (MI zi zis)
    *** QED 
  
  -------------------------------------------------------------------------------
  ------------------ Helper Proofs ----------------------------------------------
  -------------------------------------------------------------------------------
  
  
  {-@ assumeGoodIndex :: input:SMTString -> target:SMTString -> is:List Int 
                      -> {v:List (GoodIndex input target) | v == is} @-} 
  assumeGoodIndex :: SMTString -> SMTString -> List Int -> List Int 
  assumeGoodIndex input target is 
    = if isJust (areGoodIndexes input target is) then fromJust (areGoodIndexes input target is) else error ""  
  
  
  {-@ areGoodIndexes :: input:SMTString -> target:SMTString -> is:List Int 
                     -> Maybe ({v:List (GoodIndex input target) | v == is}) @-} 
  areGoodIndexes :: SMTString -> SMTString -> List Int -> Maybe (List Int) 
  areGoodIndexes input target N
    = Just N
  areGoodIndexes input target (C x xs)
    | isGoodIndex input target x 
    = case areGoodIndexes input target xs of 
         Nothing -> Nothing 
         Just is -> Just (C x is) 
    | otherwise
    = Nothing 
  
    
  emptyIndexes :: forall (target :: Symbol). (KnownSymbol target) => MI target SMTString -> List Int  -> Proof
  {-@ emptyIndexes :: mi:MI target SMTString
                   -> is:{List (GoodIndex (inputMI mi) target) | is == indixesMI mi && stringLen (inputMI mi) < stringLen target}
                   -> { is == N } @-}
  emptyIndexes (MI _ _) N 
    = trivial 
  emptyIndexes (MI _ _) (C _ _)
    = trivial 
  
  
  {-@ shiftIndexes
    :: xi:SMTString 
    -> yi:SMTString 
    -> zi:SMTString 
    -> tg:{SMTString | stringLen tg <= stringLen yi } 
    -> {  (makeNewIndices xi (concatString yi zi) tg == makeNewIndices xi yi tg)  
          && 
          (map (shift (stringLen xi)) (makeNewIndices yi zi tg) == makeNewIndices (concatString xi yi) zi tg)
       }
    @-}
  shiftIndexes :: SMTString -> SMTString -> SMTString -> SMTString -> Proof
  shiftIndexes xi yi zi tg = shiftIndexesLeft xi yi zi tg &&& shiftIndexesRight xi yi zi tg 
  
  {-@ reflect chunkString @-}
  {-@ chunkString :: Int -> xs:SMTString -> List (SMTString) / [stringLen xs] @-}
  chunkString :: Int -> SMTString -> List (SMTString)
  chunkString i xs 
    | i <= 0 
    = C xs N 
    | stringLen xs <= i 
    = C xs N 
    | otherwise
    = C (takeString i xs) (chunkString i (dropString i xs))
  
  
  
  {-@ shiftIndexesLeft
    :: xi:SMTString 
    -> yi:SMTString 
    -> zi:SMTString 
    -> tg:{SMTString | stringLen tg <= stringLen yi } 
    -> {  makeNewIndices xi (concatString yi zi) tg == makeNewIndices xi yi tg}
    @-}
  shiftIndexesLeft :: SMTString -> SMTString -> SMTString -> SMTString -> Proof
  shiftIndexesLeft xi yi zi tg
    | stringLen tg < 2 
    =   makeNewIndices xi (concatString yi zi) tg 
    ==. N
    ==. makeNewIndices xi yi tg 
    *** QED 
    | otherwise
    =   makeNewIndices xi (concatString yi zi) tg 
    ==. makeIndices (concatString xi (concatString yi zi)) tg 
                     (maxInt (stringLen xi - (stringLen tg-1)) 0)
                     (stringLen xi - 1)
    ==. makeIndices (concatString (concatString xi yi) zi) tg 
                     (maxInt (stringLen xi - (stringLen tg-1)) 0)
                     (stringLen xi - 1)
       ?concatStringAssoc xi yi zi 
    ==. makeIndices (concatString xi yi) tg 
                     (maxInt (stringLen xi - (stringLen tg-1)) 0)
                     (stringLen xi - 1)                
        ? concatmakeNewIndices (maxInt (stringLen xi - (stringLen tg-1)) 0) (stringLen xi - 1) tg (concatString xi yi) zi 
    ==. makeNewIndices xi yi tg 
    *** QED 
  
  
  
  {-@ concatmakeNewIndices
    :: lo:Nat -> hi:Int
    -> target: SMTString
    -> input : {SMTString | hi + stringLen target <= stringLen input } 
    -> input': SMTString   
    -> {  makeIndices (concatString input input') target lo hi == makeIndices input target lo hi }
    / [hi - lo]  @-}
  concatmakeNewIndices :: Int -> Int -> SMTString -> SMTString -> SMTString  -> Proof
  concatmakeNewIndices lo hi target input input'
    | hi < lo 
    =   makeIndices input target lo hi
    ==. N
    ==. makeIndices (concatString input input') target lo hi 
    *** QED 
    | lo == hi, isGoodIndex input target lo
    =   makeIndices input target lo hi
    ==. lo `C` N
    ==. makeIndices (concatString input input') target lo hi 
        ? isGoodIndexConcatString input input' target lo  
    *** QED 
    | lo == hi
    =  makeIndices input target lo hi 
    ==. N
    ==. makeIndices (concatString input input') target lo hi
        ? isGoodIndexConcatString input input' target lo  
    *** QED 
  concatmakeNewIndices lo hi target input input' 
    | isGoodIndex input target lo
    =   makeIndices input target lo hi
    ==. lo `C` (makeIndices input target (lo + 1) hi)
    ==. lo `C` (makeIndices (concatString input input') target (lo + 1) hi)
         ? concatmakeNewIndices (lo+1) hi target input input'
    ==. makeIndices  (concatString input input') target lo hi
        ? isGoodIndexConcatString input input' target lo  
    *** QED 
    | otherwise 
    =   makeIndices input target lo hi
    ==. makeIndices input target (lo + 1) hi
    ==. makeIndices (concatString input input') target (lo + 1) hi
         ? concatmakeNewIndices (lo+1) hi target input input'
    ==. makeIndices  (concatString input input') target lo hi
        ? isGoodIndexConcatString input input' target lo  
    *** QED 
  
  
  
  {-@ isGoodIndexConcatFront 
    :: input:SMTString -> input':SMTString -> tg:SMTString -> i:Nat
    -> {((isGoodIndex input tg i) <=> isGoodIndex (concatString input' input) tg (stringLen input' + i) )
       } @-}
  isGoodIndexConcatFront :: SMTString -> SMTString -> SMTString -> Int -> Proof 
  isGoodIndexConcatFront input input' tg i 
    =   isGoodIndex input tg i 
    ==. (subString input i (stringLen tg)  == tg  
        && i + stringLen tg <= stringLen input 
        && 0 <= i)  
    ==. (subString input i (stringLen tg)  == tg  
        && (stringLen input' + i) + stringLen tg <= stringLen (concatString input' input) 
        && 0 <= i)  
    ==. (subString (concatString input' input) (stringLen input' + i) (stringLen tg)  == tg  
        && (stringLen input' + i) + stringLen tg <= stringLen (concatString input' input) 
        && 0 <= (stringLen input' + i))  
        ? (subStringConcatFront input input' (stringLen tg) i *** QED)
    ==. isGoodIndex (concatString input' input) tg (stringLen input' + i) 
    *** QED 
  
  
  {-@ isGoodIndexConcatString 
    :: input:SMTString -> input':SMTString -> tg:SMTString -> i:{Int | i + stringLen tg <= stringLen input }
    -> {((isGoodIndex input tg i) <=> isGoodIndex (concatString input input') tg i)
       } @-}
  isGoodIndexConcatString :: SMTString -> SMTString -> SMTString -> Int -> Proof 
  isGoodIndexConcatString input input' tg i 
    =   isGoodIndex input tg i 
    ==. (subString input i (stringLen tg)  == tg  
        && i + stringLen tg <= stringLen input
        && 0 <= i) 
    ==. (subString (concatString input input') i (stringLen tg)  == tg  
        && i + stringLen tg <= stringLen input 
        && 0 <= i)   
        ? (subStringConcat input input' (stringLen tg) i *** QED )
    ==. (subString (concatString input input') i (stringLen tg)  == tg  
        && i + stringLen tg <= stringLen (concatString input input') 
        && 0 <= i)   
        ? (((stringLen input <= stringLen (concatString input input') *** QED ) &&& (lenConcat input input') *** QED))
    ==. isGoodIndex (concatString input input') tg i 
    *** QED 
  
  
  
  
  
  
  {-@ shiftIndexesRight
    :: xi:SMTString 
    -> yi:SMTString 
    -> zi:SMTString 
    -> tg:{SMTString | stringLen tg <= stringLen yi } 
    -> { map (shift (stringLen xi)) (makeNewIndices yi zi tg) == makeNewIndices (concatString xi yi) zi tg }
    @-}
  shiftIndexesRight :: SMTString -> SMTString -> SMTString -> SMTString -> Proof
  shiftIndexesRight xi yi zi tg
    | stringLen tg < 2 
    =   makeNewIndices (concatString xi yi) zi tg 
    ==. N
    ==. map (shift (stringLen xi)) N
    ==. map (shift (stringLen xi)) (makeNewIndices yi zi tg)
    *** QED 
  shiftIndexesRight xi yi zi tg
  -- NV NV NV 
  -- This is suspicious!!! it should require exactly the precondition 
  -- || tg || <= || yi || 
  --   | stringLen tg  <= stringLen yi + 1 
    =   makeNewIndices (concatString xi yi) zi tg  
    ==. makeIndices (concatString (concatString xi yi) zi) tg 
                     (maxInt (stringLen (concatString xi yi) - (stringLen tg -1)) 0)
                     (stringLen (concatString xi yi) - 1 )
    ==. makeIndices (concatString (concatString xi yi) zi) tg 
                     (stringLen (concatString xi yi) - (stringLen tg -1))
                     (stringLen (concatString xi yi) - 1 )
    ==. makeIndices (concatString (concatString xi yi) zi) tg 
                     (stringLen xi + stringLen yi - stringLen tg + 1)
                     (stringLen xi + stringLen yi - 1 )
    ==. makeIndices (concatString xi (concatString yi zi)) tg 
                     (stringLen xi + stringLen yi - stringLen tg + 1)
                     (stringLen xi + stringLen yi - 1 )
         ?concatStringAssoc xi yi zi
    ==. map (shift (stringLen xi)) (makeIndices (concatString yi zi) tg (stringLen yi - stringLen tg + 1) (stringLen yi - 1))
         ? shiftIndexesRight' (stringLen yi - stringLen tg + 1)
                              (stringLen yi - 1)
                              xi 
                              (concatString yi zi)
                              tg 
    ==. map (shift (stringLen xi)) 
                 (makeIndices (concatString yi zi) tg 
                               (maxInt (stringLen yi - (stringLen tg -1)) 0)
                               (stringLen yi -1))
    ==. map (shift (stringLen xi)) 
                 (makeNewIndices yi zi tg)
    *** QED
  
  {-@ shiftIndexesRight'
    :: lo:Nat 
    -> hi:Int  
    -> x:SMTString 
    -> input:SMTString 
    -> tg:SMTString
    -> { map (shift (stringLen x)) (makeIndices input tg lo hi) == makeIndices (concatString x input) tg (stringLen x + lo) (stringLen x + hi) }
    / [if hi < lo then 0 else  hi-lo]
    @-}
  shiftIndexesRight' :: Int -> Int -> SMTString -> SMTString -> SMTString -> Proof
  shiftIndexesRight' lo hi x input target
    | hi < lo 
    =   map (shift (stringLen x)) (makeIndices input target lo hi)
    ==. map (shift (stringLen x)) N
    ==. N
    ==. makeIndices (concatString x input) target (stringLen x + lo) (stringLen x + hi)
    *** QED 
    | lo == hi, isGoodIndex input target lo 
    =   map (shift (stringLen x)) (makeIndices input target lo hi)
    ==. map (shift (stringLen x)) (lo `C` N)
    ==. ((shift (stringLen x)) lo) `C` (map (shift (stringLen x)) N)
    ==. (stringLen x + lo) `C` N
    ==. makeIndices (concatString x input) target (stringLen x + lo) (stringLen x + hi)
       ? isGoodIndexConcatFront input x target lo  -- ( => IsGoodIndex (concatString x input) target (stringLen x + lo))
    *** QED 
    | lo == hi
    =   map (shift (stringLen x)) (makeIndices input target lo hi)
    ==. map (shift (stringLen x)) N
    ==. N
    ==. makeIndices (concatString x input) target (stringLen x + lo) (stringLen x + hi)
       ? (isGoodIndexConcatFront input x target lo *** QED)
    *** QED 
  
  shiftIndexesRight' lo hi x input target
    | isGoodIndex input target lo
    =   map (shift (stringLen x)) (makeIndices input target lo hi)
    ==. map (shift (stringLen x)) (lo `C`(makeIndices input target (lo+1) hi))
    ==. (shift (stringLen x) lo) `C` (map (shift (stringLen x)) (makeIndices input target (lo+1) hi))
    ==. (shift (stringLen x) lo) `C` (makeIndices (concatString x input) target (stringLen x + (lo+1)) (stringLen x + hi))
        ? shiftIndexesRight' (lo+1) hi x input target
    ==. (stringLen x + lo) `C` (makeIndices (concatString x input) target (stringLen x + (lo+1)) (stringLen x + hi))
    ==. makeIndices (concatString x input) target (stringLen x + lo) (stringLen x + hi)
       ? (isGoodIndexConcatFront input x target lo *** QED)
    *** QED 
    | otherwise
    =   map (shift (stringLen x)) (makeIndices input target lo hi)
    ==. map (shift (stringLen x)) (makeIndices input target (lo + 1) hi)
    ==. makeIndices (concatString x input) target (stringLen x + (lo+1)) (stringLen x + hi)
        ? shiftIndexesRight' (lo+1) hi x input target
    ==. makeIndices (concatString x input) target (stringLen x + lo) (stringLen x + hi)
       ? (isGoodIndexConcatFront input x target lo *** QED)
    *** QED 
  
  
  {-@ shiftNewIndexes
    :: xi:SMTString 
    -> yi:SMTString 
    -> zi:SMTString 
    -> tg:{SMTString | stringLen yi < stringLen tg  } 
    -> {  append (makeNewIndices xi (concatString yi zi) tg) (map (shift (stringLen xi)) (makeNewIndices yi zi tg)) == append (makeNewIndices xi yi tg) (makeNewIndices (concatString xi yi) zi tg)
       }
    @-}
  shiftNewIndexes :: SMTString -> SMTString -> SMTString -> SMTString -> Proof
  shiftNewIndexes xi yi zi tg 
    | stringLen tg < 2 
    =   append (makeNewIndices xi (concatString yi zi) tg) (map (shift (stringLen xi)) (makeNewIndices yi zi tg)) 
    ==. append N (map (shift (stringLen xi)) N) 
    ==. map (shift (stringLen xi)) N 
    ==. N 
    ==. append N N
    ==. append (makeNewIndices xi yi tg) (makeNewIndices (concatString xi yi) zi tg)
    *** QED 
  
  shiftNewIndexes xi yi zi tg 
    | stringLen xi == 0 
    =   append (makeNewIndices xi (concatString yi zi) tg) 
                    (map (shift (stringLen xi)) (makeNewIndices yi zi tg))
    ==. append (makeNewIndices stringEmp (concatString yi zi) tg) 
                    (map (shift (stringLen xi)) (makeNewIndices yi zi tg))
    ? stringEmpProp xi 
    ==. append (makeNewIndices stringEmp (concatString yi zi) tg) 
                    (map (shift (stringLen xi)) (makeNewIndices yi zi tg))
    ? makeNewIndicesNullRight (concatString yi zi) tg
    ==. append N
                    (map (shift (stringLen xi)) (makeNewIndices yi zi tg))
    ==. map (shift (stringLen xi)) (makeNewIndices yi zi tg)
    ==. map (shift 0) (makeNewIndices yi zi tg)
        ? mapShiftZero (makeNewIndices yi zi tg)
    ==. makeNewIndices yi zi tg
    ==. makeNewIndices (concatString xi yi) zi tg
          ? concatEmpLeft xi yi 
    ==. append N (makeNewIndices (concatString xi yi) zi tg)
    ==. append (makeNewIndices stringEmp yi tg) (makeNewIndices (concatString xi yi) zi tg)
         ? makeNewIndicesNullRight yi tg
    ==. append (makeNewIndices xi yi tg) (makeNewIndices (concatString xi yi) zi tg)
        ? stringEmpProp xi
    *** QED 
    | stringLen yi == 0 
    =   append (makeNewIndices xi (concatString yi zi) tg) 
                    (map (shift (stringLen xi)) (makeNewIndices yi zi tg))
    ==. append (makeNewIndices xi zi tg) 
                    (map (shift (stringLen xi)) (makeNewIndices yi zi tg))
        ? concatEmpLeft yi zi 
    ==. append (makeNewIndices xi zi tg) 
                    (map (shift (stringLen xi)) (makeNewIndices stringEmp zi tg))
        ? stringEmpProp yi
    ==. append (makeNewIndices xi zi tg) 
                    (map (shift (stringLen xi)) N)
        ? makeNewIndicesNullRight zi tg 
    ==. append (makeNewIndices xi zi tg) 
                    N
    ==. makeNewIndices xi zi tg 
         ?appendEmp (makeNewIndices xi zi tg)
    ==. makeNewIndices (concatString xi yi) zi tg
         ? concatEmpRight xi yi
    ==. append N (makeNewIndices (concatString xi yi) zi tg)
    ==. append (makeNewIndices xi stringEmp tg) (makeNewIndices (concatString xi yi) zi tg)
         ? makeNewIndicesNullLeft xi tg 
    ==. append (makeNewIndices xi yi tg) (makeNewIndices (concatString xi yi) zi tg)
         ? stringEmpProp yi
    *** QED 
    | stringLen yi - stringLen tg == -1 
    = let minidx = maxInt (stringLen xi - stringLen tg + 1) 0 in 
        append (makeNewIndices xi (concatString yi zi) tg) 
                    (map (shift (stringLen xi)) (makeNewIndices yi zi tg)) 
    ==. append (makeIndices (concatString xi (concatString yi zi)) tg
                                  (maxInt (stringLen xi - stringLen tg + 1) 0)
                                  (stringLen xi -1)) 
                    (map (shift (stringLen xi)) 
                              (makeIndices (concatString yi zi) tg
                                            (maxInt (stringLen yi - stringLen tg +1) 0)
                                            (stringLen yi -1)
                              )) 
    ==. append (makeIndices (concatString xi (concatString yi zi)) tg
                                  (maxInt (stringLen xi - stringLen tg + 1) 0)
                                  (stringLen xi -1)) 
                    (map (shift (stringLen xi)) 
                              (makeIndices (concatString yi zi) tg
                                            (maxInt 0 0)
                                            (stringLen yi -1)
                              )) 
    ==. append (makeIndices (concatString xi (concatString yi zi)) tg
                                  (maxInt (stringLen xi - stringLen tg + 1) 0)
                                  (stringLen xi -1)) 
                    (map (shift (stringLen xi)) 
                              (makeIndices (concatString yi zi) tg
                                            0
                                            (stringLen yi -1)
                              )) 
    ==. append (makeIndices (concatString xi (concatString yi zi)) tg
                                  minidx
                                  (stringLen xi -1)) 
                    (makeIndices (concatString xi (concatString yi zi)) tg 
                                  (stringLen xi) 
                                  (stringLen xi + stringLen yi -1)) 
        ? shiftIndexesRight' 0 (stringLen yi -1) xi (concatString yi zi) tg 
    ==. append (makeIndices (concatString (concatString xi yi) zi) tg
                                  minidx
                                  (stringLen xi -1)) 
                    (makeIndices (concatString (concatString xi yi) zi) tg 
                                  (stringLen xi) 
                                  (stringLen xi + stringLen yi -1)) 
        ? concatStringAssoc xi yi zi 
  
    ==. append (append 
  
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  minidx
                                  (stringLen xi + stringLen yi - stringLen tg))
  
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (stringLen xi)
                                  (stringLen xi -1))
  
                                  ) 
                    (makeIndices (concatString (concatString xi yi) zi) tg 
                                  (stringLen xi)
                                  (stringLen xi + stringLen yi -1)) 
        ? mergeIndixes (concatString (concatString xi yi) zi) tg 
                       minidx -- maxInt (stringLen xi - stringLen tg + 1) 0
                       (stringLen xi -1)
                       (stringLen xi -1)
    ==. append (append 
  
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  minidx
                                  (stringLen xi + stringLen yi - stringLen tg))
  
                    N
  
                                  ) 
                    (makeIndices (concatString (concatString xi yi) zi) tg 
                                  (stringLen xi)
                                  (stringLen xi + stringLen yi -1)) 
    ==. append (makeIndices (concatString (concatString xi yi) zi) tg
                                  minidx
                                  (stringLen xi + stringLen yi - stringLen tg))
                    (makeIndices (concatString (concatString xi yi) zi) tg 
                                  (stringLen xi)
                                  (stringLen xi + stringLen yi -1)) 
        ?appendEmp (makeIndices (concatString (concatString xi yi) zi) tg
                                      minidx
                                      (stringLen xi + stringLen yi - stringLen tg))
    ==. append (makeIndices (concatString (concatString xi yi) zi) tg
                                  minidx
                                  (stringLen xi -1))
  
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  ((stringLen xi))
                                  (stringLen xi + stringLen yi -1))
    ==. append (makeIndices (concatString (concatString xi yi) zi) tg
                                  minidx 
                                  (stringLen (concatString xi yi)  - stringLen tg))
  
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (stringLen xi)
                                  (stringLen xi + stringLen yi -1))
  
    ==. append (makeIndices (concatString xi yi) tg 
                                  minidx
                                  (stringLen xi-1)
                    ) 
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (stringLen xi)
                                  (stringLen xi + stringLen yi  - 1)
                    )
        ? catIndixes (concatString xi yi) zi tg minidx (stringLen xi-1)
    ==. append (makeIndices (concatString xi yi) tg 
                                  minidx 
                                  -- maxInt (stringLen xi - stringLen tg + 1) 0 && 2 <= stringLen tg
                                  (stringLen xi-1)
                    ) 
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (stringLen xi)
                                  (stringLen xi + stringLen yi  - 1)
                    )
  
    ==. append (makeIndices (concatString xi yi) tg 
                                  minidx
                                  (stringLen xi-1)
                    ) 
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (maxInt (stringLen xi) 0)
                                  (stringLen xi + stringLen yi  - 1)
                    )
  
  
    ==. append (makeIndices (concatString xi yi) tg 
                                  minidx
                                  (stringLen xi-1)
                    ) 
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (maxInt (stringLen xi + stringLen yi - stringLen tg + 1) 0)
                                  (stringLen xi + stringLen yi  - 1)
                    )
  
    ==. append (makeIndices (concatString xi yi) tg 
                                  minidx
                                  (stringLen xi-1)
                    ) 
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (maxInt (stringLen (concatString xi yi) - stringLen tg + 1) 0)
                                  (stringLen (concatString xi yi) - 1)
                    )
    ==. append (makeIndices (concatString xi yi) tg 
                                  (maxInt (stringLen xi - stringLen tg +1) 0)
                                  (stringLen xi-1)
                    ) 
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (maxInt (stringLen (concatString xi yi) - stringLen tg + 1) 0)
                                  (stringLen (concatString xi yi) - 1)
                    )
    ==. append (makeNewIndices xi yi tg) (makeNewIndices (concatString xi yi) zi tg)
    *** QED 
  shiftNewIndexes xi yi zi tg 
  -- THIS ALWAYS HOLDS 
  --   | stringLen yi + 1 <= stringLen tg
    | 0 <= stringLen xi + stringLen yi - stringLen tg
   --  , 0 < stringLen xi 
    = let minidx = maxInt (stringLen xi - stringLen tg + 1) 0 in 
        append (makeNewIndices xi (concatString yi zi) tg) 
                    (map (shift (stringLen xi)) (makeNewIndices yi zi tg)) 
    ==. append (makeIndices (concatString xi (concatString yi zi)) tg
                                  (maxInt (stringLen xi - stringLen tg + 1) 0)
                                  (stringLen xi -1)) 
                    (map (shift (stringLen xi)) 
                              (makeIndices (concatString yi zi) tg
                                            (maxInt (stringLen yi - stringLen tg +1) 0)
                                            (stringLen yi -1)
                              )) 
    ==. append (makeIndices (concatString xi (concatString yi zi)) tg
                                  minidx
                                  (stringLen xi -1)) 
                    (map (shift (stringLen xi)) 
                              (makeIndices (concatString yi zi) tg
                                             0
                                            (stringLen yi -1)
                              )) 
    ==. append (makeIndices (concatString xi (concatString yi zi)) tg
                                  minidx
                                  (stringLen xi -1)) 
                    (makeIndices (concatString xi (concatString yi zi)) tg 
                                  (stringLen xi) 
                                  (stringLen xi + stringLen yi -1)) 
        ? shiftIndexesRight' 0 (stringLen yi -1) xi (concatString yi zi) tg 
    ==. append (makeIndices (concatString (concatString xi yi) zi) tg
                                  minidx
                                  (stringLen xi -1)) 
                    (makeIndices (concatString (concatString xi yi) zi) tg 
                                  (stringLen xi) 
                                  (stringLen xi + stringLen yi -1)) 
        ? concatStringAssoc xi yi zi 
  
    ==. append (append 
  
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  minidx
                                  (stringLen xi + stringLen yi - stringLen tg))
  
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (stringLen xi + stringLen yi - stringLen tg + 1)
                                  (stringLen xi -1))
  
                                  ) 
                    (makeIndices (concatString (concatString xi yi) zi) tg 
                                  (stringLen xi)
                                  (stringLen xi + stringLen yi -1)) 
        ? mergeIndixes (concatString (concatString xi yi) zi) tg 
                       minidx -- maxInt (stringLen xi - stringLen tg + 1) 0
                       (stringLen xi + stringLen yi - stringLen tg)
                       (stringLen xi -1)
    ==. append (makeIndices (concatString (concatString xi yi) zi) tg
                                  minidx 
                                  (stringLen xi + stringLen yi - stringLen tg))
  
                   (append
  
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (stringLen xi + stringLen yi - stringLen tg +1)
                                  (stringLen xi -1))
  
                                  
                    (makeIndices (concatString (concatString xi yi) zi) tg 
                                  (stringLen xi)
                                  (stringLen xi + stringLen yi -1)) )
        ? appendAssoc
                (makeIndices (concatString (concatString xi yi) zi) tg
                                  minidx
                                  (stringLen xi + stringLen yi - stringLen tg))
                (makeIndices (concatString (concatString xi yi) zi) tg
                                  (stringLen xi + stringLen yi - stringLen tg+1)
                                  (stringLen xi -1))
                (makeIndices (concatString (concatString xi yi) zi) tg 
                                  (stringLen xi)
                                  (stringLen xi + stringLen yi -1))
  
    ==. append (makeIndices (concatString (concatString xi yi) zi) tg
                                  minidx
                                  (stringLen xi + stringLen yi - stringLen tg))
  
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  ((stringLen xi + stringLen yi - stringLen tg+1))
                                  (stringLen xi + stringLen yi -1))
       ? mergeIndixes (concatString (concatString xi yi) zi) tg 
                    ((stringLen xi + stringLen yi - stringLen tg+1))
                    (stringLen xi-1)
                    (stringLen xi + stringLen yi -1)
  
    ==. append (makeIndices (concatString (concatString xi yi) zi) tg
                                  minidx 
                                  (stringLen (concatString xi yi)  - stringLen tg))
  
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (stringLen xi + stringLen yi - stringLen tg + 1)
                                  (stringLen xi + stringLen yi -1))
  
    ==. append (makeIndices (concatString xi yi) tg 
                                  minidx
                                  (stringLen xi-1)
                    ) 
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (stringLen xi + stringLen yi - stringLen tg + 1)
                                  (stringLen xi + stringLen yi  - 1)
                    )
        ? catIndixes (concatString xi yi) zi tg minidx (stringLen xi-1)
  
    ==. append (makeIndices (concatString xi yi) tg 
                                  minidx
                                  (stringLen xi-1)
                    ) 
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (maxInt (stringLen xi + stringLen yi - stringLen tg + 1) 0)
                                  (stringLen xi + stringLen yi  - 1)
                    )
  
    ==. append (makeIndices (concatString xi yi) tg 
                                  minidx
                                  (stringLen xi-1)
                    ) 
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (maxInt (stringLen (concatString xi yi) - stringLen tg + 1) 0)
                                  (stringLen (concatString xi yi) - 1)
                    )
    ==. append (makeIndices (concatString xi yi) tg 
                                  (maxInt (stringLen xi - stringLen tg +1) 0)
                                  (stringLen xi-1)
                    ) 
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (maxInt (stringLen (concatString xi yi) - stringLen tg + 1) 0)
                                  (stringLen (concatString xi yi) - 1)
                    )
    ==. append (makeNewIndices xi yi tg) (makeNewIndices (concatString xi yi) zi tg)
    *** QED 
  
  --   | stringLen yi + 1 <= stringLen tg
    | stringLen xi + stringLen yi < stringLen tg
    =   append (makeNewIndices xi (concatString yi zi) tg) 
                    (map (shift (stringLen xi)) (makeNewIndices yi zi tg)) 
    ==. append (makeIndices (concatString xi (concatString yi zi)) tg
                                  (maxInt (stringLen xi - stringLen tg + 1) 0)
                                  (stringLen xi -1)) 
                    (map (shift (stringLen xi)) 
                              (makeIndices (concatString yi zi) tg
                                            (maxInt (stringLen yi - stringLen tg +1) 0)
                                            (stringLen yi -1)
                              )) 
    ==. append (makeIndices (concatString xi (concatString yi zi)) tg
                                  0
                                  (stringLen xi -1)) 
                    (map (shift (stringLen xi)) 
                              (makeIndices (concatString yi zi) tg
                                             0
                                            (stringLen yi -1)
                              )) 
    ==. append (makeIndices (concatString xi (concatString yi zi)) tg
                                  0
                                  (stringLen xi -1)) 
                    (makeIndices (concatString xi (concatString yi zi)) tg 
                                  (stringLen xi) 
                                  (stringLen xi + stringLen yi -1)) 
        ? shiftIndexesRight' 0 (stringLen yi -1) xi (concatString yi zi) tg 
    ==. append (makeIndices (concatString (concatString xi yi) zi) tg
                                  0
                                  (stringLen xi -1)) 
                    (makeIndices (concatString (concatString xi yi) zi) tg 
                                  (stringLen xi) 
                                  (stringLen xi + stringLen yi -1)) 
        ? concatStringAssoc xi yi zi 
  
    ==. makeIndices (concatString (concatString xi yi) zi) tg
                                  0
                                  (stringLen (concatString xi yi) - 1)
        ?mergeIndixes (concatString (concatString xi yi) zi) tg 
                      0 
                      (stringLen xi-1) 
                      (stringLen (concatString xi yi) -1)
  
    ==. append N 
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  0
                                  (stringLen (concatString xi yi) - 1)
                    )
  
    ==. append (makeIndices (concatString xi yi) tg 
                                  0
                                  (stringLen xi-1)
                    ) 
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  0
                                  (stringLen (concatString xi yi) - 1)
                    )
        ? smallInput (concatString xi yi) tg 0 (stringLen xi -1)
    ==. append (makeIndices (concatString xi yi) tg 
                                  (maxInt (stringLen xi - stringLen tg +1) 0)
                                  (stringLen xi-1)
                    ) 
                    (makeIndices (concatString (concatString xi yi) zi) tg
                                  (maxInt (stringLen (concatString xi yi) - stringLen tg + 1) 0)
                                  (stringLen (concatString xi yi) - 1)
                    )
    ==. append (makeNewIndices xi yi tg) (makeNewIndices (concatString xi yi) zi tg)
    *** QED 
  
  -- NIKI CHECK: Feels have done this proof before 
  maxIndixes 
    :: SMTString -> SMTString -> Int -> Int -> Proof 
  {-@ maxIndixes 
    :: input:SMTString -> target:SMTString -> lo:{Nat | stringLen input < lo + stringLen target} -> hi:Int
    -> {makeIndices input target lo hi = N}
    / [hi - lo ] @-}
  maxIndixes input target lo hi 
    | hi < lo 
    =   makeIndices input target lo hi  
    ==. N
    *** QED 
    | lo == hi, not (isGoodIndex input target lo)
    =   makeIndices input target lo hi  
    ==. N
    *** QED 
    | not (isGoodIndex input target lo)
    =   makeIndices input target lo hi
    ==. N 
    ==. makeIndices input target (lo+1) hi 
        ? maxIndixes input target (lo+1) hi 
    *** QED 
  
  
  mergeIndixes :: SMTString -> SMTString -> Int -> Int -> Int -> Proof
  {-@ mergeIndixes 
    :: input:SMTString -> target:SMTString -> lo:Nat -> mid:{Int | lo <= mid} -> hi:{Int | mid <= hi} 
    -> {makeIndices input target lo hi == append (makeIndices input target lo mid) (makeIndices input target (mid+1) hi)} 
    / [mid] @-}
  mergeIndixes input target lo mid hi 
    | lo == mid, isGoodIndex input target lo 
    =   append (makeIndices input target lo mid) (makeIndices input target (mid+1) hi)
    ==. append (makeIndices input target lo lo)  (makeIndices input target (mid+1) hi)
    ==. append (lo `C` N)  (makeIndices input target (mid+1) hi)
    ==. lo  `C` (append N  (makeIndices input target (lo+1) hi))
    ==. lo  `C` (makeIndices input target (lo+1) hi)
    ==. makeIndices input target lo hi
    *** QED 
    | lo == mid, not (isGoodIndex input target lo)
    =   append (makeIndices input target lo mid) (makeIndices input target (mid+1) hi)
    ==. append (makeIndices input target lo lo)  (makeIndices input target (mid+1) hi)
    ==. append (lo `C` N)  (makeIndices input target (mid+1) hi)
    ==. (append N  (makeIndices input target (lo+1) hi))
    ==. makeIndices input target lo hi
    *** QED 
    | lo < mid, not (isGoodIndex input target mid)
    =   makeIndices input target lo hi
    ==. append (makeIndices input target lo (mid-1)) 
                    (makeIndices input target mid hi)
         ? mergeIndixes input target lo (mid-1) hi 
  
    ==. append (makeIndices input target lo (mid-1)) 
                    (makeIndices input target (mid+1) hi)
  
    ==. append (makeIndices input target lo mid) 
                    (makeIndices input target (mid+1) hi)
        ?makeNewIndicesBadLast input target lo mid
    *** QED 
    | lo < mid, isGoodIndex input target mid
    =   makeIndices input target lo hi
    ==. append (makeIndices input target lo (mid-1)) 
                    (makeIndices input target mid hi)
         ? mergeIndixes input target lo (mid-1) hi 
  
    ==. append (makeIndices input target lo (mid-1)) 
                    (mid `C` makeIndices input target (mid+1) hi)
  
  
    ==. append (makeIndices input target lo (mid-1)) 
                    (mid `C` (append N (makeIndices input target (mid+1) hi)))
  
    ==. append (makeIndices input target lo (mid-1)) 
                    (append (C mid N) (makeIndices input target (mid+1) hi))
  
    ==. append (append (makeIndices input target lo (mid-1)) (C mid N)) 
                    (makeIndices input target (mid+1) hi)
        ? appendAssoc (makeIndices input target lo (mid-1)) (C mid N) (makeIndices input target (mid+1) hi)
  
    ==. append (makeIndices input target lo mid) 
                    (makeIndices input target (mid+1) hi)
        ?makeNewIndicesGoodLast input target lo mid
    *** QED 
  
  
  makeNewIndicesGoodLast, makeNewIndicesBadLast 
    :: SMTString -> SMTString -> Int -> Int -> Proof 
  {-@ makeNewIndicesGoodLast 
    :: input:SMTString -> target:SMTString -> lo:Nat -> hi:{Int | lo <= hi && (isGoodIndex input target hi)}
    -> {makeIndices input target lo hi == append (makeIndices input target lo (hi-1)) (C hi N)}
    / [hi - lo] @-}
  makeNewIndicesGoodLast input target lo hi 
    | lo == hi, (isGoodIndex input target lo)
    =   makeIndices input target lo hi 
    ==. hi `C` N 
    ==. append (N) (C hi N)
    ==. append (makeIndices input target lo (hi-1)) (C hi N)
    *** QED 
    | not (isGoodIndex input target lo), isGoodIndex input target hi 
    =   makeIndices input target lo hi 
    ==. makeIndices input target (lo+1) hi
    ==. append (makeIndices input target (lo+1) (hi-1)) (C hi N)
         ? makeNewIndicesGoodLast input target (lo+1) hi  
    ==. append (makeIndices input target lo (hi-1)) (C hi N)
    *** QED 
    | isGoodIndex input target lo, isGoodIndex input target hi
    =   makeIndices input target lo hi 
    ==. lo `C` makeIndices input target (lo+1) hi
    ==. lo `C` (append (makeIndices input target (lo+1) (hi-1)) (C hi N))
         ? makeNewIndicesGoodLast input target (lo+1) hi  
    ==. (append (lo `C` makeIndices input target (lo+1) (hi-1)) (C hi N))
    ==. append (makeIndices input target lo (hi-1)) (C hi N)
    *** QED 
  
  {-@ makeNewIndicesBadLast 
    :: input:SMTString -> target:SMTString -> lo:Nat -> hi:{Int | lo <= hi && (not (isGoodIndex input target hi))}
    -> {makeIndices input target lo hi == makeIndices input target lo (hi-1)}
    / [hi - lo]
  @-}
  -- NV sweet proof 
  makeNewIndicesBadLast input target lo hi 
    | lo == hi, not (isGoodIndex input target lo)
    =   makeIndices input target lo (hi-1) 
    ==. N 
    ==. makeIndices input target lo hi
    *** QED 
    | not (isGoodIndex input target lo), not (isGoodIndex input target hi) 
    =   makeIndices input target lo hi 
    ==. makeIndices input target (lo+1) hi
    ==. makeIndices input target (lo+1) (hi-1)
         ? makeNewIndicesBadLast input target (lo+1) hi   
    ==. makeIndices input target lo (hi-1)
    *** QED 
    | isGoodIndex input target lo , not (isGoodIndex input target hi) 
    =   makeIndices input target lo hi 
    ==. lo `C` makeIndices input target (lo+1) hi
    ==. lo `C` makeIndices input target (lo+1) (hi-1)
         ? makeNewIndicesBadLast input target (lo+1) hi   
    ==. makeIndices input target lo (hi-1)
    *** QED 
  
  
  catIndixes :: SMTString -> SMTString -> SMTString -> Int -> Int -> Proof 
  {-@ catIndixes 
       :: input:SMTString -> x:SMTString 
       -> target:{SMTString | 0 <= stringLen input - stringLen target + 1} 
       -> lo:{Nat | lo <= stringLen input - stringLen target } 
       -> hi:{Int | stringLen input - stringLen target <= hi}
       -> { makeIndices input target lo hi == makeIndices (concatString input x) target lo (stringLen input - stringLen target) }
    @-}
  catIndixes input x target lo hi 
    =   makeIndices input target lo hi
    ==. append (makeIndices input target lo (stringLen input - stringLen target))
                    (makeIndices input target (stringLen input - stringLen target + 1) hi)
         ? mergeIndixes input target lo (stringLen input - stringLen target) hi
    ==. append (makeIndices input target lo (stringLen input - stringLen target))
                    N
         ? maxIndixes input target (stringLen input - stringLen target + 1) hi
    ==. makeIndices input target lo (stringLen input - stringLen target)
         ? appendEmp (makeIndices input target lo (stringLen input - stringLen target))
    ==. makeIndices (concatString input x) target lo (stringLen input - stringLen target)
         ? concatmakeNewIndices lo (stringLen input - stringLen target) target input x 
    *** QED 
  
  
  
  
  map_len_fusion :: SMTString -> SMTString -> List Int -> Proof
  {-@ map_len_fusion 
    :: xi:SMTString 
    -> yi:SMTString 
    -> zis:List Int 
    -> {  map (shift (stringLen (concatString xi yi))) zis == map (shift (stringLen xi)) (map (shift (stringLen yi)) zis) 
       }
    @-}
  map_len_fusion xi yi N 
    =   map (shift (stringLen (concatString xi yi))) N
    ==. N
    ==. map (shift (stringLen xi)) N
    ==. map (shift (stringLen xi)) (map (shift (stringLen yi)) N)
    *** QED  
  map_len_fusion xi yi (C i is)
    =   map (shift (stringLen (concatString xi yi))) (C i is)
    ==. shift (stringLen (concatString xi yi)) i `C` map (shift (stringLen (concatString xi yi))) is 
    ==. shift (stringLen xi + stringLen yi) i `C` map (shift (stringLen (concatString xi yi))) is 
        ? concatLen xi yi 
    ==. shift (stringLen xi) (shift (stringLen yi) i) `C` map (shift (stringLen (concatString xi yi))) is 
        ? concatLen xi yi 
    ==. shift (stringLen xi) (shift (stringLen yi) i) `C` map (shift (stringLen xi)) (map (shift (stringLen yi)) is)
        ? map_len_fusion xi yi is 
    ==. map (shift (stringLen xi)) (shift (stringLen yi) i `C` map (shift (stringLen yi)) is)
    ==. map (shift (stringLen xi)) (map (shift (stringLen yi)) (i `C` is))
    *** QED 
  
  smallInput :: SMTString -> SMTString -> Int -> Int -> Proof  
  {-@ smallInput :: input:SMTString -> target:{SMTString | stringLen input < stringLen target } -> lo:Nat -> hi:Int 
             -> {makeIndices input target lo hi == N } 
             / [hi -lo]
    @-}
  smallInput input target lo hi 
    | hi < lo 
    = makeIndices input target lo hi 
    ==. N
    *** QED  
    | lo == hi, not (isGoodIndex input target lo)
    = makeIndices input target lo hi 
    ==. N
    *** QED  
    | not (isGoodIndex input target lo)
    = makeIndices input target lo hi 
    ==. makeIndices input target (lo+1) hi
    ==. N ? smallInput input target (lo+1) hi 
    *** QED  
  
  
  
  -------------------------------------------------------------------------------
  ----------  Indexing ----------------------------------------------------------
  -------------------------------------------------------------------------------
  
     
  data List a = N | C a (List a) deriving (Show, Eq)
  {-@ data List [idxlen] a = N | C {idxhd :: a , idxtl :: List a} @-}
  
  
  {-@ measure idxlen @-}
  {-@ idxlen :: List a -> Nat @-} 
  idxlen :: List a -> Int 
  idxlen N = 0 
  idxlen (C _ xs) = 1 + idxlen xs 
  
  {-@ reflect map @-}
  map :: (a -> b) -> List a -> List b
  map _ N = N
  map f (C x xs) = C (f x) (map f xs)
  
  {-@ reflect append @-}
  append :: List a -> List a -> List a 
  append N xs = xs 
  append (C x xs) ys = C x (append xs ys)
  
  {-@ reflect shift @-}
  shift :: Int -> Int -> Int 
  shift x y = x + y 
  
  {-@ symbolVal :: forall n proxy. KnownSymbol n => x:proxy n 
    -> {v:String | v == n && v == symbolVal x } @-}
  {-@ measure symbolVal :: p n -> String @-}
  
  {-@ reflect makeNewIndices @-}
  {-@ makeNewIndices :: s1:SMTString -> s2:SMTString -> target:SMTString -> List (GoodIndex {concatString s1 s2} target) @-}
  makeNewIndices :: SMTString -> SMTString -> SMTString -> List Int 
  makeNewIndices s1 s2 target
    | stringLen target < 2 
    = N
    | otherwise
    = makeIndices (concatString s1 s2) target
                   (maxInt (stringLen s1 - (stringLen target-1)) 0)
                   (stringLen s1 - 1)
  
  
  {-@ reflect maxInt @-}
  maxInt :: Int -> Int -> Int 
  maxInt x y = if x <= y then y else x 
  
  {-@ reflect makeIndices @-}
  
  makeIndices :: SMTString -> SMTString -> Int -> Int -> List Int 
  {-@ makeIndices :: input:SMTString -> target:SMTString -> lo:{Int | 0 <= lo} -> hi:Int -> List (GoodIndex input target) 
    / [hi - lo] @-}
  makeIndices input target lo hi 
    | hi < lo 
    = N
    | lo == hi, isGoodIndex input target lo
    = lo `C` N
    | lo == hi 
    = N
  makeIndices input target lo hi 
    | isGoodIndex input target lo
    = lo `C` (makeIndices input target (lo + 1) hi)
    | otherwise 
    =    makeIndices input target (lo + 1) hi 
  
  {-@ reflect isGoodIndex @-}
  isGoodIndex :: SMTString -> SMTString -> Int -> Bool 
  {-@ isGoodIndex :: input:SMTString -> target:SMTString -> i:Int 
    -> {b:Bool | Prop b <=> IsGoodIndex input target i} @-}
  isGoodIndex input target i 
    =  subString input i (stringLen target)  == target  
    && i + stringLen target <= stringLen input
    && 0 <= i    
  -------------------------------------------------------------------------------
  ----------  Indexing Properties -----------------------------------------------
  -------------------------------------------------------------------------------
  
  {-@ appendEmp :: xs:List a -> {append xs N = xs } @-} 
  appendEmp :: List a -> Proof 
  appendEmp N 
    =   append N N
    ==. N
    *** QED 
  appendEmp (C x xs) 
    =   append (C x xs) N
    ==. C x (append xs N)
    ==. C x xs ? appendEmp xs 
    *** QED 
  
  
  {-@ appendAssoc :: x:List a -> y:List a -> z:List a 
       -> {(append x (append y z)) == (append (append x y) z) } @-}
  appendAssoc :: List a -> List a -> List a -> Proof
  appendAssoc N y z 
    =   append N (append y z)
    ==. append y z
    ==. append (append N y) z
    *** QED 
  appendAssoc (C x xs) y z
    =   append (C x xs) (append y z) 
    ==. C x (append xs (append y z))
    ==. C x (append (append xs y) z)
          ? appendAssoc xs y z
    ==. append (C x (append xs y)) z
    ==. append (append (C x xs) y) z
    *** QED 
  
  
  
  
  makeNewIndicesNullRight :: SMTString -> SMTString -> Proof 
  {-@ makeNewIndicesNullRight 
    :: s1:SMTString 
    -> t:SMTString 
    -> {makeNewIndices stringEmp s1 t == N } @-} 
  makeNewIndicesNullRight s t 
    | stringLen t < 2 
    = makeNewIndices stringEmp s t  ==. N *** QED 
  makeNewIndicesNullRight s t 
    =   makeNewIndices stringEmp s t
    ==. makeIndices (concatString stringEmp s) t
                     (maxInt (1 + stringLen stringEmp - stringLen t) 0)
                     (stringLen stringEmp - 1)
    ==. makeIndices s t
                     (maxInt (1 - stringLen t) 0)
                     (-1)
        ? concatStringNeutralRight s 
    ==. makeIndices s t 0 (-1)
    ==. N ? makeNewIndicesNullRightEmp s t  
    *** QED 
  
  
  -- (x1 ~ x2) ~ (x3 ~ x4)
  -- == 
  -- ((x1 ~ (x2 ~ x3)) ~ x4)
  
  
  appendGroupNew :: List a -> List a -> List a -> List a -> Proof
  {-@ appendGroupNew 
    :: x1:List a 
    -> x2:List a 
    -> x3:List a 
    -> x4:List a 
    -> {   (append (append x1 x2) (append x3 x4))
        == (append (append x1 (append x2 x3)) x4)
       } @-}
  appendGroupNew x1 x2 x3 x4 
    =   (append (append x1 x2) (append x3 x4))
    ==. (append (append (append x1 x2) x3) x4)
        ? appendAssoc (append x1 x2) x3 x4  
    ==. (append (append x1 (append x2 x3)) x4)
        ? appendAssoc x1 x2 x3
    *** QED 
  
  
  
  -- (x1 ~ (x2 ~ x3)) ~ x4 == ((x1 ~ x2) ~ x3) ~ x4
  
  appendUnGroupNew :: List a -> List a -> List a -> List a -> Proof
  {-@ appendUnGroupNew 
    :: x1:List a 
    -> x2:List a 
    -> x3:List a 
    -> x4:List a 
    -> {   ((append (append (append x1 x2) x3) x4))
        == (append (append x1 (append x2 x3)) x4)
       } @-}
  appendUnGroupNew x1 x2 x3 x4 
    =   append (append (append x1 x2) x3) x4
    ==. append (append x1 (append x2 x3)) x4
        ? appendAssoc x1 x2 x3 
    *** QED 
  
  
  appendReorder :: List a -> List a -> List a -> List a -> List a -> Proof
  {-@ appendReorder 
    :: x1:List a 
    -> x2:List a 
    -> x3:List a 
    -> x4:List a 
    -> x5:List a 
    -> {   (append (append x1 x2) (append (append x3 x4) x5))
        == (append (append (append (append x1 x2) x3) x4) x5)
       } @-}
  appendReorder x1 x2 x3 x4 x5 
    =   append (append x1 x2) (append (append x3 x4) x5)
    ==. append (append x1 x2) (append x3 (append x4 x5))
         ? appendAssoc x3 x4 x5 
    ==. append (append (append x1 x2) x3) (append x4 x5)
        ? appendAssoc (append x1 x2) x3 (append x4 x5) 
    ==. append ((append (append (append x1 x2) x3)) x4) x5
        ? appendAssoc (append (append x1 x2) x3) x4 x5 
    *** QED 
  
  -- ((x1~x2) ~ ((x3~x4) ~ x5))
  -- == 
  --   ((((x1~x2) ~x3) ~x4) ~x5
  
  map_append :: (a -> b) -> List a -> List a -> Proof
  {-@ map_append 
       :: f:(a -> b) -> xs:List a -> ys:List a 
       -> {map f (append xs ys) == append (map f xs) (map f ys)}
    @-}
  map_append f N ys 
    =   map f (append N ys)
    ==. map f ys 
    ==. append N (map f ys)
    ==. append (map f N) (map f ys)
    *** QED 
  map_append f (C x xs) ys 
    =   map f (append (C x xs) ys)
    ==. map f (x `C` (append xs ys))
    ==. f x `C` (map f (append xs ys))
    ==. f x `C` (append (map f xs) (map f ys))
        ? map_append f xs ys 
    ==. append (f x `C` map f xs) (map f ys)
    ==. append (map f (x `C` xs)) (map f ys)
    *** QED 
  
  mapShiftZero :: List Int -> Proof
  {-@ mapShiftZero :: is:List Int -> {map (shift 0) is == is } @-}
  mapShiftZero N 
    = map (shift 0) N ==. N *** QED
  mapShiftZero (C i is)
    =   map (shift 0) (C i is)
    ==. shift 0 i `C` map (shift 0) is 
    ==. i `C` is ? mapShiftZero is  
    *** QED 
  
  
  {-@ makeNewIndicesNullRightEmp :: s:SMTString -> t:SMTString -> {makeIndices s t 0 (-1) == N } @-}
  makeNewIndicesNullRightEmp :: SMTString -> SMTString -> Proof
  makeNewIndicesNullRightEmp s t 
    =   makeIndices s t 0 (-1) 
    ==. N
    *** QED 
  
  makeNewIndicesNullLeft :: SMTString -> SMTString -> Proof 
  {-@ makeNewIndicesNullLeft 
    :: s:SMTString 
    -> t:SMTString 
    -> {makeNewIndices s stringEmp t == N } @-} 
  makeNewIndicesNullLeft s t 
    | stringLen t < 2 
    = makeNewIndices s stringEmp t ==. N *** QED 
  makeNewIndicesNullLeft  s t 
    | 1 + stringLen s <= stringLen t
    =   makeNewIndices s stringEmp t
    ==. makeIndices (concatString s stringEmp) t
                     (maxInt (1 + stringLen s - stringLen t)  0)
                     (stringLen s - 1)
    ==. makeIndices s t
                     0
                     (stringLen s - 1) 
                     ? concatStringNeutral s
    ==. makeIndices s t
                     0
                     (stringLen s - 1)
    ==. N ? makeNewIndicesNull1 s t 0 (stringLen s - 1)
    *** QED 
  makeNewIndicesNullLeft s t 
    =   makeNewIndices s stringEmp t
    ==. makeIndices (concatString s stringEmp) t
                     (maxInt (1 + stringLen s - stringLen t)  0)
                     (stringLen s - 1)
    ==. makeIndices (concatString s stringEmp) t
                     (1 + stringLen s - stringLen t)
                     (stringLen s - 1)
    ==. makeIndices s t
                     (1 + stringLen s - stringLen t)
                     (stringLen s - 1) ? concatStringNeutral s 
    ==. N ? makeNewIndicesNull2 s t (1 + stringLen s - stringLen t) (stringLen s - 1)
    *** QED 
  
  
  makeNewIndicesNull1 :: SMTString -> SMTString -> Int -> Int -> Proof 
  {-@ makeNewIndicesNull1 
    :: s:SMTString 
    -> t:{SMTString | 1 + stringLen s <= stringLen t } 
    -> lo:Nat 
    -> hi:Int
    -> {makeIndices s t lo hi == N } / [hi - lo] @-} 
  makeNewIndicesNull1 s1 t lo hi
    | hi < lo 
    = makeIndices s1 t lo hi ==. N *** QED 
    | lo == hi, not (isGoodIndex s1 t lo)
    = makeIndices s1 t lo hi ==. N *** QED  
    | not (isGoodIndex s1 t lo)
    =   makeIndices s1 t lo hi
    ==. makeIndices s1 t (lo + 1) hi 
    ==. N ? makeNewIndicesNull1 s1 t (lo+1) hi
    *** QED 
  
  
  makeNewIndicesNull2 :: SMTString -> SMTString -> Int -> Int -> Proof 
  {-@ makeNewIndicesNull2 
    :: s:SMTString 
    -> t:{SMTString | stringLen t < 2 + stringLen s } 
    -> lo:{Int | -1 <= lo && 1 + stringLen s - stringLen t <= lo  } 
    -> hi:{Int | lo <= hi}
    -> {makeIndices s t lo hi == N } / [hi - lo] @-} 
  makeNewIndicesNull2 s1 t lo hi
    | lo == hi, not (isGoodIndex s1 t lo)
    = makeIndices s1 t lo hi ==. N *** QED  
    | not (isGoodIndex s1 t lo)
    =   makeIndices s1 t lo hi
    ==. makeIndices s1 t (lo + 1) hi 
    ==. N ? makeNewIndicesNull2 s1 t (lo+1) hi
    *** QED 
   
  